cube and clause

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

src/smt/smt_clause.cpp

@@ -28,7 +28,7 @@ namespace smt {
     clause * clause::mk(ast_manager & m, unsigned num_lits, literal * lits, clause_kind k, justification * js, 
                         clause_del_eh * del_eh, bool save_atoms, expr * const * bool_var2expr_map) {
         SASSERT(k == CLS_AUX || js == 0 || !js->in_region());
-        SASSERT(num_lits >= 2);
+        SASSERT(num_lits > 2);
         unsigned sz                = get_obj_size(num_lits, k, save_atoms, del_eh != nullptr, js != nullptr);
         void * mem                 = m.get_allocator().allocate(sz);
         clause * cls               = new (mem) clause();

src/smt/smt_context.cpp

@@ -1815,7 +1815,7 @@ namespace smt {
     */
     bool context::decide() {
 
-        if (m_clause && at_search_level()) {
+        if (at_search_level() && !m_clause_lits.empty()) {
             switch (decide_clause()) {
             case l_true:  // already satisfied
                 break;
@@ -3137,17 +3137,19 @@ namespace smt {
 
     void context::init_clause(expr_ref_vector const& clause) {
         if (m_clause) del_clause(m_clause);
+        m_clause = nullptr;
         m_clause_lits.reset();
         for (expr* lit : clause) {
             internalize_formula(lit, true);
             mark_as_relevant(lit);
             m_clause_lits.push_back(get_literal(lit));
         }
-        m_clause = mk_clause(m_clause_lits.size(), m_clause_lits.c_ptr(), nullptr);
+        if (m_clause_lits.size() > 2) 
+            m_clause = clause::mk(m_manager, m_clause_lits.size(), m_clause_lits.c_ptr(), CLS_AUX);
     }
 
     lbool context::decide_clause() {
-        if (!m_clause) return l_true;
+        if (m_clause_lits.empty()) return l_true;
         shuffle(m_clause_lits.size(), m_clause_lits.c_ptr(), m_random);
         for (literal l : m_clause_lits) {
             switch (get_assignment(l)) {
@@ -3162,20 +3164,38 @@ namespace smt {
             }            
         }
         for (unsigned i = m_assigned_literals.size(); i-- > 0; ) {
-            literal lit = m_assigned_literals[i];
+            literal nlit = ~m_assigned_literals[i];
-            if (m_clause_lits.contains(~lit)) {
+            if (m_clause_lits.contains(nlit)) {
-                for (unsigned j = 0, sz = m_clause->get_num_literals(); j < sz; ++j) {
+                switch (m_clause_lits.size()) {
-                    if (m_clause->get_literal(j) == ~lit) {
+                case 1: {
-                        if (j > 0) m_clause->swap_lits(j, 0);
+                    b_justification js;
-                        break;
+                    set_conflict(js, ~nlit);
+                    break;
+                } 
+                case 2: {
+                    if (nlit == m_clause_lits[1]) {
+                        std::swap(m_clause_lits[0], m_clause_lits[1]);
                     }
+                    b_justification js(~m_clause_lits[1]);
+                    set_conflict(js, ~nlit);
+                    break;
                 }
-                b_justification js(m_clause);
+                default: {
-                set_conflict(js, ~lit);
+                    for (unsigned j = 0, sz = m_clause->get_num_literals(); j < sz; ++j) {
-                return l_false;
+                        if (m_clause->get_literal(j) == nlit) {
+                            if (j > 0) m_clause->swap_lits(j, 0);
+                            break;
+                        }
+                    }
+                    b_justification js(m_clause);
+                    set_conflict(js, ~nlit);
+                    break;
+                }
+                }
+                break;
             }
         }
-        UNREACHABLE();
+        VERIFY(!resolve_conflict());
         return l_false;
     }
 
@@ -3280,6 +3300,7 @@ namespace smt {
         
         if (m_clause) del_clause(m_clause);
         m_clause = nullptr;
+        m_clause_lits.reset();
         m_unsat_core.reset();
         m_stats.m_num_checks++;
         pop_to_base_lvl();

src/solver/solver_pool.cpp

@@ -107,12 +107,35 @@ public:
         }
     }
 
+    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();
         scoped_watch _t_(m_pool.m_check_watch);
         m_pool.m_stats.m_num_checks++;
-
+        
         stopwatch sw;
         sw.start();
         internalize_assertions();

src/test/CMakeLists.txt

@@ -24,6 +24,7 @@ add_executable(test-z3
   chashtable.cpp
   check_assumptions.cpp
   cnf_backbones.cpp
+  cube_clause.cpp
   datalog_parser.cpp
   ddnf.cpp
   diff_logic.cpp

src/test/cube_clause.cpp

@@ -0,0 +1,58 @@
+#include "ast/reg_decl_plugins.h"
+#include "solver/solver_pool.h"
+#include "smt/smt_solver.h"
+
+
+void tst_cube_clause() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    params_ref p;
+    lbool r;
+    ref<solver> solver = mk_smt_solver(m, p, symbol::null);
+
+    expr_ref a(m.mk_const(symbol("a"), m.mk_bool_sort()), m);
+    expr_ref b(m.mk_const(symbol("b"), m.mk_bool_sort()), m);
+    expr_ref c(m.mk_const(symbol("c"), m.mk_bool_sort()), m);
+    expr_ref d(m.mk_const(symbol("d"), m.mk_bool_sort()), m);
+    expr_ref e(m.mk_const(symbol("e"), m.mk_bool_sort()), m);
+    expr_ref f(m.mk_const(symbol("f"), m.mk_bool_sort()), m);
+    expr_ref g(m.mk_const(symbol("g"), m.mk_bool_sort()), m);
+    expr_ref fml(m);
+    fml = m.mk_not(m.mk_and(a, b));
+    solver->assert_expr(fml);
+    fml = m.mk_not(m.mk_and(c, d));
+    solver->assert_expr(fml);
+    fml = m.mk_not(m.mk_and(e, f));
+    solver->assert_expr(fml);
+    expr_ref_vector cube(m), clause(m), core(m);
+    r = solver->check_sat(cube);
+    std::cout << r << "\n";
+    cube.push_back(a);
+    r = solver->check_sat(cube);
+    std::cout << r << "\n";
+    cube.push_back(c);
+    cube.push_back(e);
+    r = solver->check_sat(cube);
+    std::cout << r << "\n";
+    clause.push_back(b);
+    r = solver->check_sat(cube, clause);
+    std::cout << r << "\n";
+    core.reset();
+    solver->get_unsat_core(core);
+    std::cout << core << "\n";
+    clause.push_back(d);
+    r = solver->check_sat(cube, clause);
+    std::cout << r << "\n";
+    core.reset();
+    solver->get_unsat_core(core);
+    std::cout << core << "\n";
+    clause.push_back(f);
+    r = solver->check_sat(cube, clause);
+    std::cout << r << "\n";
+    core.reset();
+    solver->get_unsat_core(core);
+    std::cout << core << "\n";
+    clause.push_back(g);
+    r = solver->check_sat(cube, clause);
+    std::cout << r << "\n";
+}

src/test/main.cpp

@@ -172,6 +172,7 @@ int main(int argc, char ** argv) {
     TST(var_subst);
     TST(simple_parser);
     TST(api);
+    TST(cube_clause);
     TST(old_interval);
     TST(get_implied_equalities);
     TST(arith_simplifier_plugin);