Added functions for computing inconsistencies..

CMakeLists.txt

@@ -29,6 +29,7 @@ if(${HEURISTIC_TYPE_INDEX} EQUAL -1)
 endif()
 message(STATUS "Heuristic type: ${HEURISTIC_TYPE}")
 
+option(CHECK_INCONSISTENCIES "Check inconsistencies at each step" OFF)
 option(ENABLE_VISUALIZATION "Enable visualization features" OFF)
 
 add_library(oRatioLib src/solver.cpp src/graph.cpp src/flaw.cpp src/resolver.cpp src/smart_type.cpp src/flaws/atom_flaw.cpp src/flaws/bool_flaw.cpp src/flaws/disj_flaw.cpp src/flaws/disjunction_flaw.cpp src/flaws/enum_flaw.cpp src/types/agent.cpp src/types/state_variable.cpp src/types/consumable_resource.cpp src/types/reusable_resource.cpp)
@@ -54,6 +55,11 @@ elseif(${HEURISTIC_TYPE} STREQUAL "h2_add")
     target_compile_definitions(oRatioLib PRIVATE H2_ADD)
 endif()
 
+message(STATUS "Check inconsistencies at each step: ${CHECK_INCONSISTENCIES}")
+if(CHECK_INCONSISTENCIES)
+    target_compile_definitions(oRatioLib PRIVATE CHECK_INCONSISTENCIES)
+endif()
+
 message(STATUS "Enable oRatio visualization features: ${ENABLE_VISUALIZATION}")
 if(ENABLE_VISUALIZATION)
     target_compile_definitions(oRatioLib PRIVATE ENABLE_VISUALIZATION)

include/flaw.hpp

@@ -153,7 +153,18 @@ namespace ratio
 
   std::string to_state(const flaw &f) noexcept;
 
-  const json::json flaw_schema = {{"flaw", {{"type", "object"}, {"properties", {{"id", {{"type", "integer"}}}, {"causes", {{"type", "array"}, {"description", "The resolvers that caused this flaw."}, {"items", {{"type", "integer"}}}}}, {"state", {{"type", "string"}, {"enum", {"active", "forbidden", "inactive"}}}}, {"phi", {{"type", "string"}}}, {"cost", {{"$ref", "#/components/schemas/rational"}}}, {"pos", {{"type", "integer"}}}, {"data", {{"type", "object"}}}}}, {"required", {"id", "causes", "state", "pos", "phi", "cost"}}}}};
+  const json::json flaw_schema{
+      {"flaw",
+       {{"type", "object"},
+        {"properties",
+         {{"id", {{"type", "integer"}}},
+          {"causes", {{"type", "array"}, {"description", "The resolvers that caused this flaw."}, {"items", {{"type", "integer"}}}}},
+          {"state", {{"type", "string"}, {"enum", {"active", "forbidden", "inactive"}}}},
+          {"phi", {{"type", "string"}}},
+          {"cost", {{"$ref", "#/components/schemas/rational"}}},
+          {"pos", {{"type", "integer"}}},
+          {"data", {{"type", "object"}}}}},
+        {"required", {"id", "causes", "state", "pos", "phi", "cost"}}}}};
 #endif
 
   /**

include/graph.hpp

@@ -97,6 +97,31 @@ namespace ratio
       return res;
     }
 
+    /**
+     * Checks if the graph has any active flaws.
+     *
+     * @return true if there are active flaws, false otherwise.
+     */
+    bool has_active_flaws() const noexcept { return !active_flaws.empty(); }
+
+    /**
+     * @brief Checks if the graph has any flaws with infinite cost.
+     *
+     * If the graph has flaws with infinite cost, it is impossible to resolve them.
+     *
+     * @return true if the graph has flaws with infinite cost, false otherwise.
+     */
+    bool has_infinite_cost_active_flaws() const noexcept;
+
+    /**
+     * @brief Returns the most expensive flaw.
+     *
+     * This function returns a reference to the most expensive flaw in the graph. The most expensive flaw is the best candidate to be resolved next.
+     *
+     * @return A reference to the most expensive flaw.
+     */
+    flaw &get_most_expensive_flaw() const noexcept;
+
     /**
      * @brief Get the current resolver.
      *
@@ -141,6 +166,32 @@ namespace ratio
      */
     void add_layer();
 
