Refactor local search solver and flaws: enhance flaw handling, introduce new resolver classes, and update solver methods for improved functionality

Author: riccardodebenedictis

extern/linspire

@@ -8,17 +8,24 @@ namespace ratio
   class ls_flaw : public riddle::flaw
   {
   public:
-    ls_flaw(solver &cr, std::vector<std::shared_ptr<riddle::resolver>> &&causes, const utils::lit &phi);
+    ls_flaw(solver &cr, std::vector<std::shared_ptr<riddle::resolver>> &&causes);
 
     const utils::lit &get_phi() const noexcept { return phi; }
 
+    utils::rational get_estimated_cost() const noexcept override;
+
+  private:
+    utils::lit get_phi(const std::vector<std::shared_ptr<riddle::resolver>> &causes) const noexcept;
+
   private:
     const utils::lit phi;
+    utils::rational est_cost = utils::rational::positive_infinite; // the estimated cost of this flaw..
   };
 
   class ls_resolver : public resolver
   {
   public:
+    ls_resolver(ls_flaw &flw, utils::rational &&intrinsic_cost);
     ls_resolver(ls_flaw &flw, utils::rational &&intrinsic_cost, const utils::lit &rho);
 
     const utils::lit &get_rho() const noexcept { return rho; }
@@ -30,9 +37,7 @@ namespace ratio
   class enum_flaw final : public ls_flaw
   {
   public:
-    enum_flaw(solver &slv, std::vector<std::shared_ptr<riddle::resolver>> &&causes, const utils::lit &phi, riddle::component_type &tp, std::vector<riddle::expr> &&values, utils::var ev) noexcept;
-
-    utils::rational get_estimated_cost() const noexcept override;
+    enum_flaw(solver &slv, std::vector<std::shared_ptr<riddle::resolver>> &&causes, riddle::component_type &tp, std::vector<riddle::expr> &&values, utils::var ev) noexcept;
 
     [[nodiscard]] const riddle::enum_expr &get_var() const noexcept { return var; }
 
@@ -57,9 +62,7 @@ namespace ratio
   class clause_flaw final : public ls_flaw
   {
   public:
-    clause_flaw(solver &slv, std::vector<std::shared_ptr<riddle::resolver>> &&causes, const utils::lit &phi, std::vector<riddle::bool_expr> &&clause) noexcept;
-
-    utils::rational get_estimated_cost() const noexcept override;
+    clause_flaw(solver &slv, std::vector<std::shared_ptr<riddle::resolver>> &&causes, std::vector<riddle::bool_expr> &&clause) noexcept;
 
     [[nodiscard]] const std::vector<riddle::bool_expr> &get_clause() const noexcept { return clause; }
 
@@ -72,12 +75,24 @@ namespace ratio
     std::vector<riddle::bool_expr> clause;
   };
 
-  class disjunction_flaw final : public ls_flaw
+  class choose_lit final : public ls_resolver
   {
   public:
-    disjunction_flaw(solver &slv, std::vector<std::shared_ptr<riddle::resolver>> &&causes, const utils::lit &phi, std::vector<std::unique_ptr<riddle::conjunction>> &&disjuncts) noexcept;
+    choose_lit(clause_flaw &f, riddle::bool_expr lit) noexcept;
 
-    utils::rational get_estimated_cost() const noexcept override;
+  private:
+    bool apply() noexcept override;
+
+    [[nodiscard]] json::json to_json() const override;
+
+  private:
+    riddle::bool_expr lit; // the literal to choose..
+  };
+
+  class disjunction_flaw final : public ls_flaw
+  {
+  public:
+    disjunction_flaw(solver &slv, std::vector<std::shared_ptr<riddle::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; }
 
@@ -89,4 +104,133 @@ namespace ratio
   private:
     std::vector<std::unique_ptr<riddle::conjunction>> disjuncts;
   };
+
+  class choose_conjunction final : public ls_resolver
+  {
+  public:
+    choose_conjunction(disjunction_flaw &f, riddle::conjunction &conj) noexcept;
+
+  private:
+    bool apply() noexcept override;
+
+    [[nodiscard]] json::json to_json() const override;
+
+  private:
+    riddle::conjunction &conj;
+  };
+
+  class atom_flaw final : public ls_flaw
+  {
+  public:
+    atom_flaw(solver &slv, std::vector<std::shared_ptr<riddle::resolver>> &&causes, bool is_fact, riddle::predicate &pred, std::map<std::string, riddle::expr, std::less<>> &&args, riddle::bool_expr &&sigma) noexcept;
+
+    [[nodiscard]] const riddle::atom_expr &get_atom() const noexcept { return atm; }
+
+  private:
+    void compute_resolvers() override;
+
+    [[nodiscard]] json::json to_json() const override;
+
+  private:
+    riddle::atom_expr atm;
+  };
+
+  class activate_fact final : public ls_resolver
+  {
+  public:
+    activate_fact(atom_flaw &f) noexcept;
+
+  private:
+    bool apply() noexcept override;
+
+    json::json to_json() const override;
+  };
+
+  class activate_goal final : public ls_resolver
+  {
+  public:
+    activate_goal(atom_flaw &f) noexcept;
+
+  private:
+    bool apply() noexcept override;
+
+    json::json to_json() const override;
+  };
+
+  class unify_atom final : public ls_resolver
+  {
+  public:
+    unify_atom(atom_flaw &f, riddle::atom_expr atm) noexcept;
+
+  private:
+    bool apply() noexcept override;
+
+    json::json to_json() const override;
+
+  private:
+    riddle::atom_expr atm; // the atom to unify with..
+  };
+
+  class sv_peak final : public ls_flaw
+  {
+  public:
+    sv_peak(solver &slv, std::vector<riddle::atom_expr> &&atms) noexcept;
+
+  private:
+    void compute_resolvers() noexcept override;
+
+  private:
+    std::vector<riddle::atom_expr> atms;
+  };
+
+  class rr_peak final : public ls_flaw
+  {
+  public:
+    rr_peak(solver &slv, std::vector<riddle::atom_expr> &&atms) noexcept;
+
+  private:
+    void compute_resolvers() noexcept override;
+
+  private:
+    std::vector<riddle::atom_expr> atms;
+  };
+
+  class cr_overproduction final : public ls_flaw
+  {
+  public:
+    cr_overproduction(solver &slv, std::vector<riddle::atom_expr> &&prod_atms, std::vector<riddle::atom_expr> &&cons_atms) noexcept;
+
+  private:
+    void compute_resolvers() noexcept override;
+
+  private:
+    std::vector<riddle::atom_expr> prod_atms;
+    std::vector<riddle::atom_expr> cons_atms;
+  };
+
+  class cr_overconsumption final : public ls_flaw
+  {
+  public:
+    cr_overconsumption(solver &slv, std::vector<riddle::atom_expr> &&cons_atms, std::vector<riddle::atom_expr> &&prod_atms) noexcept;
+
+  private:
+    void compute_resolvers() noexcept override;
+
+  private:
+    std::vector<riddle::atom_expr> cons_atms;
+    std::vector<riddle::atom_expr> prod_atms;
+  };
+
+  class ordering final : public ls_resolver
+  {
+  public:
+    ordering(ls_flaw &flw, riddle::atom_expr before, riddle::atom_expr after) noexcept;
+
+  private:
+    bool apply() noexcept override;
+
+  private:
+    riddle::atom_expr before;
+    riddle::atom_expr after;
+  };
 } // namespace ratio

extern/riddle

@@ -6,18 +6,20 @@
 namespace ratio
 {
   class ls_flaw;
+  class ls_resolver;
 
   class local_search_solver : public solver
   {
     friend class ls_flaw;
+    friend class ls_resolver;
 
   public:
     local_search_solver() noexcept;
 
     [[nodiscard]] riddle::expr new_enum(riddle::component_type &tp, std::vector<riddle::expr> &&values) override;
 
-    void new_disjunction(std::vector<std::unique_ptr<riddle::conjunction>> &&) override;
-    void new_clause(std::vector<riddle::bool_expr> &&) override;
+    void new_disjunction(std::vector<std::unique_ptr<riddle::conjunction>> &&disjuncts) override;
+    void new_clause(std::vector<riddle::bool_expr> &&exprs) override;
 
     void solve() override;
 
@@ -26,6 +28,9 @@ namespace ratio
   private:
     riddle::atom_expr create_atom(bool is_fact, riddle::predicate &pred, std::map<std::string, std::shared_ptr<riddle::term>, std::less<>> &&args) override;
 
+    void new_clause(std::vector<utils::lit> &&lits);
+    utils::lbool sat_val(const utils::lit &l) const noexcept;
+
 #ifdef ORATIO_ENABLE_LISTENERS
   private:
     /**

include/local_search/local_search_flaws.hpp

@@ -154,7 +154,7 @@ namespace ratio
         return j;
     }
 
-    unify_atom::unify_atom(atom_flaw &flw, riddle::atom_expr atm) noexcept : riddle::resolver(flw, utils::rational(1)), resolver(flw, utils::rational(2)), atm(std::move(atm)) {}
+    unify_atom::unify_atom(atom_flaw &flw, riddle::atom_expr atm) noexcept : riddle::resolver(flw, utils::rational(0)), resolver(flw, utils::rational(0)), atm(std::move(atm)) {}
     bool unify_atom::apply() noexcept
     {
         if (!ratio::resolver::get_flaw().get_core().assert_expr(static_cast<riddle::atom &>(*atm).get_sigma()))

include/local_search/local_search_solver.hpp

@@ -173,6 +173,16 @@ namespace ratio
         }
     }
 
+    void basic_solver::new_disjunction(std::vector<std::unique_ptr<riddle::conjunction>> &&disjuncts)
+    {
+        assert(disjuncts.size() > 1);
+        std::vector<std::shared_ptr<riddle::resolver>> causes;
+        if (!static_cast<node &>(get_current_node()).resolvers.empty())
+            causes.push_back(static_cast<node &>(get_current_node()).resolvers.back());
+        auto df = new_flaw<disjunction_flaw>(*this, std::move(causes), std::move(disjuncts));
+        FLAW_CREATED(*df);
+        static_cast<node &>(get_current_node()).open_flaws.insert(df);
+    }
     void basic_solver::new_clause(std::vector<riddle::bool_expr> &&exprs)
     {
         assert(!exprs.empty());
@@ -191,16 +201,6 @@ namespace ratio
             static_cast<node &>(get_current_node()).open_flaws.insert(cf);
         }
     }
-    void basic_solver::new_disjunction(std::vector<std::unique_ptr<riddle::conjunction>> &&disjuncts)
-    {
-        assert(disjuncts.size() > 1);
-        std::vector<std::shared_ptr<riddle::resolver>> causes;
-        if (!static_cast<node &>(get_current_node()).resolvers.empty())
-            causes.push_back(static_cast<node &>(get_current_node()).resolvers.back());
-        auto df = new_flaw<disjunction_flaw>(*this, std::move(causes), std::move(disjuncts));
-        FLAW_CREATED(*df);
-        static_cast<node &>(get_current_node()).open_flaws.insert(df);
-    }
 
     void basic_solver::solve()
     {