Add z3disjunction_flaw class and enhance z3solver with new disjunctio…

…n handling

include/graph.hpp

@@ -1,6 +1,7 @@
 #pragma once
 
 #include "core.hpp"
+#include <deque>
 
 #ifdef ENABLE_API
 #define NEW_FLAW(f) flaw_created(f)
@@ -90,6 +91,7 @@ namespace ratio
       auto f = new Tp(std::forward<Args>(args)...);
       NEW_FLAW(*f);
       flaws.emplace_back(std::unique_ptr<flaw>(f));
+      flaw_q.push_back(*f);
       return *f;
     }
 
@@ -206,5 +208,6 @@ namespace ratio
     std::vector<std::unique_ptr<resolver>> resolvers;      // The set of resolvers
     std::optional<std::reference_wrapper<flaw>> c_flaw;    // the current flaw..
     std::optional<std::reference_wrapper<resolver>> c_res; // the current resolver..
+    std::deque<std::reference_wrapper<flaw>> flaw_q;       // the flaw queue (for the graph building procedure)..
   };
 } // namespace ratio

include/z3/z3flaws.hpp

@@ -46,4 +46,18 @@ namespace ratio
   private:
     riddle::atom_expr atom;
   };
+
+  class z3disjunction_flaw : public z3flaw
+  {
+  public:
+    z3disjunction_flaw(z3solver &slv, std::vector<std::reference_wrapper<resolver>> &&causes, std::vector<std::unique_ptr<riddle::conjunction>> &&disjuncts) noexcept;
+
+    [[nodiscard]] const std::vector<std::unique_ptr<riddle::conjunction>> &get_disjuncts() const noexcept { return disjuncts; }
+
+  private:
+    void compute_resolvers() override;
+
+  private:
+    std::vector<std::unique_ptr<riddle::conjunction>> disjuncts;
+  };
 } // namespace ratio

src/z3/z3flaws.cpp

@@ -1,4 +1,5 @@
 #include "z3flaws.hpp"
+#include "conjunction.hpp"
 
 namespace ratio
 {
@@ -19,4 +20,10 @@ namespace ratio
     void z3atom_flaw::compute_resolvers()
     {
     }
+
+    z3disjunction_flaw::z3disjunction_flaw(z3solver &slv, std::vector<std::reference_wrapper<resolver>> &&causes, std::vector<std::unique_ptr<riddle::conjunction>> &&disjuncts) noexcept : z3flaw(slv, std::move(causes)), disjuncts(std::move(disjuncts)) {}
+
+    void z3disjunction_flaw::compute_resolvers()
+    {
+    }
 } // namespace ratio

src/z3/z3solver.cpp

@@ -296,6 +296,10 @@ namespace ratio
 
     void z3solver::new_disjunction(std::vector<std::unique_ptr<riddle::conjunction>> &&disjuncts)
     {
+        std::vector<std::reference_wrapper<resolver>> causes;
+        if (get_current_resolver().has_value())
+            causes.push_back(get_current_resolver().value());
+        new_flaw<z3disjunction_flaw>(*this, std::move(causes), std::move(disjuncts));
     }
     void z3solver::assert_fact(riddle::bool_expr fact)
     {
@@ -314,7 +318,7 @@ namespace ratio
         std::vector<std::reference_wrapper<resolver>> causes;
         if (get_current_resolver().has_value())
             causes.push_back(get_current_resolver().value());
-        auto &f = new_flaw<z3atom_flaw>(*this, std::move(causes), atm);
+        new_flaw<z3atom_flaw>(*this, std::move(causes), atm);
         return atm;
     }