Add virtual state management and JSON serialization to graph and reso…

…lver classes

include/graph.hpp

@@ -37,6 +37,9 @@ namespace ratio
 
   public:
     graph(std::string_view name = "oRatio");
+    virtual ~graph() = default;
+
+    [[nodiscard]] virtual json::json to_json() const override;
 
   protected:
     /**
@@ -225,6 +228,8 @@ namespace ratio
 
     [[nodiscard]] bool is_expanded() const noexcept { return expanded; }
 
+    [[nodiscard]] virtual utils::lbool get_state() const = 0;
+
     [[nodiscard]] const std::vector<std::reference_wrapper<resolver>> get_causes() const noexcept { return causes; }
 
     [[nodiscard]] const std::vector<std::reference_wrapper<resolver>> get_resolvers() const noexcept { return resolvers; }
@@ -233,6 +238,10 @@ namespace ratio
 
     [[nodiscard]] const std::vector<std::reference_wrapper<resolver>> get_supports() const noexcept { return supports; }
 
+    [[nodiscard]] virtual json::json to_json() const;
+
+    [[nodiscard]] uintptr_t get_id() const noexcept { return reinterpret_cast<uintptr_t>(this); }
+
   protected:
     template <typename Tp, typename... Args>
     Tp &new_resolver(Args &&...args) noexcept
@@ -267,12 +276,18 @@ namespace ratio
     [[nodiscard]] flaw &get_flaw() noexcept { return f; }
     [[nodiscard]] const flaw &get_flaw() const noexcept { return f; }
 
+    [[nodiscard]] virtual utils::lbool get_state() const = 0;
+
     [[nodiscard]] const utils::rational &get_intrinsic_cost() const noexcept { return intrinsic_cost; }
 
     [[nodiscard]] const std::vector<std::reference_wrapper<flaw>> &get_preconditions() const noexcept { return preconditions; }
 
     [[nodiscard]] utils::rational get_estimated_cost() const noexcept;
 
+    [[nodiscard]] virtual json::json to_json() const;
+
+    [[nodiscard]] uintptr_t get_id() const noexcept { return reinterpret_cast<uintptr_t>(this); }
+
   private:
     virtual void apply() = 0;
 

include/timeline.hpp

@@ -0,0 +1,15 @@
+#pragma once
+
+#include "json.hpp"
+
+namespace ratio
+{
+  class timeline
+  {
+  public:
+    timeline() = default;
+    virtual ~timeline() = default;
+
+    [[nodiscard]] virtual json::json extract() const = 0;
+  };
+} // namespace ratio

include/z3/z3flaws.hpp

@@ -10,6 +10,8 @@ namespace ratio
   public:
     z3flaw(z3solver &slv, std::vector<std::reference_wrapper<resolver>> &&causes) noexcept;
 
+    [[nodiscard]] utils::lbool get_state() const noexcept override;
+
     [[nodiscard]] z3::expr &get_phi() noexcept { return phi; }
     [[nodiscard]] const z3::expr &get_phi() const noexcept { return phi; }
 
@@ -30,6 +32,8 @@ namespace ratio
     z3resolver(flaw &f, utils::rational &&intrinsic_cost) noexcept;
     z3resolver(flaw &f, utils::rational &&intrinsic_cost, z3::expr &&rho) noexcept;
 
+    [[nodiscard]] utils::lbool get_state() const noexcept override;
+
     [[nodiscard]] z3::expr &get_rho() noexcept { return rho; }
     [[nodiscard]] const z3::expr &get_rho() const noexcept { return rho; }
 

src/graph.cpp

@@ -7,6 +7,12 @@ namespace ratio
 {
     graph::graph(std::string_view name) : core(name) {}
 
+    json::json graph::to_json() const
+    {
+        json::json j_graph = core::to_json();
+        return j_graph;
+    }
+
     std::vector<std::reference_wrapper<flaw>> graph::get_queued_flaws() const noexcept
     {
         std::vector<std::reference_wrapper<flaw>> res;
@@ -83,6 +89,7 @@ namespace ratio
             supports.push_back(cause);                  // .. and it also supports the `cause` cause..
         }
     }
+
     utils::rational flaw::compute_cost() const
     {
         switch (resolvers.size())
@@ -99,6 +106,28 @@ namespace ratio
         }
     }
 
+    json::json flaw::to_json() const
+    {
+        json::json j_flaw{{"cost", {{"num", est_cost.numerator()}, {"den", est_cost.denominator()}}}};
+        switch (get_state())
+        {
+        case utils::True:
+            j_flaw["state"] = "active";
+            break;
+        case utils::False:
+            j_flaw["state"] = "forbidden";
+            break;
+        case utils::Undefined:
+            j_flaw["state"] = "inactive";
+            break;
+        }
+        json::json j_causes(json::json_type::array);
+        for (const auto &c : causes)
+            j_causes.push_back(c.get().get_id());
+        j_flaw["causes"] = std::move(j_causes);
+        return j_flaw;
+    }
+
     resolver::resolver(flaw &f, utils::rational &&intrinsic_cost) : f(f), intrinsic_cost(intrinsic_cost) { f.resolvers.push_back(*this); }
 
     utils::rational resolver::resolver::get_estimated_cost() const noexcept
@@ -118,4 +147,26 @@ namespace ratio
                                     .get_estimated_cost();
 #endif
     }
+
+    json::json resolver::to_json() const
+    {
+        json::json j_resolver{{"cost", {{"num", intrinsic_cost.numerator()}, {"den", intrinsic_cost.denominator()}}}};
+        switch (get_state())
+        {
+        case utils::True:
+            j_resolver["state"] = "active";
+            break;
+        case utils::False:
+            j_resolver["state"] = "forbidden";
+            break;
+        case utils::Undefined:
+            j_resolver["state"] = "inactive";
+            break;
+        }
+        json::json j_preconditions(json::json_type::array);
+        for (const auto &p : preconditions)
+            j_preconditions.push_back(p.get().get_id());
+        j_resolver["preconditions"] = std::move(j_preconditions);
+        return j_resolver;
+    }
 } // namespace ratio

src/z3/z3flaws.cpp

@@ -9,6 +9,17 @@ namespace ratio
             slv.slv.add(z3::implies(phi, pos <= static_cast<z3flaw &>(cause.get().get_flaw()).get_position() - 1));
     }
 
+    utils::lbool z3flaw::get_state() const noexcept
+    {
+        auto val = static_cast<const z3solver &>(get_graph()).mdl.eval(phi, true);
+        if (val.is_true())
+            return utils::True;
+        else if (val.is_false())
+            return utils::False;
+        else
+            return utils::Undefined;
+    }
+
     z3::expr z3flaw::compute_phi(z3solver &slv, const std::vector<std::reference_wrapper<resolver>> &causes) noexcept
     {
         z3::expr_vector args(slv.ctx);
@@ -20,6 +31,17 @@ namespace ratio
     z3resolver::z3resolver(flaw &f, utils::rational &&intrinsic_cost) noexcept : resolver(f, std::move(intrinsic_cost)), rho(static_cast<z3solver &>(f.get_graph()).ctx.bool_const(("b" + std::to_string(static_cast<z3solver &>(f.get_graph()).bool_count++)).c_str())) {}
     z3resolver::z3resolver(flaw &f, utils::rational &&intrinsic_cost, z3::expr &&rho) noexcept : resolver(f, std::move(intrinsic_cost)), rho(std::move(rho)) {}
 
+    utils::lbool z3resolver::get_state() const noexcept
+    {
+        auto val = static_cast<const z3solver &>(get_flaw().get_graph()).mdl.eval(rho, true);
+        if (val.is_true())
+            return utils::True;
+        else if (val.is_false())
+            return utils::False;
+        else
+            return utils::Undefined;
+    }
+
     void z3resolver::add(const z3::expr &e) { static_cast<z3solver &>(get_flaw().get_graph()).slv.add(z3::implies(rho, e)); }
 
     z3atom_flaw::z3atom_flaw(z3solver &slv, std::vector<std::reference_wrapper<resolver>> &&causes, bool is_fact, riddle::predicate &pred, std::map<std::string, std::shared_ptr<riddle::item>, std::less<>> &&args) noexcept : z3flaw(slv, std::move(causes)), atm(std::make_shared<atom>(*this, pred, is_fact, std::move(args))) {}