core opt

src/opt/maxcore.cpp

@@ -510,6 +510,7 @@ public:
         for (auto const & [core, w] : cores) {
             if (core.empty())
                 return l_false;
+            ++m_stats.m_num_cores;
             remove_soft(core, m_asms);
             split_core(core);
             process_unsat(core, w);

src/opt/maxsmt.cpp

@@ -342,16 +342,14 @@ namespace opt {
 
     void maxsmt::updt_params(params_ref& p) {
         m_params.append(p);
-        if (m_msolver) {
+        if (m_msolver) 
             m_msolver->updt_params(p);
     }
-    }
 
     void maxsmt::collect_statistics(statistics& st) const {
-        if (m_msolver) {
+        if (m_msolver) 
             m_msolver->collect_statistics(st);
     }
-    }
 
     solver& maxsmt::s() {
         return m_c.get_solver(); 

src/opt/opt_context.cpp

@@ -1533,21 +1533,17 @@ namespace opt {
     }
 
     void context::collect_statistics(statistics& stats) const {
-        if (m_solver) {
+        if (m_solver) 
             m_solver->collect_statistics(stats);
-        }
+        if (m_simplify) 
-        if (m_simplify) {
             m_simplify->collect_statistics(stats);        
-        }
+        for (auto const& kv : m_maxsmts) 
-        for (auto const& kv : m_maxsmts) {
             kv.m_value->collect_statistics(stats);
-        }        
         get_memory_statistics(stats);
         get_rlimit_statistics(m.limit(), stats);
-        if (m_qmax) {
+        if (m_qmax) 
             m_qmax->collect_statistics(stats);
     }
-    }
 
     void context::collect_param_descrs(param_descrs & r) {
         opt_params::collect_param_descrs(r);

src/opt/opt_preprocess.cpp

@@ -15,6 +15,19 @@ Author:
 
     Nikolaj Bjorner (nbjorner) 2022-04-11
 
+
+Notes:
+
+   maxsat x, y, z, u . x + y + z <= 1 and F 
+=>
+   maxsst x or y or z, u . x + y + z <= 1 and F
+   lower bound increased by 2
+
+   maxsat x, y, z, u . x + y + z >= 2 and F 
+=>
+   maxsst x and y and z, u . x + y + z >= 2 and F
+   lower bound decreased by 2
+
 --*/
 
 #pragma once
@@ -113,10 +126,25 @@ namespace opt {
             m_trail.push_back(sf.s);
             if (new_soft.contains(sf.s))
                 new_soft[sf.s] += sf.weight;
-            else
+            else {
                 new_soft.insert(sf.s, sf.weight);
                 fmls.push_back(sf.s);
             }
+        }
+        return new_soft;
+    }
+
+    obj_map<expr, rational> preprocess::dualize(obj_map<expr, rational> const& soft, expr_ref_vector& fmls) {
+        obj_map<expr, rational> new_soft;
+        for (auto const& [k, v] : soft) {
+            expr* nk = mk_not(m, k);
+            m_trail.push_back(nk);
+            new_soft.insert(nk, v);
+        }
+        unsigned i = 0;
+        for (expr* f : fmls)
+            fmls[i++] = mk_not(m, f);
+
         return new_soft;
     }
 
@@ -131,6 +159,24 @@ namespace opt {
             return false;
         for (auto& mux : mutexes) 
             process_mutex(mux, new_soft, lower);
+
+
+        if (mutexes.empty())
+        {
+            obj_map<expr, rational> dual_soft = dualize(new_soft, fmls);
+            mutexes.reset();
+            lbool is_sat = s.find_mutexes(fmls, mutexes);
+            if (is_sat == l_false)
+                return true;
+            if (is_sat == l_undef)
+                return false;
+            rational llower(0);
+            for (auto& mux : mutexes) 
+                process_mutex(mux, dual_soft, llower);
+            if (dual_soft.size() != new_soft.size())
+                new_soft = dualize(dual_soft, fmls);
+        }
+        
         softs.reset();
         for (auto const& [k, v] : new_soft)
             softs.push_back(soft(expr_ref(k, m), v, false));
@@ -183,6 +229,7 @@ namespace opt {
         SASSERT(sum1 == sum2);        
     }
 
+
     preprocess::preprocess(solver& s):  m(s.get_manager()), s(s), m_trail(m) {}
     
     bool preprocess::operator()(vector<soft>& soft, rational& lower) {

src/opt/opt_preprocess.h

@@ -34,6 +34,8 @@ namespace opt {
         bool prop_mutexes(vector<soft>& softs, rational& lower);
         void process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft, rational& lower);
 
+        obj_map<expr, rational> dualize(obj_map<expr, rational> const& soft, expr_ref_vector& fmls);
+
     public:
         preprocess(solver& s);
         bool operator()(vector<soft>& soft, rational& lower);

src/sat/sat_solver/inc_sat_solver.cpp

@@ -698,6 +698,33 @@ public:
 
 private:
 
+    lbool check_uninterpreted() {
+        func_decl_ref_vector funs(m);
+        m_goal2sat.get_interpreted_funs(funs);
+
+        if (!funs.empty()) {
+            m_has_uninterpreted = true;
+            std::stringstream strm;
+            strm << "(sat.giveup interpreted functions sent to SAT solver " << funs <<")";
+            TRACE("sat", tout << strm.str() << "\n";);
+            IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
+            set_reason_unknown(strm.str());
+            return l_undef;
+        }
+        return l_true;        
+    }
+
+    lbool internalize_goal(unsigned sz, expr* const* fmls) {
+        m_solver.pop_to_base_level();
+        if (m_solver.inconsistent()) 
+            return l_false;        
+        m_pc.reset();
+        m_goal2sat(m, sz, fmls, m_params, m_solver, m_map, m_dep2asm, is_incremental());
+        if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
+        m_sat_mc->flush_smc(m_solver, m_map);
+        return check_uninterpreted();
+    }
+
     lbool internalize_goal(goal_ref& g) {        
         m_solver.pop_to_base_level();
         if (m_solver.inconsistent()) 
@@ -712,12 +739,14 @@ private:
         }
         SASSERT(!g->proofs_enabled());
         TRACE("sat", m_solver.display(tout); g->display(tout););
+
         try {
             if (m_is_cnf) {
                 m_subgoals.push_back(g.get());
             }
             else {
                 (*m_preprocess)(g, m_subgoals);
+                m_is_cnf = true;
             }
         }
         catch (tactic_exception & ex) {
@@ -737,8 +766,8 @@ private:
             IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n");
             return l_undef;
         }
+        
         g = m_subgoals[0];
-        func_decl_ref_vector funs(m);
         m_pc = g->pc();
         m_mcs.set(m_mcs.size()-1, concat(m_mcs.back(), g->mc()));
         TRACE("sat", g->display_with_dependencies(tout););
@@ -746,19 +775,10 @@ private:
         // ensure that if goal is already internalized, then import mc from m_solver.
 
         m_goal2sat(*g, m_params, m_solver, m_map, m_dep2asm, is_incremental());
-        m_goal2sat.get_interpreted_funs(funs);
+
         if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
         m_sat_mc->flush_smc(m_solver, m_map);
-        if (!funs.empty()) {
+        return check_uninterpreted();
-            m_has_uninterpreted = true;
-            std::stringstream strm;
-            strm << "(sat.giveup interpreted functions sent to SAT solver " << funs <<")";
-            TRACE("sat", tout << strm.str() << "\n";);
-            IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
-            set_reason_unknown(strm.str());
-            return l_undef;
-        }
-        return l_true;
     }
 
     lbool internalize_assumptions(unsigned sz, expr* const* asms) {
@@ -766,17 +786,30 @@ private:
             m_asms.shrink(0);
             return l_true;
         }
+        for (unsigned i = 0; i < sz; ++i) 
+            m_is_cnf &= is_literal(asms[i]);
+        for (unsigned i = 0; i < get_num_assumptions(); ++i) 
+            m_is_cnf &= is_literal(get_assumption(i));
+
+        if (m_is_cnf) {
+            //            std::cout << "assumptions " << sz << " " << get_num_assumptions() << " " << m_fmls_head << " " <<  m_fmls.size() << "\n";
+            expr_ref_vector fmls(m);
+            fmls.append(sz, asms);
+            for (unsigned i = 0; i < get_num_assumptions(); ++i)
+                fmls.push_back(get_assumption(i));
+            m_goal2sat.assumptions(m, fmls.size(), fmls.data(), m_params, m_solver, m_map, m_dep2asm, is_incremental());
+            extract_assumptions(fmls.size(), fmls.data());
+            return l_true;
+        }
+
         goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
-        for (unsigned i = 0; i < sz; ++i) {
+        for (unsigned i = 0; i < sz; ++i) 
             g->assert_expr(asms[i], m.mk_leaf(asms[i]));
-        }
+        for (unsigned i = 0; i < get_num_assumptions(); ++i) 
-        for (unsigned i = 0; i < get_num_assumptions(); ++i) {
             g->assert_expr(get_assumption(i), m.mk_leaf(get_assumption(i)));
-        }
         lbool res = internalize_goal(g);
-        if (res == l_true) {
+        if (res == l_true) 
             extract_assumptions(sz, asms);
-        }
         return res;
     }
 
@@ -905,18 +938,25 @@ private:
     }
 
     lbool internalize_formulas() {
-        if (m_fmls_head == m_fmls.size()) {
+        if (m_fmls_head == m_fmls.size()) 
             return l_true;
+
+        lbool res;
+        
+        if (m_is_cnf) {
+            std::cout << "cnf\n";
+            res = internalize_goal(m_fmls.size() - m_fmls_head, m_fmls.data() + m_fmls_head);
         }
+        else {
             goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
             for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
                 expr* fml = m_fmls.get(i);
                 g->assert_expr(fml);
             }
-        lbool res = internalize_goal(g);
+            res = internalize_goal(g);
-        if (res != l_undef) {
-            m_fmls_head = m_fmls.size();
         }
+        if (res != l_undef) 
+            m_fmls_head = m_fmls.size();
         m_internalized_converted = false;
         return res;
     }

src/sat/tactic/goal2sat.cpp

@@ -894,7 +894,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_result_stack.pop_back();
     }
 
-    void operator()(goal const & g) {
     struct scoped_reset {
         imp& i;
         scoped_reset(imp& i) :i(i) {}
@@ -904,6 +903,27 @@ struct goal2sat::imp : public sat::sat_internalizer {
             i.m_lit2app.reset();
         }
     };
+    
+    void operator()(unsigned n, expr* const* fmls) {
+        scoped_reset _reset(*this);
+        // collect_boolean_interface(g, m_interface_vars);
+        for (unsigned i = 0; i < n; ++i) 
+            process(fmls[i]);
+    }
+
+    void assumptions(unsigned n, expr* const* fmls) {
+        scoped_reset _reset(*this);
+        // collect_boolean_interface(g, m_interface_vars);
+        for (unsigned i = 0; i < n; ++i) {
+            expr* f = fmls[i];
+            expr* f1 = f;
+            bool sign = m.is_not(f, f1);
+            insert_dep(f, f1, sign);
+        }
+    }
+
+
+    void operator()(goal const & g) {
         scoped_reset _reset(*this);
         collect_boolean_interface(g, m_interface_vars);
         unsigned size = g.size();
@@ -1002,16 +1022,30 @@ void goal2sat::collect_param_descrs(param_descrs & r) {
     r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas");
 }
 
-
+void goal2sat::init(ast_manager& m, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external) {
-void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
     if (!m_imp) {
-        m_imp = alloc(imp, g.m(), p, t, m, dep2asm, default_external);
+        m_imp = alloc(imp, m, p, t, map, dep2asm, default_external);
         for (unsigned i = 0; i < m_scopes; ++i)
             m_imp->user_push();
     }
+}
+
+void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
+    init(g.m(), p, t, m, dep2asm, default_external);
     (*m_imp)(g);    
 }
 
+void goal2sat::operator()(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external) {
+    init(m, p, t, map, dep2asm, default_external);
+    (*m_imp)(n, fmls);
+}
+
+void goal2sat::assumptions(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external) {
+    init(m, p, t, map, dep2asm, default_external);
+    m_imp->assumptions(n, fmls);
+}
+
+
 void goal2sat::get_interpreted_funs(func_decl_ref_vector& funs) {
     if (m_imp) 
         funs.append(m_imp->interpreted_funs());

src/sat/tactic/goal2sat.h

@@ -34,15 +34,19 @@ Notes:
 #include "sat/smt/sat_internalizer.h"
 
 class goal2sat {
+public:
+    typedef obj_map<expr, sat::literal> dep2asm_map;
+private:
     struct imp;
     imp *  m_imp;
-    unsigned m_scopes { 0 };
+    unsigned m_scopes = 0;
+
+    void init(ast_manager& m, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external);
 
 public:
     goal2sat();
     ~goal2sat();
 
-    typedef obj_map<expr, sat::literal> dep2asm_map;
 
     static void collect_param_descrs(param_descrs & r);
 
@@ -60,6 +64,10 @@ public:
     */
     void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
 
+    void operator()(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external = false);
+
+    void assumptions(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external = false);
+
     void get_interpreted_funs(func_decl_ref_vector& funs);
 
     bool has_interpreted_funs() const;