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();