Enhance z3solver with JSON serialization methods and update atom stat…

…e handling

include/z3/z3solver.hpp

@@ -19,6 +19,8 @@ namespace ratio
 
     [[nodiscard]] riddle::bool_expr operator==(riddle::expr rhs) const override;
 
+    [[nodiscard]] json::json to_json() const override;
+
   private:
     z3::expr expr;
   };
@@ -35,6 +37,8 @@ namespace ratio
 
     [[nodiscard]] riddle::bool_expr operator==(riddle::expr rhs) const override;
 
+    [[nodiscard]] json::json to_json() const override;
+
   private:
     z3::expr expr;
   };
@@ -49,6 +53,8 @@ namespace ratio
 
     [[nodiscard]] riddle::bool_expr operator==(riddle::expr rhs) const override;
 
+    [[nodiscard]] json::json to_json() const override;
+
   private:
     z3::expr expr;
   };
@@ -63,6 +69,8 @@ namespace ratio
 
     [[nodiscard]] riddle::bool_expr operator==(riddle::expr rhs) const override;
 
+    [[nodiscard]] json::json to_json() const override;
+
   private:
     z3::expr expr;
   };
@@ -79,7 +87,9 @@ namespace ratio
 
     [[nodiscard]] riddle::bool_expr operator==(riddle::expr rhs) const override;
 
-    [[nodiscard]] bool is_active() const noexcept;
+    [[nodiscard]] riddle::atom_state get_state() const override;
+
+    [[nodiscard]] json::json to_json() const override;
 
   private:
     z3flaw &flaw;   // the flaw associated with this atom..
@@ -121,6 +131,7 @@ namespace ratio
 
     [[nodiscard]] riddle::string_expr new_string() override;
     [[nodiscard]] riddle::string_expr new_string(std::string &&value) override;
+    [[nodiscard]] std::string string_value(const riddle::string_item &expr) const noexcept override;
 
     [[nodiscard]] riddle::enum_expr new_enum(riddle::type &tp, std::vector<std::reference_wrapper<utils::enum_val>> &&values) override;
     [[nodiscard]] utils::enum_val &enum_value(const riddle::enum_item &expr) const noexcept override;

src/z3/z3solver.cpp

@@ -31,6 +31,12 @@ namespace ratio
         else
             assert(false);
     }
+    json::json bool_item::to_json() const
+    {
+        json::json j = riddle::bool_item::to_json();
+        j["lit"] = expr.to_string();
+        return j;
+    }
 
     riddle::bool_expr arith_item::operator==(riddle::expr rhs) const
     {
@@ -56,6 +62,12 @@ namespace ratio
         else
             assert(false);
     }
+    json::json arith_item::to_json() const
+    {
+        json::json j = riddle::arith_item::to_json();
+        j["lin"] = expr.to_string();
+        return j;
+    }
 
     riddle::bool_expr string_item::operator==(riddle::expr rhs) const
     {
@@ -81,6 +93,12 @@ namespace ratio
         else
             assert(false);
     }
+    json::json string_item::to_json() const
+    {
+        json::json j = riddle::string_item::to_json();
+        j["str"] = expr.to_string();
+        return j;
+    }
 
     riddle::bool_expr enum_item::operator==(riddle::expr rhs) const
     {
@@ -149,6 +167,12 @@ namespace ratio
                 return std::make_shared<bool_item>(static_cast<riddle::bool_type &>(get_type()), ctx.bool_val(false));
         }
     }
+    json::json enum_item::to_json() const
+    {
+        json::json j = riddle::enum_item::to_json();
+        j["var"] = expr.to_string();
+        return j;
+    }
 
     atom::atom(z3flaw &flaw, riddle::predicate &pred, bool is_fact, std::map<std::string, std::shared_ptr<riddle::item>, std::less<>> &&args) : riddle::atom(pred, is_fact, std::move(args)), flaw(flaw), sigma(static_cast<z3solver &>(get_core()).ctx.int_const(("a" + std::to_string(static_cast<z3solver &>(get_core()).atom_count++)).c_str()))
     {
@@ -182,7 +206,26 @@ namespace ratio
         else
             assert(false);
     }
-    bool atom::is_active() const noexcept { return static_cast<z3solver &>(get_core()).mdl.eval(sigma, true).get_numeral_int() == 1; }
+    riddle::atom_state atom::get_state() const
+    {
+        switch (static_cast<z3solver &>(get_core()).mdl.eval(sigma, true).get_numeral_int())
+        {
+        case 0:
+            return riddle::atom_state::inactive;
+        case 1:
+            return riddle::atom_state::active;
+        case 2:
+            return riddle::atom_state::unified;
+        default:
+            assert(false);
+        }
+    }
+    json::json atom::to_json() const
+    {
+        json::json j = riddle::atom::to_json();
+        j["sigma"] = sigma.to_string();
+        return j;
+    }
 
     z3solver::z3solver(std::string_view name) : graph(name), slv(ctx), mdl(ctx)
     {
@@ -256,6 +299,8 @@ namespace ratio
     riddle::string_expr z3solver::new_string() { return std::make_shared<string_item>(static_cast<riddle::string_type &>(get_type(riddle::string_kw)), ctx.string_const(("s" + std::to_string(string_count++)).c_str())); }
     riddle::string_expr z3solver::new_string(std::string &&value) { return std::make_shared<string_item>(static_cast<riddle::string_type &>(get_type(riddle::string_kw)), ctx.string_val(value.c_str())); }
 
+    std::string z3solver::string_value(const riddle::string_item &expr) const noexcept { return mdl.eval(static_cast<const string_item &>(expr).get_expr(), true).to_string(); }
+
     riddle::enum_expr z3solver::new_enum(riddle::type &tp, std::vector<std::reference_wrapper<utils::enum_val>> &&values)
     {
         auto xpr = ctx.int_const(("e" + std::to_string(enum_count++)).c_str());

src/z3/z3types.cpp

@@ -21,7 +21,7 @@ namespace ratio
         std::unordered_map<const riddle::component *, std::map<utils::inf_rational, std::pair<std::vector<atom *>, std::vector<atom *>>>> sv_instances;
         for (const auto &[name, pred] : get_predicates())
             for (const auto &atm : pred->get_atoms())
-                if (static_cast<atom &>(*atm).is_active())
+                if (static_cast<atom &>(*atm).get_state() == riddle::atom_state::active)
                 {
                     auto &tau = static_cast<riddle::enum_item &>(*atm->get(riddle::tau_kw)); // the atom's tau variable..
                     auto &sv = static_cast<riddle::component &>(get_core().enum_value(tau)); // the tau variable's value..
@@ -69,7 +69,7 @@ namespace ratio
         std::unordered_map<riddle::component *, std::map<utils::inf_rational, std::pair<std::vector<atom *>, std::vector<atom *>>>> sv_instances;
         for (const auto &[name, pred] : get_predicates())
             for (const auto &atm : pred->get_atoms())
-                if (static_cast<atom &>(*atm).is_active())
+                if (static_cast<atom &>(*atm).get_state() == riddle::atom_state::active)
                 {
                     auto &tau = static_cast<riddle::enum_item &>(*atm->get(riddle::tau_kw)); // the atom's tau variable..
                     auto &sv = static_cast<riddle::component &>(get_core().enum_value(tau)); // the tau variable's value..