+    /**
+     * @brief Solves inconsistencies in the system.
+     *
+     * This function is responsible for resolving any inconsistencies that may exist in the system.
+     */
+    void solve_inconsistencies();
+
+    /**
+     * @brief Get the current inconsistencies of the solver.
+     *
+     * This function returns the current inconsistencies of the solver.
+     * The inconsistencies are represented as a vector of vectors of pairs of literals and doubles.
+     * Each vector of pairs represents a possible decision which can be taken to resolve the inconsistency.
+     * The pairs represent the literals and the costs of the literals.
+     *
+     * @return std::vector<std::vector<std::pair<utils::lit, double>>> The current inconsistencies of the solver.
+     */
+    [[nodiscard]] std::vector<std::vector<std::pair<utils::lit, double>>> get_incs() const noexcept;
+
+    /**
+     * @brief Resets the smart types.
+     *
+     * This function resets the smart types used by the solver.
+     */
+    void reset_smart_types() noexcept;
+
   protected:
     /**
      * @brief Enqueues the given flaw in the graph.
@@ -194,6 +245,7 @@ namespace ratio
     utils::lit ni{utils::TRUE_lit};                                                 // the current controlling literal..
     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..
+    std::vector<smart_type *> smart_types;                                          // the smart-types..
     VARIABLE_TYPE gamma;                                                            // the variable representing the validity of this graph..
   };
 

include/smart_type.hpp

@@ -13,6 +13,7 @@
 namespace ratio
 {
   class solver;
+  class graph;
   class atom;
   class resolver;
 
@@ -23,6 +24,7 @@ namespace ratio
   class smart_type : public riddle::component_type
   {
     friend class solver;
+    friend class graph;
 
   public:
     /**

include/solver.hpp

@@ -20,6 +20,7 @@ namespace ratio
 {
   class atom_flaw;
   class graph;
+  class smart_type;
 #ifdef ENABLE_VISUALIZATION
   class flaw_listener;
   class resolver_listener;
@@ -69,6 +70,14 @@ namespace ratio
      */
     void take_decision(const utils::lit &d);
 
+    /**
+     * @brief Advances to the next step in the solver.
+     *
+     * This function is responsible for moving the solver to the next step in the computation.
+     * It performs any necessary calculations or updates to the solver's internal state.
+     */
+    void next();
+
     [[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; }

src/graph.cpp

@@ -1,4 +1,5 @@
 #include "graph.hpp"
+#include "smart_type.hpp"
 #include "logging.hpp"
 #include <cassert>
 
@@ -19,6 +20,19 @@ namespace ratio
             throw riddle::unsolvable_exception();
     }
 
+    bool graph::has_infinite_cost_active_flaws() const noexcept
+    {
+        return std::any_of(active_flaws.cbegin(), active_flaws.cend(), [](const auto &f)
+                           { return is_infinite(f->get_estimated_cost()); });
+    }
+
+    flaw &graph::get_most_expensive_flaw() const noexcept
+    {
+        assert(!active_flaws.empty());
+        return **std::max_element(active_flaws.cbegin(), active_flaws.cend(), [](const auto &lhs, const auto &rhs)
+                                  { return lhs->get_estimated_cost() < rhs->get_estimated_cost(); });
+    }
+
     void graph::build()
     {
         LOG_DEBUG("[" << slv.get_name() << "] Building the graph");
@@ -47,6 +61,103 @@ namespace ratio
         assert(get_sat().root_level());
     }
 
