From ce592d77160e956a824ba8d4668b3174203ef96c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Jun 2017 19:44:02 -0700 Subject: [PATCH] add facility to add lemmas Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 10 ++++++++++ src/api/dotnet/Solver.cs | 15 +++++++++++++++ src/api/z3_api.h | 10 ++++++++++ src/opt/opt_solver.h | 1 + src/sat/sat_solver.cpp | 14 +++++++------- src/sat/sat_solver.h | 8 ++++---- src/sat/sat_solver/inc_sat_solver.cpp | 18 ++++++++++++++---- src/sat/tactic/goal2sat.cpp | 15 ++++++++++----- src/sat/tactic/goal2sat.h | 3 ++- src/smt/smt_solver.cpp | 4 ++++ src/solver/combined_solver.cpp | 6 ++++++ src/solver/solver.h | 6 ++++++ src/solver/tactic2solver.cpp | 4 ++++ src/tactic/portfolio/bounded_int2bv_solver.cpp | 4 ++++ src/tactic/portfolio/enum2bv_solver.cpp | 10 ++++++++++ src/tactic/portfolio/pb2bv_solver.cpp | 4 ++++ 16 files changed, 111 insertions(+), 21 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 09e522db2..0d6383970 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -258,6 +258,16 @@ extern "C" { to_solver_ref(s)->assert_expr(to_expr(a), to_expr(p)); Z3_CATCH; } + + void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a) { + Z3_TRY; + LOG_Z3_solver_assert_lemma(c, s, a); + RESET_ERROR_CODE(); + init_solver(c, s); + CHECK_FORMULA(a,); + to_solver_ref(s)->assert_lemma(to_expr(a)); + Z3_CATCH; + } Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s) { Z3_TRY; diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 078f5bc7a..d2c63ecce 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -181,6 +181,21 @@ namespace Microsoft.Z3 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject); } + /// + /// Assert a lemma (or multiple) into the solver. + /// + public void AssertLemma(params BoolExpr[] constraints) + { + Contract.Requires(constraints != null); + Contract.Requires(Contract.ForAll(constraints, c => c != null)); + + Context.CheckContextMatch(constraints); + foreach (BoolExpr a in constraints) + { + Native.Z3_solver_assert_lemma(Context.nCtx, NativeObject, a.NativeObject); + } + } + /// /// The number of assertions in the solver. /// diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 317b32923..85d007e70 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5949,6 +5949,16 @@ extern "C" { */ void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p); + /** + \brief add a lemma. A lemma is a assumed to be a consequence of the current assertions. + Adding a lemma should therefore be a logical no-op. Solvers are free to ignore lemmas. + + \pre \c a must be a Boolean expression + + def_API('Z3_solver_assert_lemma', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST))) + */ + void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a); + /** \brief Return the set of asserted formulas on the solver. diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index cef270abc..1f15a44d0 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -92,6 +92,7 @@ namespace opt { virtual void collect_param_descrs(param_descrs & r); virtual void collect_statistics(statistics & st) const; virtual void assert_expr(expr * t); + virtual void assert_lemma(expr* t) {} virtual void push_core(); virtual void pop_core(unsigned n); virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 77a816660..36cf9b526 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -209,7 +209,7 @@ namespace sat { } } - void solver::mk_clause(unsigned num_lits, literal * lits) { + void solver::mk_clause(unsigned num_lits, literal * lits, bool learned) { m_model_is_current = false; DEBUG_CODE({ for (unsigned i = 0; i < num_lits; i++) @@ -217,24 +217,24 @@ namespace sat { }); if (m_user_scope_literals.empty()) { - mk_clause_core(num_lits, lits, false); + mk_clause_core(num_lits, lits, learned); } else { m_aux_literals.reset(); m_aux_literals.append(num_lits, lits); m_aux_literals.append(m_user_scope_literals); - mk_clause_core(m_aux_literals.size(), m_aux_literals.c_ptr(), false); + mk_clause_core(m_aux_literals.size(), m_aux_literals.c_ptr(), learned); } } - void solver::mk_clause(literal l1, literal l2) { + void solver::mk_clause(literal l1, literal l2, bool learned) { literal ls[2] = { l1, l2 }; - mk_clause(2, ls); + mk_clause(2, ls, learned); } - void solver::mk_clause(literal l1, literal l2, literal l3) { + void solver::mk_clause(literal l1, literal l2, literal l3, bool learned) { literal ls[3] = { l1, l2, l3 }; - mk_clause(3, ls); + mk_clause(3, ls, learned); } void solver::del_clause(clause& c) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index b6dffe511..9da445cad 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -203,10 +203,10 @@ namespace sat { // // ----------------------- bool_var mk_var(bool ext = false, bool dvar = true); - void mk_clause(literal_vector const& lits) { mk_clause(lits.size(), lits.c_ptr()); } - void mk_clause(unsigned num_lits, literal * lits); - void mk_clause(literal l1, literal l2); - void mk_clause(literal l1, literal l2, literal l3); + void mk_clause(literal_vector const& lits, bool learned = false) { mk_clause(lits.size(), lits.c_ptr(), learned); } + void mk_clause(unsigned num_lits, literal * lits, bool learned = false); + void mk_clause(literal l1, literal l2, bool learned = false); + void mk_clause(literal l1, literal l2, literal l3, bool learned = false); protected: void del_clause(clause & c); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 9d9c24b8f..4cff85510 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -241,6 +241,16 @@ public: assert_expr(t); } } + + virtual void assert_lemma(expr* e) { + dep2asm_t dep2asm; + goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled + for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) { + g->assert_expr(m_fmls[i].get()); + } + VERIFY(l_undef != internalize_goal(g, dep2asm, true)); + } + virtual ast_manager& get_manager() const { return m; } virtual void assert_expr(expr * t) { m_internalized = false; @@ -501,7 +511,7 @@ public: private: - lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) { + lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) { m_mc.reset(); m_pc.reset(); m_dep_core.reset(); @@ -527,7 +537,7 @@ private: g = m_subgoals[0]; expr_ref_vector atoms(m); TRACE("sat", g->display_with_dependencies(tout);); - m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true); + m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true, is_lemma); m_goal2sat.get_interpreted_atoms(atoms); if (!atoms.empty()) { std::stringstream strm; @@ -552,7 +562,7 @@ private: 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, dep2asm); + lbool res = internalize_goal(g, dep2asm, false); if (res == l_true) { extract_assumptions(sz, asms, dep2asm); } @@ -673,7 +683,7 @@ private: for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) { g->assert_expr(m_fmls[i].get()); } - lbool res = internalize_goal(g, dep2asm); + lbool res = internalize_goal(g, dep2asm, false); if (res != l_undef) { m_fmls_head = m_fmls.size(); } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index cb4a19e89..eb3bc9d3e 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -67,6 +67,7 @@ struct goal2sat::imp { expr_ref_vector m_interpreted_atoms; bool m_default_external; bool m_xor_solver; + bool m_is_lemma; imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external): m(_m), @@ -77,7 +78,8 @@ struct goal2sat::imp { m_dep2asm(dep2asm), m_trail(m), m_interpreted_atoms(m), - m_default_external(default_external) { + m_default_external(default_external), + m_is_lemma(false) { updt_params(p); m_true = sat::null_bool_var; } @@ -98,19 +100,21 @@ struct goal2sat::imp { m_solver.mk_clause(1, &l); } + void set_lemma_mode(bool f) { m_is_lemma = f; } + void mk_clause(sat::literal l1, sat::literal l2) { TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";); - m_solver.mk_clause(l1, l2); + m_solver.mk_clause(l1, l2, m_is_lemma); } void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) { TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";); - m_solver.mk_clause(l1, l2, l3); + m_solver.mk_clause(l1, l2, l3, m_is_lemma); } void mk_clause(unsigned num, sat::literal * lits) { TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";); - m_solver.mk_clause(num, lits); + m_solver.mk_clause(num, lits, m_is_lemma); } sat::bool_var mk_true() { @@ -863,9 +867,10 @@ struct goal2sat::scoped_set_imp { }; -void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) { +void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external, bool is_lemma) { imp proc(g.m(), p, t, m, dep2asm, default_external); scoped_set_imp set(this, &proc); + proc.set_lemma_mode(is_lemma); proc(g); dealloc(m_interpreted_atoms); m_interpreted_atoms = alloc(expr_ref_vector, g.m()); diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 5bfb28f60..9dfb5b24f 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -50,6 +50,7 @@ public: static bool has_unsupported_bool(goal const & s); + /** \brief "Compile" the goal into the given sat solver. Store a mapping from atoms to boolean variables into m. @@ -60,7 +61,7 @@ public: \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel), an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory). */ - void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false); + void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false, bool is_lemma = false); void get_interpreted_atoms(expr_ref_vector& atoms); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index ef81fbfd2..d7ecbfd50 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -116,6 +116,10 @@ namespace smt { m_name2assertion.insert(a, t); } + virtual void assert_lemma(expr* t) { + // no-op + } + virtual void push_core() { m_context.push(); } diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index b23aabc2d..c35a794e5 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -179,6 +179,12 @@ public: m_solver2->assert_expr(t, a); } + virtual void assert_lemma(expr* t) { + m_solver1->assert_lemma(t); + if (m_solver2_initialized) + m_solver2->assert_lemma(t); + } + virtual void push() { switch_inc_mode(); m_solver1->push(); diff --git a/src/solver/solver.h b/src/solver/solver.h index 5346cf4a4..f32c10887 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -90,6 +90,12 @@ public: */ virtual void assert_expr(expr * t, expr * a) = 0; + /** + \brief Add a lemma to the assertion stack. A lemma is assumed to be a consequence of already + asserted formulas. The solver is free to ignore lemmas. + */ + virtual void assert_lemma(expr * t) = 0; + /** \brief Create a backtracking point. */ diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index d3d8e59ce..6743eac74 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -55,6 +55,7 @@ public: virtual void set_produce_models(bool f) { m_produce_models = f; } virtual void assert_expr(expr * t); + virtual void assert_lemma(expr * t); virtual void push_core(); virtual void pop_core(unsigned n); @@ -115,6 +116,9 @@ void tactic2solver::assert_expr(expr * t) { m_result = 0; } +void tactic2solver::assert_lemma(expr * t) { +} + void tactic2solver::push_core() { m_scopes.push_back(m_assertions.size()); m_result = 0; diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 746856543..4ef909234 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -93,6 +93,10 @@ public: } } + virtual void assert_lemma(expr * t) { + m_solver->assert_lemma(t); + } + virtual void push_core() { flush_assertions(); m_solver->push(); diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 67be432c2..39519af4e 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -64,6 +64,16 @@ public: m_solver->assert_expr(bounds); } + virtual void assert_lemma(expr* t) { + expr_ref tmp(t, m); + expr_ref_vector bounds(m); + proof_ref tmp_proof(m); + m_rewriter(t, tmp, tmp_proof); + m_solver->assert_lemma(tmp); + m_rewriter.flush_side_constraints(bounds); + m_solver->assert_expr(bounds); + } + virtual void push_core() { m_rewriter.push(); m_solver->push(); diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index 27e2a5850..29f3314cb 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -56,6 +56,10 @@ public: m_assertions.push_back(t); } + virtual void assert_lemma(expr * t) { + m_solver->assert_lemma(t); + } + virtual void push_core() { flush_assertions(); m_rewriter.push();