From 26339119e4dd23e4e9fbf0772b1c1422cffa75df Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 29 May 2018 13:16:30 -0700 Subject: [PATCH] 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 | 21 ++----------- src/solver/solver.cpp | 21 ------------- src/solver/solver.h | 5 ++- src/solver/solver_na2as.cpp | 6 ++++ src/solver/solver_na2as.h | 6 ++-- src/solver/solver_pool.cpp | 61 +++++++++++++++++++++---------------- 6 files changed, 50 insertions(+), 70 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 0f5338ba6..d715e4879 100644 --- a/src/smt/smt_solver.cpp +++ b/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 r = m_context.check(cube, clause); - switch (r) { - case l_false: - if (pr) *pr = get_proof(); - if (core) { - ptr_vector _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; + lbool check_sat_cc_core(expr_ref_vector const& cube, expr_ref_vector const& clause) override { + return m_context.check(cube, clause); } struct scoped_minimize_core { diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index d295427e4..84b5eb588 100644 --- a/src/solver/solver.cpp +++ b/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"); } diff --git a/src/solver/solver.h b/src/solver/solver.h index 59a61b3c7..3d9befdbc 100644 --- a/src/solver/solver.h +++ b/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. diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index f98e08cdb..ac241b4a2 100644 --- a/src/solver/solver_na2as.cpp +++ b/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); diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h index 75fb27189..a3ed85a9a 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -36,19 +36,21 @@ public: void assert_expr_core2(expr * t, expr * a) override; // virtual void assert_expr_core(expr * t) = 0; - + // 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; - + unsigned get_num_assumptions() const override { return m_assumptions.size(); } expr * get_assumption(unsigned idx) const override { return m_assumptions[idx]; } lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override; lbool find_mutexes(expr_ref_vector const& vars, 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; }; diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 4b54639ec..8012dd129 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -107,37 +107,12 @@ 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(); scoped_watch _t_(m_pool.m_check_watch); m_pool.m_stats.m_num_checks++; - + stopwatch sw; sw.start(); internalize_assertions(); @@ -156,13 +131,45 @@ public: 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; } + 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) {