+    void graph::solve_inconsistencies()
+    {
+        LOG_DEBUG("[" << slv.get_name() << "] Solving inconsistencies");
+
+        auto incs = get_incs(); // all the current inconsistencies..
+        LOG_DEBUG("[" << slv.get_name() << "] Found " << incs.size() << " inconsistencies");
+
+        // we solve the inconsistencies..
+        while (!incs.empty())
+        {
+            if (const auto &uns_inc = std::find_if(incs.cbegin(), incs.cend(), [](const auto &v)
+                                                   { return v.empty(); });
+                uns_inc != incs.cend())
+            { // we have an unsolvable inconsistency..
+                LOG_DEBUG("[" << slv.get_name() << "] Unsatisfiable inconsistency");
+                slv.next(); // we move to the next state..
+            }
+            else if (const auto &inc = std::find_if(incs.cbegin(), incs.cend(), [](const auto &v)
+                                                    { return v.size() == 1; });
+                     inc != incs.cend())
+            { // we have a trivial inconsistency..
+                LOG_DEBUG("[" << slv.get_name() << "] Trivial inconsistency");
+                assert(get_sat().value(inc->front().first) == utils::Undefined);
+                // we can learn something from it..
+                std::vector<utils::lit> learnt;
+                learnt.push_back(inc->front().first);
+                for (const auto &l : get_sat().get_decisions())
+                    learnt.push_back(!l);
+                record(std::move(learnt));
+                if (!get_sat().propagate())
+                    throw riddle::unsolvable_exception();
+            }
+            else
+            { // we have a non-trivial inconsistency, so we have to take a decision..
+                std::vector<std::pair<utils::lit, double>> bst_inc;
+                double k_inv = std::numeric_limits<double>::infinity();
+                for (const auto &inc : incs)
+                {
+                    double bst_commit = std::numeric_limits<double>::infinity();
+                    for ([[maybe_unused]] const auto &[choice, commit] : inc)
+                        if (commit < bst_commit)
+                            bst_commit = commit;
+                    double c_k_inv = 0;
+                    for ([[maybe_unused]] const auto &[choice, commit] : inc)
+                        c_k_inv += 1l / (1l + (commit - bst_commit));
+                    if (c_k_inv < k_inv)
+                    {
+                        k_inv = c_k_inv;
+                        bst_inc = inc;
+                    }
+                }
+
+                // we select the best choice (i.e. the least committing one) from those available for the best flaw..
+                slv.take_decision(std::min_element(bst_inc.cbegin(), bst_inc.cend(), [](const auto &ch0, const auto &ch1)
+                                                   { return ch0.second < ch1.second; })
+                                      ->first);
+            }
+
+            incs = get_incs(); // we get the new inconsistencies..
+            LOG_DEBUG("[" << slv.get_name() << "] Found " << incs.size() << " inconsistencies");
+        }
+
+        LOG_DEBUG("[" << slv.get_name() << "] Inconsistencies solved");
+    }
+
+    std::vector<std::vector<std::pair<utils::lit, double>>> graph::get_incs() const noexcept
+    {
+        std::vector<std::vector<std::pair<utils::lit, double>>> incs;
+        for (const auto &st : smart_types)
+        {
+            auto st_incs = st->get_current_incs();
+            incs.insert(incs.end(), st_incs.begin(), st_incs.end());
+        }
+        return incs;
+    }
+
+    void graph::reset_smart_types() noexcept
+    {
+        // we reset the smart types..
+        smart_types.clear();
+        // we seek for the existing smart types..
+        std::queue<riddle::component_type *> q;
+        for (const auto &t : slv.get_types())
+            if (auto ct = dynamic_cast<riddle::component_type *>(&t.get()))
+                q.push(ct);
+        while (!q.empty())
+        {
+            auto ct = q.front();
+            q.pop();
+            if (const auto st = dynamic_cast<smart_type *>(ct); st)
+                smart_types.emplace_back(st);
+            for (const auto &t : ct->get_types())
+                if (auto c_ct = dynamic_cast<riddle::component_type *>(&t.get()))
+                    q.push(c_ct);
+        }
+    }
+
     void graph::expand_flaw(flaw &f)
     {
         assert(!f.expanded);

src/resolver.cpp

@@ -56,7 +56,7 @@ namespace ratio
             return "active";
         case utils::False:
             return "forbidden";
-        case utils::Undefined:
+        default:
             return "inactive";
         }
     }

