From 07f84f4fb21a5b6475ab4684f28fa8ef7fccdf21 Mon Sep 17 00:00:00 2001
From: Riccardo De Benedictis <riccardo.debenedictis@cnr.it>
Date: Sat, 4 Jan 2025 19:01:04 +0100
Subject: [PATCH] Add z3disjunction_flaw class and enhance z3solver with new
 disjunction handling

---
 include/graph.hpp      |  3 +++
 include/z3/z3flaws.hpp | 14 ++++++++++++++
 src/z3/z3flaws.cpp     |  7 +++++++
 src/z3/z3solver.cpp    |  6 +++++-
 4 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/include/graph.hpp b/include/graph.hpp
index 782e55a..4edcaff 100644
--- a/include/graph.hpp
+++ b/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
diff --git a/include/z3/z3flaws.hpp b/include/z3/z3flaws.hpp
index 9576396..80f887e 100644
--- a/include/z3/z3flaws.hpp
+++ b/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
diff --git a/src/z3/z3flaws.cpp b/src/z3/z3flaws.cpp
index 13a9072..38cc7b1 100644
--- a/src/z3/z3flaws.cpp
+++ b/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
\ No newline at end of file
diff --git a/src/z3/z3solver.cpp b/src/z3/z3solver.cpp
index 58f8f19..80e741e 100644
--- a/src/z3/z3solver.cpp
+++ b/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;
     }