solver::check_sat_cc : check_sat assuming cube and clause

Extends check_sat with an ability to assume a single clause in
addition to assuming a cube of assumptions

src/smt/smt_solver.cpp

@@ -190,26 +190,9 @@ namespace smt {
             return m_context.check(num_assumptions, assumptions);
         }
 
-        using solver_na2as::check_sat;
 
-        lbool check_sat(expr_ref_vector const& cube, expr_ref_vector const& clause, model_ref* mdl, expr_ref_vector* core, proof_ref* pr) override {
+        lbool check_sat_cc_core(expr_ref_vector const& cube, expr_ref_vector const& clause) override {
-            lbool r = m_context.check(cube, clause);
+            return m_context.check(cube, clause);
-            switch (r) {
-            case l_false:
-                if (pr) *pr = get_proof();
-                if (core) {
-                    ptr_vector<expr> _core;
-                    get_unsat_core(_core);
-                    core->append(_core.size(), _core.c_ptr());
-                }
-                break;
-            case l_true:
-                if (mdl) get_model(*mdl);
-                break;
-            default:
-                break;
-            }
-            return r;
         }
 
         struct scoped_minimize_core {

src/solver/solver.cpp

@@ -202,27 +202,6 @@ void solver::assert_expr(expr* f, expr* t) {
     assert_expr_core2(fml, a);    
 }
 
-lbool solver::check_sat(expr_ref_vector const& cube, expr_ref_vector const& clause, model_ref* mdl, expr_ref_vector* core, proof_ref* pr) {
-    ast_manager& m = clause.get_manager();
-    scoped_push _push(*this);
-    expr_ref disj = mk_or(clause);
-    assert_expr(disj);
-    lbool r = check_sat(cube);
-    switch (r) {
-    case l_false: 
-        if (core) get_unsat_core(*core);
-        if (pr) *pr = get_proof();
-        break;
-    case l_true: 
-        if (mdl) get_model(*mdl);
-        break;
-    default:
-        break;
-    }
-    return r;
-}
-
-
 void solver::collect_param_descrs(param_descrs & r) {
     r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: false) enforce model conversion when asserting formulas");
 }

src/solver/solver.h

@@ -152,7 +152,10 @@ public:
        The cube corresponds to auxiliary assumptions. The clause as an auxiliary disjunction that is also
        assumed for the check.
     */
-    virtual lbool check_sat(expr_ref_vector const& cube, expr_ref_vector const& clause, model_ref* mdl = nullptr, expr_ref_vector* core = nullptr, proof_ref* pr = nullptr);
+    virtual lbool check_sat_cc(expr_ref_vector const& cube, expr_ref_vector const& clause) {
+        if (clause.empty()) return check_sat(cube.size(), cube.c_ptr());
+        NOT_IMPLEMENTED_YET();
+    }
 
     /**
        \brief Set a progress callback procedure that is invoked by this solver during check_sat.

src/solver/solver_na2as.cpp

@@ -67,6 +67,12 @@ lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptio
     return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr());
 }
 
+lbool solver_na2as::check_sat_cc(const expr_ref_vector &assumptions, const expr_ref_vector &clause) {
+    if (clause.empty()) return check_sat(assumptions.size(), assumptions.c_ptr());
+    append_assumptions app(m_assumptions, assumptions.size(), assumptions.c_ptr());
+    return check_sat_cc_core(m_assumptions, clause);
+}
+
 lbool solver_na2as::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
     append_assumptions app(m_assumptions, asms.size(), asms.c_ptr());
     return get_consequences_core(m_assumptions, vars, consequences);

src/solver/solver_na2as.h

@@ -39,6 +39,7 @@ public:
 
     // Subclasses of solver_na2as should redefine the following *_core methods instead of these ones.
     lbool check_sat(unsigned num_assumptions, expr * const * assumptions) override;
+    lbool check_sat_cc(const expr_ref_vector &assumptions, const expr_ref_vector &clause) override;
     void push() override;
     void pop(unsigned n) override;
     unsigned get_scope_level() const override;
@@ -49,6 +50,7 @@ public:
     lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override;
 protected:
     virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0;
+    virtual lbool check_sat_cc_core(const expr_ref_vector &assumptions, const expr_ref_vector &clause) {NOT_IMPLEMENTED_YET();}
     virtual void push_core() = 0;
     virtual void pop_core(unsigned n) = 0;
 };

src/solver/solver_pool.cpp

@@ -107,31 +107,6 @@ public:
         }
     }
 
-    using solver_na2as::check_sat;
-
-    lbool check_sat(expr_ref_vector const& cube, expr_ref_vector const& clause, model_ref* mdl, expr_ref_vector* core, proof_ref* pr) override {
-        SASSERT(!m_pushed || get_scope_level() > 0);
-        m_proof.reset();
-        internalize_assertions();
-        expr_ref_vector cube1(cube);
-        cube1.push_back(m_pred);
-        lbool res = m_base->check_sat(cube1, clause, mdl, core, pr);
-        switch (res) {
-        case l_true:
-            m_pool.m_stats.m_num_sat_checks++;
-            break;
-        case l_undef:
-            m_pool.m_stats.m_num_undef_checks++;
-            break;
-        default:
-            break;
-        }
-        set_status(res);
-        
-        return res;
-    }
-
-    // NSB: seems we would add m_pred as an assumption?
     lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override {
         SASSERT(!m_pushed || get_scope_level() > 0);
         m_proof.reset();
@@ -163,6 +138,38 @@ public:
         return res;
     }
 
+    lbool check_sat_cc_core(const expr_ref_vector &cube,
+                            const expr_ref_vector &clause) override {
+        SASSERT(!m_pushed || get_scope_level() > 0);
+        m_proof.reset();
+        scoped_watch _t_(m_pool.m_check_watch);
+        m_pool.m_stats.m_num_checks++;
+
+        stopwatch sw;
+        sw.start();
+        internalize_assertions();
+        lbool res = m_base->check_sat_cc(cube, clause);
+        sw.stop();
+        switch (res) {
+        case l_true:
+            m_pool.m_check_sat_watch.add(sw);
+            m_pool.m_stats.m_num_sat_checks++;
+            break;
+        case l_undef:
+            m_pool.m_check_undef_watch.add(sw);
+            m_pool.m_stats.m_num_undef_checks++;
+            break;
+        default:
+            break;
+        }
+        set_status(res);
+
+        // if (false /*m_dump_benchmarks && sw.get_seconds() >= m_pool.fparams().m_dump_min_time*/) {
+        //     dump_benchmark(num_assumptions, assumptions, res, sw);
+        // }
+        return res;
+    }
+
     void push_core() override {
         SASSERT(!m_pushed || get_scope_level() > 0);
         if (m_in_delayed_scope) {