src/solver.cpp

@@ -15,8 +15,12 @@
 
 #ifdef ENABLE_VISUALIZATION
 #define STATE_CHANGED() state_changed()
+#define CURRENT_FLAW(f) current_flaw(f)
+#define CURRENT_RESOLVER(r) current_resolver(r)
 #else
 #define STATE_CHANGED()
+#define CURRENT_FLAW(f)
+#define CURRENT_RESOLVER(r)
 #endif
 
 namespace ratio
@@ -46,8 +50,10 @@ namespace ratio
         LOG_DEBUG("[" << name << "] Reading script: " << script);
         core::read(script);
 
-        if (!sat.propagate())
+        if (!sat.propagate()) // we propagate the constraints..
             throw riddle::unsolvable_exception();
+        gr.reset_smart_types(); // we reset the smart types..
+
         STATE_CHANGED();
     }
 
@@ -56,14 +62,58 @@ namespace ratio
         LOG_DEBUG("[" << name << "] Reading problem files");
         core::read(files);
 
-        if (!sat.propagate())
+        if (!sat.propagate()) // we propagate the constraints..
             throw riddle::unsolvable_exception();
+        gr.reset_smart_types(); // we reset the smart types..
+
         STATE_CHANGED();
     }
 
     bool solver::solve()
     {
         LOG_DEBUG("[" << name << "] Solving problem");
+        gr.build();
+#ifdef CHECK_INCONSISTENCIES
+        // we solve all the current inconsistencies..
+        solve_inconsistencies();
+
+        while (gr.has_active_flaws())
+        {
+            while (gr.has_infinite_cost_active_flaws())
+                next(); // we move to the next state..
+
+            auto &f = gr.get_most_expensive_flaw(); // we get the most expensive flaw..
+            CURRENT_FLAW(f);
+            auto &r = f.get_best_resolver(); // we get the best resolver for the flaw..
+            CURRENT_RESOLVER(r);
+
+            // we take the decision by activating the best resolver..
+            take_decision(r.get_rho());
+
+            // we solve all the current inconsistencies..
+            solve_inconsistencies();
+        }
+#else
+        do
+        {
+            while (gr.has_active_flaws())
+            {
+                while (gr.has_infinite_cost_active_flaws())
+                    next(); // we move to the next state..
+
+                auto &f = gr.get_most_expensive_flaw(); // we get the most expensive flaw..
+                CURRENT_FLAW(f);
+                auto &r = f.get_best_resolver(); // we get the best resolver for the flaw..
+                CURRENT_RESOLVER(r);
+
+                // we take the decision by activating the best resolver..
+                take_decision(r.get_rho());
+            }
+            // we solve all the current inconsistencies..
+            gr.solve_inconsistencies();
+        } while (gr.has_active_flaws());
+#endif
+        LOG_DEBUG("[" << name << "] Problem solved");
         return true;
     }
 
@@ -78,6 +128,18 @@ namespace ratio
         STATE_CHANGED();
     }
 
+    void solver::next()
+    {
+        LOG_DEBUG("[" << name << "] Next..");
+        if (!sat.next())
+            throw riddle::unsolvable_exception();
+
+        if (sat.root_level())
+            gr.build(); // we make sure the graph is built..
+
+        STATE_CHANGED();
+    }
+
     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()));