add totalizer version of rc2

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/opt/maxcore.cpp

@@ -13,6 +13,7 @@ Abstract:
     - mus-mss:    based on dual refinement of bounds.
     - binary:     binary version of maxres
     - rc2:        implementaion of rc2 heuristic using cardinality constraints
+    - rc2t:       implementaion of rc2 heuristic using totalizerx
     - rc2-binary: hybrid of rc2 and binary maxres. Perform one step of binary maxres. 
                   If there are more than 16 soft constraints create a cardinality constraint.
 
@@ -60,6 +61,7 @@ Notes:
 #include "ast/ast_pp.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/ast_util.h"
+#include "ast/ast_smt_pp.h"
 #include "model/model_smt2_pp.h"
 #include "solver/solver.h"
 #include "solver/mus.h"
@@ -71,6 +73,8 @@ Notes:
 #include "opt/opt_cores.h"
 #include "opt/maxsmt.h"
 #include "opt/maxcore.h"
+#include "opt/totalizer.h"
+#include <iostream>
 
 using namespace opt;
 
@@ -81,6 +85,7 @@ public:
         s_primal_dual,
         s_primal_binary,
         s_rc2,
+        s_rc2tot,
         s_primal_binary_rc2
     };
 private:
@@ -160,6 +165,9 @@ public:
         case s_rc2:
             m_trace_id = "rc2";
             break;
+        case s_rc2tot:
+            m_trace_id = "rc2tot";
+            break;
         case s_primal_binary_rc2:
             m_trace_id = "rc2bin";
             break;
@@ -366,6 +374,7 @@ public:
         case s_primal:
         case s_primal_binary:
         case s_rc2:
+        case s_rc2tot:
         case s_primal_binary_rc2:
             return mus_solver();
         case s_primal_dual:
@@ -558,6 +567,7 @@ public:
             bin_max_resolve(core, w);
             break;
         case strategy_t::s_rc2:
+        case strategy_t::s_rc2tot:
             max_resolve_rc2(core, w);
             break;
         case strategy_t::s_primal_binary_rc2:
@@ -780,8 +790,38 @@ public:
     obj_map<expr, expr*>      m_at_mostk;
     obj_map<expr, bound_info> m_bounds;
     rational                  m_unfold_upper;
+    obj_map<expr, totalizer*> m_totalizers;
+
+    expr* mk_atmost_tot(expr_ref_vector const& es, unsigned bound, rational const& weight) {
+        pb_util pb(m);
+        expr_ref am(pb.mk_at_most_k(es, 0), m);
+        totalizer* t = nullptr;        
+        if (!m_totalizers.find(am, t)) {
+            m_trail.push_back(am);
+            t = alloc(totalizer, es);
+            m_totalizers.insert(am, t);
+        }
+        expr* at_least = t->at_least(bound + 1);
+        am = m.mk_not(at_least);
+        m_trail.push_back(am);
+        expr_ref_vector& clauses = t->clauses();
+        for (auto & clause : clauses) {
+            add(clause);
+            m_defs.push_back(clause);
+        }
+        clauses.reset();
+        auto& defs = t->defs();
+        for (auto & [v, d] : defs) 
+            update_model(v, d);
+        defs.reset();
+        bound_info b(es, bound, weight);
+        m_bounds.insert(am, b);
+        return am;
+    }
 
     expr* mk_atmost(expr_ref_vector const& es, unsigned bound, rational const& weight) {
+        if (m_st == strategy_t::s_rc2tot)
+            return mk_atmost_tot(es, bound, weight);
         pb_util pb(m);
         expr_ref am(pb.mk_at_most_k(es, bound), m);
         expr* r = nullptr;
@@ -1040,6 +1080,9 @@ public:
         m_unfold_upper = 0;
         m_at_mostk.reset();
         m_bounds.reset();
+        for (auto& [k,t] : m_totalizers)
+            dealloc(t);
+        m_totalizers.reset();
         return l_true;
     }
 
@@ -1109,6 +1152,11 @@ opt::maxsmt_solver_base* opt::mk_rc2(
     return alloc(maxcore, c, id, soft, maxcore::s_rc2);
 }
 
