From 005a6d93bb84eddedf2580c9820c163757d32bc8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 May 2018 11:29:36 -0700 Subject: [PATCH] cube and clause Signed-off-by: Nikolaj Bjorner --- src/smt/smt_clause.cpp | 2 +- src/smt/smt_context.cpp | 47 +++++++++++++++++++++--------- src/solver/solver_pool.cpp | 25 +++++++++++++++- src/test/CMakeLists.txt | 1 + src/test/cube_clause.cpp | 58 ++++++++++++++++++++++++++++++++++++++ src/test/main.cpp | 1 + 6 files changed, 119 insertions(+), 15 deletions(-) create mode 100644 src/test/cube_clause.cpp diff --git a/src/smt/smt_clause.cpp b/src/smt/smt_clause.cpp index a9365fffc..4266ab246 100644 --- a/src/smt/smt_clause.cpp +++ b/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(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4210039b0..ab7e4fa35 100644 --- a/src/smt/smt_context.cpp +++ b/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]; - if (m_clause_lits.contains(~lit)) { - for (unsigned j = 0, sz = m_clause->get_num_literals(); j < sz; ++j) { - if (m_clause->get_literal(j) == ~lit) { - if (j > 0) m_clause->swap_lits(j, 0); - break; + literal nlit = ~m_assigned_literals[i]; + if (m_clause_lits.contains(nlit)) { + switch (m_clause_lits.size()) { + case 1: { + b_justification js; + 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); - set_conflict(js, ~lit); - return l_false; + default: { + for (unsigned j = 0, sz = m_clause->get_num_literals(); j < sz; ++j) { + 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(); diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 0aee5c3dc..dbad0999e 100644 --- a/src/solver/solver_pool.cpp +++ b/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(); diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index da4194a2c..1dc0290d8 100644 --- a/src/test/CMakeLists.txt +++ b/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 diff --git a/src/test/cube_clause.cpp b/src/test/cube_clause.cpp new file mode 100644 index 000000000..f625789e4 --- /dev/null +++ b/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 = 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"; +} diff --git a/src/test/main.cpp b/src/test/main.cpp index c1f169a3a..41f051f24 100644 --- a/src/test/main.cpp +++ b/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);