diff --git a/lib/ast.h b/lib/ast.h
index 8691ed1f4..030a154d0 100644
--- a/lib/ast.h
+++ b/lib/ast.h
@@ -1823,7 +1823,9 @@ public:
bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); }
bool is_true(expr const * n) const { return n == m_true; }
bool is_false(expr const * n) const { return n == m_false; }
- bool is_complement_core(expr const * n1, expr const * n2) const { return (is_true(n1) && is_false(n2)) || (is_not(n1) && to_app(n1)->get_arg(0) == n2); }
+ bool is_complement_core(expr const * n1, expr const * n2) const {
+ return (is_true(n1) && is_false(n2)) || (is_not(n1) && to_app(n1)->get_arg(0) == n2);
+ }
bool is_complement(expr const * n1, expr const * n2) const { return is_complement_core(n1, n2) || is_complement_core(n2, n1); }
bool is_or(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_OR); }
diff --git a/lib/lib.vcxproj b/lib/lib.vcxproj
index e919ed609..975d2e88e 100644
--- a/lib/lib.vcxproj
+++ b/lib/lib.vcxproj
@@ -736,6 +736,7 @@
+
@@ -1151,6 +1152,7 @@
+
diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp
index 8c09607c4..2cfc2af2d 100644
--- a/lib/pdr_context.cpp
+++ b/lib/pdr_context.cpp
@@ -667,19 +667,9 @@ namespace pdr {
}
void pred_transformer::model2cube(app* c, expr* val, expr_ref_vector& res) const {
- datatype_util dt(m);
if (m.is_bool(val)) {
res.push_back(m.is_true(val)?c:m.mk_not(c));
}
- else if (is_app(val) && dt.is_constructor(to_app(val))) {
- func_decl* f = to_app(val)->get_decl();
- func_decl* r = dt.get_constructor_recognizer(f);
- res.push_back(m.mk_app(r,c));
- ptr_vector const& acc = *dt.get_constructor_accessors(f);
- for (unsigned i = 0; i < acc.size(); ++i) {
- model2cube(m.mk_app(acc[i], c), to_app(val)->get_arg(i), res);
- }
- }
else {
res.push_back(m.mk_eq(c, val));
}
@@ -1142,6 +1132,8 @@ namespace pdr {
}
context::~context() {
+ reset_model_generalizers();
+ reset_core_generalizers();
reset();
}
@@ -1153,10 +1145,6 @@ namespace pdr {
dealloc(it->m_value);
}
m_rels.reset();
- std::for_each(m_model_generalizers.begin(), m_model_generalizers.end(), delete_proc());
- std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc());
- m_model_generalizers.reset();
- m_core_generalizers.reset();
m_search.reset();
m_query = 0;
m_last_result = l_undef;
@@ -1206,6 +1194,8 @@ namespace pdr {
void context::update_rules(datalog::rule_set& rules) {
decl2rel rels;
+ init_model_generalizers(rules);
+ init_core_generalizers(rules);
init_rules(rules, rels);
decl2rel::iterator it = rels.begin(), end = rels.end();
for (; it != end; ++it) {
@@ -1219,8 +1209,6 @@ namespace pdr {
for (; it != end; ++it) {
m_rels.insert(it->m_key, it->m_value);
}
- init_model_generalizers();
- init_core_generalizers();
VERIFY(m_rels.find(m_query_pred, m_query));
}
@@ -1283,12 +1271,15 @@ namespace pdr {
bool is_propositional() { return m_is_propositional; }
};
- bool context::is_propositional() {
+ bool context::is_propositional(datalog::rule_set& rules) {
expr_fast_mark1 mark;
is_propositional_proc proc(m);
- decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
- for (; proc.is_propositional() && it != end; ++it) {
- quick_for_each_expr(proc, mark, it->m_value->transition());
+ datalog::rule_set::iterator it = rules.begin(), end = rules.end();
+ for (; proc.is_propositional() && it != end; ++it) {
+ quick_for_each_expr(proc, mark, (*it)->get_head());
+ for (unsigned i = 0; i < (*it)->get_tail_size(); ++i) {
+ quick_for_each_expr(proc, mark, (*it)->get_tail(i));
+ }
}
return proc.is_propositional();
}
@@ -1316,19 +1307,27 @@ namespace pdr {
bool is_bool() { return m_is_bool; }
};
- bool context::is_bool() {
+ bool context::is_bool(datalog::rule_set& rules) {
expr_fast_mark1 mark;
is_bool_proc proc(m);
- decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
+ datalog::rule_set::iterator it = rules.begin(), end = rules.end();
for (; proc.is_bool() && it != end; ++it) {
- quick_for_each_expr(proc, mark, it->m_value->transition());
+ quick_for_each_expr(proc, mark, (*it)->get_head());
+ for (unsigned i = 0; i < (*it)->get_tail_size(); ++i) {
+ quick_for_each_expr(proc, mark, (*it)->get_tail(i));
+ }
}
return proc.is_bool();
}
+ void context::reset_model_generalizers() {
+ std::for_each(m_model_generalizers.begin(), m_model_generalizers.end(), delete_proc());
+ m_model_generalizers.reset();
+ }
- void context::init_model_generalizers() {
- if (is_propositional()) {
+ void context::init_model_generalizers(datalog::rule_set& rules) {
+ reset_model_generalizers();
+ if (is_propositional(rules)) {
m_model_generalizers.push_back(alloc(bool_model_evaluation_generalizer, *this, m));
}
else {
@@ -1344,12 +1343,27 @@ namespace pdr {
}
}
- void context::init_core_generalizers() {
+ void context::reset_core_generalizers() {
+ std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc());
+ m_core_generalizers.reset();
+ }
+
+ void context::init_core_generalizers(datalog::rule_set& rules) {
+ reset_core_generalizers();
if (m_params.get_bool(":use-multicore-generalizer", false)) {
m_core_generalizers.push_back(alloc(core_multi_generalizer, *this));
}
- if (m_params.get_bool(":use-farkas", true) && !is_bool()) {
- m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams));
+ if (m_params.get_bool(":use-farkas", true) && !is_bool(rules)) {
+ // TBD:
+ m.toggle_proof_mode(PGM_FINE);
+ m_fparams.m_proof_mode = PGM_FINE;
+ m_fparams.m_arith_bound_prop = BP_NONE;
+ m_fparams.m_arith_auto_config_simplex = true;
+ m_fparams.m_arith_propagate_eqs = false;
+ m_fparams.m_arith_eager_eq_axioms = false;
+ m_fparams.m_arith_eq_bounds = false;
+
+ // m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams));
}
if (m_params.get_bool(":use-farkas-properties", false)) {
m_core_generalizers.push_back(alloc(core_farkas_properties_generalizer, *this));
diff --git a/lib/pdr_context.h b/lib/pdr_context.h
index e0ac2c53d..dc93e7433 100644
--- a/lib/pdr_context.h
+++ b/lib/pdr_context.h
@@ -321,11 +321,11 @@ namespace pdr {
// Initialization
class is_propositional_proc;
- bool is_propositional();
+ bool is_propositional(datalog::rule_set& rules);
class is_bool_proc;
- bool is_bool();
- void init_model_generalizers();
- void init_core_generalizers();
+ bool is_bool(datalog::rule_set& rules);
+ void init_model_generalizers(datalog::rule_set& rules);
+ void init_core_generalizers(datalog::rule_set& rules);
bool check_invariant(unsigned lvl);
bool check_invariant(unsigned lvl, func_decl* fn);
@@ -336,6 +336,9 @@ namespace pdr {
void simplify_formulas();
+ void reset_model_generalizers();
+ void reset_core_generalizers();
+
public:
/**
diff --git a/lib/pdr_farkas_learner.cpp b/lib/pdr_farkas_learner.cpp
index 5a5352207..0f1df172f 100644
--- a/lib/pdr_farkas_learner.cpp
+++ b/lib/pdr_farkas_learner.cpp
@@ -33,6 +33,7 @@ Revision History:
#include "pdr_interpolant_provider.h"
#include "ast_ll_pp.h"
#include "arith_bounds_tactic.h"
+#include "proof_utils.h"
#define PROOF_MODE PGM_FINE
//#define PROOF_MODE PGM_COARSE
@@ -224,14 +225,13 @@ namespace pdr {
farkas_learner::farkas_learner(front_end_params& params, ast_manager& outer_mgr)
: m_proof_params(get_proof_params(params)),
- m(PROOF_MODE),
- m_brwr(m),
- p2o(m, outer_mgr),
- o2p(outer_mgr, m),
+ m_pr(PROOF_MODE),
+ p2o(m_pr, outer_mgr),
+ o2p(outer_mgr, m_pr),
m_simplifier(mk_arith_bounds_tactic(outer_mgr))
{
- m.register_decl_plugins();
- m_ctx = alloc(smt::solver, m, m_proof_params);
+ m_pr.register_decl_plugins();
+ m_ctx = alloc(smt::solver, m_pr, m_proof_params);
}
front_end_params farkas_learner::get_proof_params(front_end_params& orig_params) {
@@ -283,13 +283,13 @@ namespace pdr {
bool farkas_learner::get_lemma_guesses(expr * A_ext, expr * B_ext, expr_ref_vector& lemmas)
{
- expr_ref A(o2p(A_ext), m);
- expr_ref B(o2p(B_ext), m);
- proof_ref pr(m);
- expr_ref tmp(m);
- expr_ref_vector ilemmas(m);
- equality_expander_cfg ee_rwr_cfg(m);
- rewriter_tpl ee_rwr(m, false, ee_rwr_cfg);
+ expr_ref A(o2p(A_ext), m_pr);
+ expr_ref B(o2p(B_ext), m_pr);
+ proof_ref pr(m_pr);
+ expr_ref tmp(m_pr);
+ expr_ref_vector ilemmas(m_pr);
+ equality_expander_cfg ee_rwr_cfg(m_pr);
+ rewriter_tpl ee_rwr(m_pr, false, ee_rwr_cfg);
lemmas.reset();
@@ -297,17 +297,15 @@ namespace pdr {
ee_rwr(B, B);
expr_set bs;
- func_decl_set Bsymbs;
- expr_ref_vector blist(m);
+ expr_ref_vector blist(m_pr);
datalog::flatten_and(B, blist);
for (unsigned i = 0; i < blist.size(); ++i) {
bs.insert(blist[i].get());
}
- collect_pure_proc collect_proc(Bsymbs);
- for_each_expr(collect_proc, B);
+
if (!m_ctx) {
- m_ctx = alloc(smt::solver, m, m_proof_params);
+ m_ctx = alloc(smt::solver, m_pr, m_proof_params);
}
m_ctx->push();
@@ -320,7 +318,7 @@ namespace pdr {
bool is_unsat = res == l_false;
if (is_unsat) {
pr = m_ctx->get_proof();
- get_lemmas(m_ctx->get_proof(), bs, Bsymbs, A, ilemmas);
+ get_lemmas(m_ctx->get_proof(), bs, ilemmas);
for (unsigned i = 0; i < ilemmas.size(); ++i) {
lemmas.push_back(p2o(ilemmas[i].get()));
}
@@ -330,7 +328,7 @@ namespace pdr {
IF_VERBOSE(3, {
for (unsigned i = 0; i < ilemmas.size(); ++i) {
- verbose_stream() << "B': " << mk_pp(ilemmas[i].get(), m) << "\n";
+ verbose_stream() << "B': " << mk_pp(ilemmas[i].get(), m_pr) << "\n";
}
});
@@ -339,7 +337,7 @@ namespace pdr {
tout << "A: " << mk_pp(A_ext, m_ctx->m()) << "\n";
tout << "B: " << mk_pp(B_ext, m_ctx->m()) << "\n";
for (unsigned i = 0; i < lemmas.size(); ++i) {
- tout << "B': " << mk_pp(ilemmas[i].get(), m) << "\n";
+ tout << "B': " << mk_pp(ilemmas[i].get(), m_pr) << "\n";
});
DEBUG_CODE(
if (is_unsat) {
@@ -371,7 +369,7 @@ namespace pdr {
}
model_converter_ref mc;
proof_converter_ref pc;
- expr_dependency_ref core(m);
+ expr_dependency_ref core(lemmas.get_manager());
goal_ref_buffer result;
(*m_simplifier)(g, result, mc, pc, core);
lemmas.reset();
@@ -385,6 +383,7 @@ namespace pdr {
void farkas_learner::combine_constraints(unsigned n, app * const * lits, rational const * coeffs, expr_ref& res)
{
+ ast_manager& m = res.get_manager();
constr res_c(m);
for(unsigned i = 0; i < n; ++i) {
res_c.add(coeffs[i], lits[i]);
@@ -503,7 +502,19 @@ namespace pdr {
units under Farkas.
*/
- void farkas_learner::get_lemmas(proof* root, expr_set const& bs, func_decl_set const& Bsymbs, expr* A, expr_ref_vector& lemmas) {
+ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector& lemmas) {
+ ast_manager& m = lemmas.get_manager();
+ bool_rewriter brwr(m);
+ func_decl_set Bsymbs;
+ collect_pure_proc collect_proc(Bsymbs);
+ expr_set::iterator it = bs.begin(), end = bs.end();
+ for (; it != end; ++it) {
+ for_each_expr(collect_proc, *it);
+ }
+
+ proof_ref tmp(root, m);
+ proof_utils::reduce_hypotheses(tmp);
+ IF_VERBOSE(2, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(tmp, m) << "\n";);
proof_ref pr(root, m);
permute_unit_resolution(pr);
@@ -567,7 +578,7 @@ namespace pdr {
// Add lemmas that depend on bs, have no hypotheses, don't depend on A.
if ((!hyps->empty() || a_depend.is_marked(p)) &&
- b_depend.is_marked(p) && !is_farkas_lemma(p)) {
+ b_depend.is_marked(p) && !is_farkas_lemma(m, p)) {
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
app* arg = to_app(p->get_arg(i));
if (IS_B_PURE(arg)) {
@@ -592,7 +603,6 @@ namespace pdr {
b_depend.mark(p, true);
}
else {
- SASSERT(m.get_fact(p) == A);
a_depend.mark(p, true);
}
break;
@@ -621,7 +631,7 @@ namespace pdr {
for (unsigned i = 0; i < to_app(fml)->get_num_args(); ++i) {
expr* f = to_app(fml)->get_arg(i);
expr_ref hyp(m);
- m_brwr.mk_not(f, hyp);
+ brwr.mk_not(f, hyp);
hyps->remove(hyp);
}
}
@@ -629,7 +639,7 @@ namespace pdr {
break;
}
case PR_TH_LEMMA: {
- if (!is_farkas_lemma(p)) break;
+ if (!is_farkas_lemma(m, p)) break;
SASSERT(m.has_fact(p));
unsigned prem_cnt = m.get_num_parents(p);
@@ -686,7 +696,7 @@ namespace pdr {
SASSERT(prem_cnt + 2 + num_args == d->get_num_parameters());
for (unsigned i = 0; i < num_args; ++i) {
expr* prem_e = args[i];
- m_brwr.mk_not(prem_e, tmp);
+ brwr.mk_not(prem_e, tmp);
VERIFY(params[i].is_rational(coef));
SASSERT(is_app(tmp));
lits.push_back(to_app(tmp));
@@ -712,6 +722,7 @@ namespace pdr {
}
void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, expr_ref_vector& lemmas) {
+ ast_manager& m = lemmas.get_manager();
ast_mark visited;
proof* p0 = p;
ptr_vector todo;
@@ -742,11 +753,13 @@ namespace pdr {
// permute unit resolution over Theory lemmas to track premises.
void farkas_learner::permute_unit_resolution(proof_ref& pr) {
- expr_ref_vector refs(m);
+ expr_ref_vector refs(pr.get_manager());
obj_map cache;
permute_unit_resolution(refs, cache, pr);
}
+
void farkas_learner::permute_unit_resolution(expr_ref_vector& refs, obj_map& cache, proof_ref& pr) {
+ ast_manager& m = pr.get_manager();
proof* pr2 = 0;
proof_ref_vector parents(m);
proof_ref prNew(pr);
@@ -825,10 +838,9 @@ namespace pdr {
cache.insert(pr, prNew);
refs.push_back(prNew);
pr = prNew;
- }
-
+ }
- bool farkas_learner::is_farkas_lemma(expr* e) {
+ bool farkas_learner::is_farkas_lemma(ast_manager& m, expr* e) {
app * a;
func_decl* d;
symbol sym;
diff --git a/lib/pdr_farkas_learner.h b/lib/pdr_farkas_learner.h
index f90419908..5ee4625c4 100644
--- a/lib/pdr_farkas_learner.h
+++ b/lib/pdr_farkas_learner.h
@@ -30,12 +30,10 @@ Revision History:
#include "front_end_params.h"
#include "tactic.h"
-
namespace pdr {
class farkas_learner {
class farkas_collector;
- class asserted_premise_collector;
class constant_replacer_cfg;
class equality_expander_cfg;
class constr;
@@ -43,8 +41,7 @@ class farkas_learner {
typedef obj_hashtable expr_set;
front_end_params m_proof_params;
- ast_manager m;
- bool_rewriter m_brwr; /** bool rewriter for m_proof_mgr */
+ ast_manager m_pr;
scoped_ptr m_ctx;
scoped_ptr m_simplifier;
@@ -68,10 +65,8 @@ class farkas_learner {
bool try_ensure_lemma_in_language(expr_ref& lemma, expr* A, const func_decl_set& lang);
- bool is_farkas_lemma(expr* e);
-
- void get_lemmas(proof* root, expr_set const& bs, func_decl_set const& Bsymbs, expr* A, expr_ref_vector& lemmas);
-
+ bool is_farkas_lemma(ast_manager& m, expr* e);
+
void get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, expr_ref_vector& lemmas);
void permute_unit_resolution(proof_ref& pr);
@@ -82,8 +77,6 @@ class farkas_learner {
static void test();
- void simplify_lemmas(expr_ref_vector& lemmas);
-
public:
farkas_learner(front_end_params& params, ast_manager& m);
@@ -100,6 +93,16 @@ public:
bool get_lemma_guesses(expr * A, expr * B, expr_ref_vector& lemmas);
+ /**
+ Traverse a proof and retrieve lemmas using the vocabulary from bs.
+ */
+ void get_lemmas(proof* root, expr_set const& bs, expr_ref_vector& lemmas);
+
+ /**
+ \brief Simplify lemmas using subsumption.
+ */
+ void simplify_lemmas(expr_ref_vector& lemmas);
+
void collect_statistics(statistics& st) const;
static void test(char const* filename);
diff --git a/lib/pdr_prop_solver.cpp b/lib/pdr_prop_solver.cpp
index e41ff04b6..9f2466180 100644
--- a/lib/pdr_prop_solver.cpp
+++ b/lib/pdr_prop_solver.cpp
@@ -25,13 +25,14 @@ Revision History:
#include "dl_util.h"
#include "model_pp.h"
#include "front_end_params.h"
-
-#define CTX_VERB_LBL 21
+#include "datatype_decl_plugin.h"
+#include "pdr_farkas_learner.h"
+#include "ast_smt2_pp.h"
//
// Auxiliary structure to introduce propositional names for assumptions that are not
// propositional. It is to work with the smt::context's restriction
-// that assumptions be propositional atoms.
+// that assumptions be propositional literals.
//
namespace pdr {
@@ -40,8 +41,10 @@ namespace pdr {
prop_solver& s;
ast_manager& m;
expr_ref_vector m_atoms;
+ expr_ref_vector m_assumptions;
obj_map m_fresh2expr;
obj_map m_expr2fresh;
+ obj_hashtable m_equivs;
unsigned m_num_fresh;
app * mk_fresh(expr* atom) {
@@ -64,28 +67,62 @@ namespace pdr {
++m_num_fresh;
m_expr2fresh.insert(atom, res);
m_fresh2expr.insert(res, atom);
- expr_ref equiv(m.mk_eq(atom, res), m);
+ expr_ref equiv(m.mk_or(atom, m.mk_not(res)), m);
s.m_ctx->assert_expr(equiv);
+ m_assumptions.push_back(equiv);
+ m_equivs.insert(equiv);
TRACE("pdr_verbose", tout << "name asserted " << mk_pp(equiv, m) << "\n";);
return res;
}
void mk_safe(expr_ref_vector& conjs) {
datalog::flatten_and(conjs);
+ expand_literals(conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
- expr * atom = conjs[i].get();
- bool negated = m.is_not(atom, atom); //remove negation
- SASSERT(!m.is_true(atom));
- if (!is_uninterp(atom) || to_app(atom)->get_num_args() != 0) {
- app * name = mk_fresh(atom);
- conjs[i] = negated?m.mk_not(name):name;
+ expr * lit = conjs[i].get();
+ expr * lit_core = lit;
+ m.is_not(lit, lit_core);
+ SASSERT(!m.is_true(lit));
+ if (!is_uninterp(lit_core) || to_app(lit_core)->get_num_args() != 0) {
+ conjs[i] = mk_fresh(lit);
+ }
+ }
+ m_assumptions.append(conjs);
+ }
+
+ void expand_literals(expr_ref_vector& conjs) {
+ arith_util arith(m);
+ datatype_util dt(m);
+ expr* e1, *e2, *c, *val;
+ for (unsigned i = 0; i < conjs.size(); ++i) {
+
+ expr* e = conjs[i].get();
+ if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) {
+ conjs[i] = arith.mk_le(e1,e2);
+ if (i+1 == conjs.size()) {
+ conjs.push_back(arith.mk_ge(e1, e2));
+ }
+ else {
+ conjs.push_back(conjs[i+1].get());
+ conjs[i+1] = arith.mk_ge(e1, e2);
+ }
+ ++i;
+ }
+ else if (m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) {
+ func_decl* f = to_app(val)->get_decl();
+ func_decl* r = dt.get_constructor_recognizer(f);
+ conjs[i] = m.mk_app(r,c);
+ ptr_vector const& acc = *dt.get_constructor_accessors(f);
+ for (unsigned i = 0; i < acc.size(); ++i) {
+ conjs.push_back(m.mk_eq(m.mk_app(acc[i], c), to_app(val)->get_arg(i)));
+ }
}
}
}
public:
safe_assumptions(prop_solver& s, expr_ref_vector const& assumptions):
- s(s), m(s.m), m_atoms(assumptions), m_num_fresh(0) {
+ s(s), m(s.m), m_atoms(assumptions), m_assumptions(m), m_num_fresh(0) {
mk_safe(m_atoms);
}
@@ -94,13 +131,26 @@ namespace pdr {
expr_ref_vector const& atoms() const { return m_atoms; }
+ unsigned assumptions_size() const { return m_assumptions.size(); }
+
+ expr* assumptions(unsigned i) const { return m_assumptions[i]; }
+
+ expr* undo_naming(expr* atom) {
+ if (m_equivs.contains(atom)) {
+ return m.mk_true();
+ }
+ SASSERT(is_app(atom)); //only apps can be used in safe cubes
+ m_fresh2expr.find(to_app(atom), atom);
+ return atom;
+ }
+
void undo_naming(expr_ref_vector& literals) {
for (unsigned i = 0; i < literals.size(); ++i) {
- expr * atom = literals[i].get(), *orig_atom;
- bool negated = m.is_not(atom, atom); //remove negation
- SASSERT(is_app(atom)); //only apps can be used in safe cubes
- if (m_fresh2expr.find(to_app(atom), orig_atom)) {
- literals[i] = negated?m.mk_not(orig_atom):orig_atom;
+ literals[i] = undo_naming(literals[i].get());
+ if (m.is_true(literals[i].get())) {
+ literals[i] = literals.back();
+ literals.pop_back();
+ --i;
}
}
}
@@ -162,7 +212,7 @@ namespace pdr {
void prop_solver::add_formula(expr * form) {
SASSERT(!m_in_level);
m_ctx->assert_expr(form);
- IF_VERBOSE(CTX_VERB_LBL, verbose_stream() << "$ asserted " << mk_pp(form, m) << "\n";);
+ IF_VERBOSE(21, verbose_stream() << "$ asserted " << mk_pp(form, m) << "\n";);
TRACE("pdr", tout << "add_formula: " << mk_pp(form, m) << "\n";);
}
@@ -175,6 +225,7 @@ namespace pdr {
lbool prop_solver::check_safe_assumptions(
+ safe_assumptions& safe,
const expr_ref_vector& atoms,
expr_ref_vector* core,
model_ref * mdl,
@@ -211,7 +262,32 @@ namespace pdr {
}
}
- if (result == l_false && core) {
+ if (result == l_false && core && m.proofs_enabled()) {
+ proof_ref pr(m);
+ pr = m_ctx->get_proof();
+ IF_VERBOSE(21, verbose_stream() << mk_ismt2_pp(pr, m) << "\n";);
+ farkas_learner fl(m_fparams, m);
+ expr_ref_vector lemmas(m);
+ obj_hashtable bs;
+ for (unsigned i = 0; i < safe.assumptions_size(); ++i) {
+ bs.insert(safe.assumptions(i));
+ }
+ fl.get_lemmas(pr, bs, lemmas);
+ safe.undo_naming(lemmas);
+ fl.simplify_lemmas(lemmas);
+
+ IF_VERBOSE(2,
+ verbose_stream() << "Lemmas\n";
+ for (unsigned i = 0; i < lemmas.size(); ++i) {
+ verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
+ });
+
+ core->reset();
+ core->append(lemmas);
+ return result;
+ }
+
+ if (result == l_false && core) {
core->reset();
for (unsigned i = 0; i < core_size; ++i) {
expr * core_expr = m_ctx->get_unsat_core_expr(i);
@@ -226,6 +302,10 @@ namespace pdr {
}
core->push_back(to_app(core_expr));
}
+ SASSERT(expr_atoms.size() >= core->size());
+
+ safe.undo_naming(*core);
+
TRACE("pdr",
tout << mk_pp(m_pm.mk_and(expr_atoms), m) << "\n";
tout << "core_exprs: ";
@@ -235,7 +315,7 @@ namespace pdr {
tout << "\n";
tout << "core: " << mk_pp(m_pm.mk_and(*core), m) << "\n";
);
- SASSERT(expr_atoms.size() >= core->size());
+
}
return result;
}
@@ -260,7 +340,8 @@ namespace pdr {
}
lbool prop_solver::check_assumptions_and_formula(
- const expr_ref_vector & atoms, expr * form,
+ const expr_ref_vector & atoms,
+ expr * form,
expr_ref_vector * core,
model_ref * mdl,
bool& assumes_level)
@@ -269,20 +350,17 @@ namespace pdr {
safe_assumptions safe(*this, atoms);
m_ctx->assert_expr(form);
CTRACE("pdr", !m.is_true(form), tout << "check with formula: " << mk_pp(form, m) << "\n";);
- lbool res = check_safe_assumptions(safe.atoms(), core, mdl, assumes_level);
+ lbool res = check_safe_assumptions(safe, safe.atoms(), core, mdl, assumes_level);
if (res == l_false && core && m_try_minimize_core) {
unsigned sz = core->size();
bool assumes_level1 = false;
- lbool res2 = check_safe_assumptions(*core, core, mdl, assumes_level1);
+ lbool res2 = check_safe_assumptions(safe, *core, core, mdl, assumes_level1);
if (res2 == l_false && sz > core->size()) {
- res = res2;
assumes_level = assumes_level1;
IF_VERBOSE(1, verbose_stream() << "reduced core size from " << sz << " to " << core->size() << "\n";);
}
}
- if (core) {
- safe.undo_naming(*core);
- }
+
//
// we don't have to undo model naming, as from the model
// we extract the values for state variables directly
diff --git a/lib/pdr_prop_solver.h b/lib/pdr_prop_solver.h
index 37ac25adb..76e65fca6 100644
--- a/lib/pdr_prop_solver.h
+++ b/lib/pdr_prop_solver.h
@@ -53,14 +53,16 @@ namespace pdr {
void push_level_atoms(unsigned level, expr_ref_vector & tgt) const;
void ensure_level(unsigned lvl);
+
+ class safe_assumptions;
lbool check_safe_assumptions(
- const expr_ref_vector & atoms,
+ safe_assumptions& assumptions,
+ expr_ref_vector const& atoms,
expr_ref_vector * core,
model_ref * mdl,
bool& assumes_level);
- class safe_assumptions;
public:
prop_solver(pdr::manager& pm, symbol const& name);
diff --git a/lib/pdr_smt_context_manager.cpp b/lib/pdr_smt_context_manager.cpp
index 6b881a019..062607f2a 100644
--- a/lib/pdr_smt_context_manager.cpp
+++ b/lib/pdr_smt_context_manager.cpp
@@ -89,6 +89,10 @@ namespace pdr {
m_context.get_model(model);
}
+ proof* _smt_context::get_proof() {
+ return m_context.get_proof();
+ }
+
smt_context_manager::smt_context_manager(front_end_params& fp, params_ref const& p, ast_manager& m):
m_fparams(fp), m_max_num_contexts(p.get_uint(":max-num-contexts", 500)),
m(m), m_num_contexts(0), m_predicate_list(m) {}
diff --git a/lib/pdr_smt_context_manager.h b/lib/pdr_smt_context_manager.h
index 718c5dd02..cdff26a19 100644
--- a/lib/pdr_smt_context_manager.h
+++ b/lib/pdr_smt_context_manager.h
@@ -40,6 +40,7 @@ namespace pdr {
virtual void assert_expr(expr* e) = 0;
virtual lbool check(expr_ref_vector& assumptions) = 0;
virtual void get_model(model_ref& model) = 0;
+ virtual proof* get_proof() = 0;
virtual unsigned get_unsat_core_size() = 0;
virtual expr* get_unsat_core_expr(unsigned i) = 0;
virtual void push() = 0;
@@ -62,6 +63,7 @@ namespace pdr {
virtual void assert_expr(expr* e);
virtual lbool check(expr_ref_vector& assumptions);
virtual void get_model(model_ref& model);
+ virtual proof* get_proof();
virtual void push() { m_context.push(); }
virtual void pop() { m_context.pop(1); }
virtual unsigned get_unsat_core_size() { return m_context.get_unsat_core_size(); }
@@ -77,6 +79,7 @@ namespace pdr {
virtual void assert_expr(expr* e);
virtual lbool check(expr_ref_vector& assumptions);
virtual void get_model(model_ref& model);
+ virtual proof* get_proof();
virtual void pop() { m_solver.pop(1); }
virtual void push() { m_solver.push(); }
// TBD: add unsat core extraction with sat::solver.
diff --git a/lib/unit_subsumption_tactic.cpp b/lib/unit_subsumption_tactic.cpp
index 5480ded54..cd43e73e3 100644
--- a/lib/unit_subsumption_tactic.cpp
+++ b/lib/unit_subsumption_tactic.cpp
@@ -37,6 +37,7 @@ struct unit_subsumption_tactic : public tactic {
m_cancel(false),
m_context(m, m_fparams, p),
m_clauses(m) {
+ m_fparams.m_proof_mode = m.proof_mode();
}
void set_cancel(bool f) {