+opt::maxsmt_solver_base* opt::mk_rc2tot(
+    maxsat_context& c, unsigned id, vector<soft>& soft) {
+    return alloc(maxcore, c, id, soft, maxcore::s_rc2tot);
+}
+
 opt::maxsmt_solver_base* opt::mk_rc2bin(
     maxsat_context& c, unsigned id, vector<soft>& soft) {
     return alloc(maxcore, c, id, soft, maxcore::s_primal_binary_rc2);

src/opt/maxcore.h

@@ -23,6 +23,8 @@ namespace opt {
 
     maxsmt_solver_base* mk_rc2(maxsat_context& c, unsigned id, vector<soft>& soft);
 
+    maxsmt_solver_base* mk_rc2tot(maxsat_context& c, unsigned id, vector<soft>& soft);
+
     maxsmt_solver_base* mk_rc2bin(maxsat_context& c, unsigned id, vector<soft>& soft);
 
     maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);

src/opt/maxsmt.cpp

@@ -193,6 +193,8 @@ namespace opt {
             m_msolver = mk_maxres_binary(m_c, m_index, m_soft);
         else if (maxsat_engine == symbol("rc2"))             
             m_msolver = mk_rc2(m_c, m_index, m_soft);
+        else if (maxsat_engine == symbol("rc2tot"))             
+            m_msolver = mk_rc2tot(m_c, m_index, m_soft);
         else if (maxsat_engine == symbol("rc2bin"))             
             m_msolver = mk_rc2bin(m_c, m_index, m_soft);
         else if (maxsat_engine == symbol("pd-maxres"))             

src/opt/opt_context.cpp

@@ -705,6 +705,8 @@ namespace opt {
 
         if (m_maxsat_engine != symbol("maxres") &&
             m_maxsat_engine != symbol("rc2") &&
+            m_maxsat_engine != symbol("rc2tot") &&
+            m_maxsat_engine != symbol("rc2bin") &&
             m_maxsat_engine != symbol("maxres-bin") &&
             m_maxsat_engine != symbol("maxres-bin-delay") &&
             m_maxsat_engine != symbol("pd-maxres") &&

src/opt/totalizer.cpp

@@ -34,13 +34,15 @@ namespace opt {
         if (r)
             ensure_bound(r, k);
 
+        expr_ref c(m), def(m);
+        expr_ref_vector ors(m), clause(m);
         for (unsigned i = k; i > 0 && !lits.get(i - 1); --i) {
             if (l->m_literals.size() + r->m_literals.size() < i) {
                 lits[i - 1] = m.mk_false();
                 continue;
             }
 
-            expr* c = m.mk_fresh_const("c", m.mk_bool_sort());
+            c = m.mk_fresh_const("c", m.mk_bool_sort());
             lits[i - 1] = c;
 
             // >= 3
@@ -49,13 +51,15 @@ namespace opt {
             // l[1] & r[0] => >= 3
             // l[2] => >= 3
 
+            ors.reset();
+
             for (unsigned j1 = 0; j1 <= i; ++j1) {
                 unsigned j2 = i - j1;
                 if (j1 > l->m_literals.size())
                     continue;
                 if (j2 > r->m_literals.size())
                     continue;
-                expr_ref_vector clause(m);
+                clause.reset();
                 if (0 < j1) {
                     expr* a = l->m_literals.get(j1 - 1);
                     clause.push_back(mk_not(m, a));
@@ -66,16 +70,19 @@ namespace opt {
                 }
                 if (clause.empty())
                     continue;
+                ors.push_back(mk_or(clause));
                 clause.push_back(c);
-                m_clauses.push_back(clause);
+                m_clauses.push_back(mk_or(clause));
             }
+            def = mk_not(m, mk_and(ors));
+            m_defs.push_back(std::make_pair(c, def));            
         }
     }
 
     totalizer::totalizer(expr_ref_vector const& literals):
         m(literals.m()),
         m_literals(literals),
-        m_tree(nullptr) {
+        m_clauses(m) {
         ptr_vector<node> trees;
         for (expr* e : literals) {
             expr_ref_vector ls(m);

src/opt/totalizer.h

@@ -30,8 +30,9 @@ namespace opt {
 
         ast_manager&            m;
         expr_ref_vector         m_literals;
-        node*                   m_tree;
+        node*                   m_tree = nullptr;
-        vector<expr_ref_vector> m_clauses;
+        expr_ref_vector         m_clauses;
+        vector<std::pair<expr_ref, expr_ref>> m_defs;
 
         void ensure_bound(node* n, unsigned k);
 
@@ -39,6 +40,7 @@ namespace opt {
         totalizer(expr_ref_vector const& literals);
         ~totalizer();
         expr* at_least(unsigned k);
-        vector<expr_ref_vector>& clauses() { return m_clauses; }
+        expr_ref_vector& clauses() { return m_clauses; }
+        vector<std::pair<expr_ref, expr_ref>>& defs() { return m_defs; }
     };   
 }

src/test/totalizer.cpp

@@ -17,9 +17,6 @@ void tst_totalizer() {
         expr* am = tot.at_least(i);
         std::cout << mk_pp(am, m) << "\n";        
     }
-    for (auto& clause : tot.clauses()) {
+    for (auto& clause : tot.clauses()) 
-        for (auto * l : clause)
+        std::cout << clause << "\n";
-            std::cout << mk_pp(l, m) << " ";
-        std::cout << "\n";
-    }
 }