Update submodules in extern/riddle and extern/semitone

include/flaw.hpp

@@ -10,11 +10,12 @@
 namespace ratio
 {
   class solver;
+  class graph;
   class resolver;
 
   class flaw
   {
-    friend class solver;
+    friend class graph;
 
   public:
     flaw(solver &s, std::vector<std::reference_wrapper<resolver>> &&causes, const bool &exclusive = false) noexcept;

include/graph.hpp

@@ -4,38 +4,88 @@
 #include <vector>
 #include <deque>
 #include <memory>
+#include "solver.hpp"
 #include "flaw.hpp"
 #include "resolver.hpp"
 
 namespace ratio
 {
-  class graph
+  class graph : public semitone::theory
   {
-    friend class solver;
-
   public:
     graph(solver &slv) noexcept;
 
-  protected:
     /**
-     * @brief Adds the given flaw to the graph.
+     * @brief Creates a new flaw of the given type.
      *
-     * @param f The flaw to add.
-     * @param enqueue Whether to enqueue the flaw.
+     * @tparam Tp The type of the flaw to create.
+     * @tparam Args The types of the arguments to pass to the flaw
+     * @param args The arguments to pass to the flaw
+     * @return Tp& The created flaw
      */
-    void add_flaw(std::unique_ptr<flaw> &&f, bool enqueue = true) noexcept;
+    template <typename Tp, typename... Args>
+    Tp &new_flaw(Args &&...args) noexcept
+    {
+      static_assert(std::is_base_of_v<flaw, Tp>, "Tp must be a subclass of flaw");
+      auto f = new Tp(std::forward<Args>(args)...);
+      if (slv.get_sat().root_level())
+      {
+        f->init();
+        phis[variable(f->get_phi())].push_back(std::unique_ptr<flaw>(f));
+      }
+      else
+        pending_flaws.push_back(std::unique_ptr<flaw>(f));
+      return *f;
+    }
+
+    /**
+     * @brief Creates a new resolver of the given type.
+     *
+     * @tparam Tp The type of the resolver to create.
+     * @tparam Args The types of the arguments to pass to the resolver
+     * @param args The arguments to pass to the resolver
+     * @return Tp& The created resolver
+     */
+    template <typename Tp, typename... Args>
+    Tp &new_resolver(Args &&...args) noexcept
+    {
+      static_assert(std::is_base_of_v<resolver, Tp>, "Tp must be a subclass of resolver");
+      auto r = new Tp(std::forward<Args>(args)...);
+      rhos[r->get_rho()].push_back(std::unique_ptr<resolver>(r));
+      return *r;
+    }
+
+    const std::optional<std::reference_wrapper<resolver>> &get_current_resolver() const noexcept { return res; }
+
+  protected:
     /**
      * @brief Enqueues the given flaw in the graph.
      *
      * @param f The flaw to enqueue.
      */
     void enqueue(flaw &f) noexcept { flaw_q.push_back(f); }
 
+    /**
+     * @brief Expands the given flaw in the graph.
+     *
+     * @param f The flaw to expand.
+     */
+    void expand_flaw(flaw &f);
+
+  private:
+    bool propagate(const utils::lit &) noexcept override { return true; }
+    bool check() noexcept override { return true; }
+    void push() noexcept override {}
+    void pop() noexcept override {}
+
   private:
     solver &slv;                                                                    // the solver this graph belongs to..
     std::unordered_map<VARIABLE_TYPE, std::vector<std::unique_ptr<flaw>>> phis;     // the phi variables (propositional variable to flaws) of the flaws..
+    std::vector<std::unique_ptr<flaw>> pending_flaws;                               // pending flaws, waiting for root-level to be initialized..
     std::unordered_map<VARIABLE_TYPE, std::vector<std::unique_ptr<resolver>>> rhos; // the rho variables (propositional variable to resolver) of the resolvers..
+    std::optional<std::reference_wrapper<resolver>> res;                            // the current resolver..
     std::deque<std::reference_wrapper<flaw>> flaw_q;                                // the flaw queue (for the graph building procedure)..
+    std::unordered_set<flaw *> active_flaws;                                        // the currently active flaws..
     VARIABLE_TYPE gamma;                                                            // the variable representing the validity of this graph..
   };
 } // namespace ratio

include/resolver.hpp

@@ -42,6 +42,13 @@ namespace ratio
      */
     utils::rational get_estimated_cost() const noexcept;
 
+    /**
+     * Applies this resolver, introducing subgoals and/or constraints.
+     *
+     * @pre the solver must be at root-level.
+     */
+    virtual void apply() = 0;
+
   private:
     flaw &f;                                                 // the flaw solved by this resolver..
     const utils::lit rho;                                    // the propositional literal indicating whether the resolver is active or not..

include/solver.hpp

@@ -2,15 +2,16 @@
 
 #include <unordered_set>
 #include "core.hpp"
+#include "sat_core.hpp"
 #include "lra_theory.hpp"
 #include "idl_theory.hpp"
 #include "rdl_theory.hpp"
 #include "ov_theory.hpp"
-#include "graph.hpp"
 
 namespace ratio
 {
   class atom_flaw;
+  class graph;
 
   class atom : public riddle::atom
   {
@@ -25,10 +26,8 @@ namespace ratio
     atom_flaw &reason; // the flaw associated to this atom..
   };
 
-  class solver : public riddle::core, public semitone::theory
+  class solver : public riddle::core
   {
-    friend class graph;
-
   public:
     solver(const std::string &name = "oRatio") noexcept;
     virtual ~solver() = default;
@@ -54,6 +53,8 @@ namespace ratio
      */
     void take_decision(const utils::lit &d);
 
+    [[nodiscard]] semitone::sat_core &get_sat() noexcept { return *sat; }
+    [[nodiscard]] const semitone::sat_core &get_sat() const noexcept { return *sat; }
     [[nodiscard]] semitone::lra_theory &get_lra_theory() noexcept { return lra; }
     [[nodiscard]] const semitone::lra_theory &get_lra_theory() const noexcept { return lra; }
     [[nodiscard]] semitone::idl_theory &get_idl_theory() noexcept { return idl; }
@@ -62,6 +63,8 @@ namespace ratio
     [[nodiscard]] const semitone::rdl_theory &get_rdl_theory() const noexcept { return rdl; }
     [[nodiscard]] semitone::ov_theory &get_ov_theory() noexcept { return ov; }
     [[nodiscard]] const semitone::ov_theory &get_ov_theory() const noexcept { return ov; }
+    [[nodiscard]] graph &get_graph() noexcept { return gr; }
+    [[nodiscard]] const graph &get_graph() const noexcept { return gr; }
 
     [[nodiscard]] std::shared_ptr<riddle::bool_item> new_bool() noexcept override;
     [[nodiscard]] std::shared_ptr<riddle::arith_item> new_int() noexcept override;
@@ -103,35 +106,12 @@ namespace ratio
     [[nodiscard]] std::shared_ptr<riddle::item> get(riddle::enum_item &enm, const std::string &name) noexcept override;
 
   private:
-    bool propagate(const utils::lit &) noexcept override { return true; }
-    bool check() noexcept override { return true; }
-    void push() noexcept override {}
-    void pop() noexcept override {}
-
-  private:
-    /**
-     * @brief Adds a new flaw to the solver.
-     *
-     * @param f The flaw to add.
-     * @param enqueue Whether to enqueue the flaw.
-     */
-    void new_flaw(std::unique_ptr<flaw> f, const bool &enqueue = true);
-    /**
-     * @brief Expands the given flaw in the graph.
-     *
-     * @param f The flaw to expand.
-     */
-    void expand_flaw(flaw &f) noexcept;
-
-  private:
-    const std::string name;                           // the name of the solver
-    semitone::lra_theory lra;                         // the linear real arithmetic theory
-    semitone::idl_theory idl;                         // the integer difference logic theory
-    semitone::rdl_theory rdl;                         // the real difference logic theory
-    semitone::ov_theory ov;                           // the object variable theory
-    graph gr;                                         // the causal graph
-    std::optional<resolver> res;                      // the current resolver
-    std::unordered_set<flaw *> active_flaws;          // the currently active flaws..
-    std::vector<std::unique_ptr<flaw>> pending_flaws; // pending flaws, waiting for root-level to be initialized..
+    const std::string name;                  // the name of the solver
+    std::shared_ptr<semitone::sat_core> sat; // the SAT core
+    semitone::lra_theory &lra;               // the linear real arithmetic theory
+    semitone::idl_theory &idl;               // the integer difference logic theory
+    semitone::rdl_theory &rdl;               // the real difference logic theory
+    semitone::ov_theory &ov;                 // the object variable theory
+    graph &gr;                               // the causal graph
   };
 } // namespace ratio

src/flaw.cpp

@@ -1,8 +1,8 @@
 #include <algorithm>
 #include <cassert>
 #include "flaw.hpp"
+#include "resolver.hpp"
 #include "solver.hpp"
-#include "sat_core.hpp"
 
 namespace ratio
 {

src/graph.cpp

@@ -1,18 +1,46 @@
 #include "graph.hpp"
-#include "solver.hpp"
+#include "logging.hpp"
+#include <cassert>
 
 namespace ratio
 {
     graph::graph(solver &slv) noexcept : slv(slv) {}
 
-    void graph::add_flaw(std::unique_ptr<flaw> &&f, bool enqueue) noexcept
+    void graph::expand_flaw(flaw &f)
     {
-        auto &phi = phis[variable(f->get_phi())];
-        phi.push_back(std::move(f));
+        assert(!f.expanded);
 
-        if (enqueue)
-            this->enqueue(*phi.back());
-        else
-            slv.expand_flaw(*phi.back());
+        LOG_TRACE("[" << slv.get_name() << "] Expanding flaw");
+        // we expand the flaw..
+        f.expand();
+
+        // we apply the flaw's resolvers..
+        for (const auto &r : f.resolvers)
+        {
+            LOG_TRACE("[" << slv.get_name() << "] Applying resolver");
+            res = r;
+            try
+            {
+                r.get().apply();
+            }
+            catch (const std::exception &e)
+            { // the resolver is inapplicable..
+                if (!sat->new_clause({!r.get().get_rho()}))
+                    throw riddle::unsolvable_exception();
+            }
+            res = std::nullopt;
+        }
+
+        switch (sat->value(f.get_phi()))
+        {
+        case utils::True: // we have a top-level (a landmark) flaw..
+            if (std::none_of(f.get_resolvers().begin(), f.get_resolvers().end(), [this](const auto &r)
+                             { return sat->value(r.get().get_rho()) == utils::True; }))
+                active_flaws.insert(&f); // the flaw has not yet already been solved (e.g. it has a single resolver)..
+            break;
+        case utils::Undefined:           // we do not have a top-level (a landmark) flaw, nor an infeasible one..
+            bind(variable(f.get_phi())); // we listen for the flaw to become active..
+            break;
+        }
     }
 } // namespace ratio

src/resolver.cpp

@@ -6,9 +6,8 @@
 #include <algorithm>
 #endif
 #include "resolver.hpp"
-#include "solver.hpp"
 #include "flaw.hpp"
-#include "sat_core.hpp"
+#include "solver.hpp"
 
 namespace ratio
 {

src/solver.cpp

@@ -1,9 +1,9 @@
 #include <cassert>
 #include <algorithm>
 #include "solver.hpp"
+#include "graph.hpp"
 #include "init.hpp"
 #include "smart_type.hpp"
-#include "sat_core.hpp"
 #include "atom_flaw.hpp"
 #include "bool_flaw.hpp"
 #include "logging.hpp"
@@ -12,7 +12,7 @@ namespace ratio
 {
     atom::atom(riddle::predicate &p, bool is_fact, atom_flaw &reason, std::map<std::string, std::shared_ptr<item>> &&args) : riddle::atom(p, is_fact, utils::lit(static_cast<solver &>(p.get_scope().get_core()).get_sat().new_var()), std::move(args)), reason(reason) {}
 
-    solver::solver(const std::string &name) noexcept : theory(std::make_shared<semitone::sat_core>()), name(name), lra(get_sat_ptr()), idl(get_sat_ptr()), rdl(get_sat_ptr()), ov(get_sat_ptr()), gr(*this) {}
+    solver::solver(const std::string &name) noexcept : name(name), sat(std::make_shared<semitone::sat_core>()), lra(sat->new_theory<semitone::lra_theory>()), idl(sat->new_theory<semitone::idl_theory>()), rdl(sat->new_theory<semitone::rdl_theory>()), ov(sat->new_theory<semitone::ov_theory>()), gr(sat->new_theory<graph>(*this)) {}
 
     void solver::init() noexcept
     {
@@ -58,7 +58,7 @@ namespace ratio
     std::shared_ptr<riddle::bool_item> solver::new_bool() noexcept
     {
         auto b = std::make_shared<riddle::bool_item>(get_bool_type(), utils::lit(sat->new_var()));
-        new_flaw(std::make_unique<bool_flaw>(*this, std::vector<std::reference_wrapper<resolver>>(), b));
+        gr.new_flaw<bool_flaw>(*this, std::vector<std::reference_wrapper<resolver>>(), b);
         return b;
     }
     std::shared_ptr<riddle::arith_item> solver::new_int() noexcept { return std::make_shared<riddle::arith_item>(get_int_type(), utils::lin(lra.new_var(), utils::rational::one)); }
@@ -285,7 +285,7 @@ namespace ratio
 
     void solver::assert_fact(const std::shared_ptr<riddle::bool_item> &fact)
     {
-        if (!sat->new_clause({res.has_value() ? !res.value().get_rho() : utils::FALSE_lit, fact->get_value()}))
+        if (!sat->new_clause({gr.get_current_resolver().has_value() ? !gr.get_current_resolver().value().get().get_rho() : utils::FALSE_lit, fact->get_value()}))
             throw riddle::unsolvable_exception();
     }
 
@@ -297,9 +297,8 @@ namespace ratio
     std::shared_ptr<riddle::atom> solver::new_atom(bool is_fact, riddle::predicate &pred, std::map<std::string, std::shared_ptr<riddle::item>> &&arguments) noexcept
     {
         LOG_TRACE("Creating new atom " << pred.get_name());
-        auto f = std::make_unique<atom_flaw>(*this, std::vector<std::reference_wrapper<resolver>>(), is_fact, pred, std::move(arguments));
-        auto atm = f->get_atom();
-        new_flaw(std::move(f));
+        auto &f = gr.new_flaw<atom_flaw>(*this, std::vector<std::reference_wrapper<resolver>>(), is_fact, pred, std::move(arguments));
+        auto atm = f.get_atom();
         // we check if we need to notify any smart types of the new goal..
         if (!is_core(atm->get_type().get_scope()))
         {
@@ -354,44 +353,5 @@ namespace ratio
             throw riddle::unsolvable_exception();
     }
 
-    void solver::new_flaw(std::unique_ptr<flaw> f, const bool &enqueue)
-    {
-        LOG_TRACE("[" << name << "] Creating new flaw");
-        if (!sat->root_level())
-        { // we postpone the flaw's initialization..
-            pending_flaws.push_back(std::move(f));
-            return;
-        }
-
-        // we initialize the flaw..
-        f->init();
-        LOG_TRACE("[" << name << "] Flaw initialized with φ: " << to_string(f->get_phi()));
-
-        switch (sat->value(f->get_phi()))
-        {
-        case utils::True: // we have a top-level (a landmark) flaw..
-            if (enqueue || std::none_of(f->get_resolvers().begin(), f->get_resolvers().end(), [this](const auto &r)
-                                        { return sat->value(r.get().get_rho()) == utils::True; }))
-                active_flaws.insert(f.get()); // the flaw has not yet already been solved (e.g. it has a single resolver)..
-            break;
-        case utils::Undefined:            // we do not have a top-level (a landmark) flaw, nor an infeasible one..
-            bind(variable(f->get_phi())); // we listen for the flaw to become active..
-            break;
-        }
-
-        // we add the flaw to the graph..
-        gr.add_flaw(std::move(f), enqueue);
-    }
-
-    void solver::expand_flaw(flaw &f) noexcept
-    {
-        assert(!f.expanded);
-
-        LOG_TRACE("[" << name << "] Expanding flaw");
-        // we expand the flaw..
-        f.expand();
-        LOG_TRACE("[" << name << "] Flaw expanded");
-    }
-
     std::shared_ptr<riddle::item> solver::get(riddle::enum_item &enm, const std::string &name) noexcept { return enm.get(name); }
 } // namespace ratio