diff --git a/lib/ast.cpp b/lib/ast.cpp
index bfb4a09b4..8e878165c 100644
--- a/lib/ast.cpp
+++ b/lib/ast.cpp
@@ -1370,10 +1370,11 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
register_plugin(fid, new_p);
SASSERT(new_p->get_family_id() == fid);
+ SASSERT(has_plugin(fid));
}
SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
- SASSERT(from.has_plugin(fid) == has_plugin(fid));
+ SASSERT(!from.has_plugin(fid) || has_plugin(fid));
}
}
diff --git a/lib/ast.h b/lib/ast.h
index 558af34bd..685ddd4ad 100644
--- a/lib/ast.h
+++ b/lib/ast.h
@@ -1835,7 +1835,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/ast_smt_pp.cpp b/lib/ast_smt_pp.cpp
index 0dcd78101..aa3a9c76d 100644
--- a/lib/ast_smt_pp.cpp
+++ b/lib/ast_smt_pp.cpp
@@ -602,12 +602,22 @@ class smt_printer {
}
}
- m_out << " :pat { ";
+ if (m_is_smt2) {
+ m_out << " :pattern ( ";
+ }
+ else {
+ m_out << " :pat { ";
+ }
for (unsigned j = 0; j < pat->get_num_args(); ++j) {
print_no_lets(pat->get_arg(j));
m_out << " ";
}
- m_out << "}";
+ if (m_is_smt2) {
+ m_out << ")";
+ }
+ else {
+ m_out << "}";
+ }
}
if (m_is_smt2 && q->get_num_patterns() > 0) {
m_out << ")";
diff --git a/lib/dl_bmc_engine.cpp b/lib/dl_bmc_engine.cpp
index 99512f89a..f9c6c49c3 100644
--- a/lib/dl_bmc_engine.cpp
+++ b/lib/dl_bmc_engine.cpp
@@ -27,6 +27,7 @@ Revision History:
#include "dl_decl_plugin.h"
#include "bool_rewriter.h"
#include "model_smt2_pp.h"
+#include "ast_smt_pp.h"
namespace datalog {
bmc::bmc(context& ctx):
@@ -214,6 +215,7 @@ namespace datalog {
lbool bmc::check_linear() {
for (unsigned i = 0; ; ++i) {
IF_VERBOSE(1, verbose_stream() << "level: " << i << "\n";);
+ checkpoint();
compile_linear(i);
lbool res = check_linear(i);
if (res == l_undef) {
@@ -711,7 +713,11 @@ namespace datalog {
md->eval(trace, trace);
md->eval(path, path);
IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n";);
- IF_VERBOSE(2, m_solver.display(verbose_stream()); verbose_stream() << "\n";);
+ ast_smt_pp pp(m);
+ for (unsigned i = 0; i < m_solver.size(); ++i) {
+ pp.add_assumption(m_solver.get_formulas()[i]);
+ }
+ IF_VERBOSE(2, pp.display_smt2(verbose_stream(), m.mk_true()); verbose_stream() << "\n";);
m_answer = get_proof(md, to_app(trace), to_app(path));
is_sat = l_true;
}
diff --git a/lib/dl_check_table.cpp b/lib/dl_check_table.cpp
index 1b1dd4974..d7dfbe1ae 100644
--- a/lib/dl_check_table.cpp
+++ b/lib/dl_check_table.cpp
@@ -96,6 +96,9 @@ namespace datalog {
(*m_tocheck)(tocheck(tgt), tocheck(src), tocheck(delta));
(*m_checker)(checker(tgt), checker(src), checker(delta));
get(tgt).well_formed();
+ if (delta) {
+ get(*delta).well_formed();
+ }
}
};
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..8771791d5 100644
--- a/lib/pdr_context.cpp
+++ b/lib/pdr_context.cpp
@@ -382,16 +382,15 @@ namespace pdr {
}
lbool pred_transformer::is_reachable(model_node& n, expr_ref_vector* core) {
- unsigned level = n.level();
- expr* state = n.state();
+ TRACE("pdr",
+ tout << "is-reachable: " << head()->get_name() << " level: " << n.level() << "\n";
+ tout << mk_pp(n.state(), m) << "\n";);
+ ensure_level(n.level());
model_ref model;
- ensure_level(level);
- prop_solver::scoped_level _sl(m_solver, level);
- TRACE("pdr", tout << "is-reachable: " << head()->get_name() << " level: " << level << "\n";
- tout << mk_pp(state, m) << "\n";);
-
- bool assumes_level;
- lbool is_sat = m_solver.check_conjunction_as_assumptions(state, core, &model, assumes_level);
+ prop_solver::scoped_level _sl(m_solver, n.level());
+ m_solver.set_core(core);
+ m_solver.set_model(&model);
+ lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state());
if (is_sat == l_true && core) {
core->reset();
model2cube(*model, *core);
@@ -411,7 +410,31 @@ namespace pdr {
}
tmp = pm.mk_and(conj);
prop_solver::scoped_level _sl(m_solver, level);
- return m_solver.check_conjunction_as_assumptions(tmp, core, 0, assumes_level) == l_false;
+ m_solver.set_core(core);
+ lbool r = m_solver.check_conjunction_as_assumptions(tmp);
+ if (r == l_false) {
+ assumes_level = m_solver.assumes_level();
+ }
+ return r == l_false;
+ }
+
+ bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& lits, bool& assumes_level) {
+ manager& pm = get_pdr_manager();
+ expr_ref_vector conj(m), core(m);
+ expr_ref fml(m), states(m);
+ states = m.mk_not(pm.mk_and(lits));
+ mk_assumptions(head(), states, conj);
+ fml = pm.mk_and(conj);
+ prop_solver::scoped_level _sl(m_solver, level);
+ m_solver.set_core(&core);
+ m_solver.set_subset_based_core(true);
+ lbool res = m_solver.check_assumptions_and_formula(lits, fml);
+ if (res == l_false) {
+ lits.reset();
+ lits.append(core);
+ assumes_level = m_solver.assumes_level();
+ }
+ return res == l_false;
}
void pred_transformer::mk_assumptions(func_decl* head, expr* fml, expr_ref_vector& result) {
@@ -425,7 +448,6 @@ namespace pdr {
for (unsigned i = 0; i < m_predicates.size(); i++) {
func_decl* d = m_predicates[i];
if (d == head) {
- // tmp1 = (m_tag2rule.size() == 1)?fml:m.mk_implies(pred, fml);
tmp1 = m.mk_implies(pred, fml);
pm.formula_n2o(tmp1, tmp2, i);
result.push_back(tmp2);
@@ -667,19 +689,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));
}
@@ -893,10 +905,21 @@ namespace pdr {
return result;
}
+ bool model_search::is_repeated(model_node& n) const {
+ model_node* p = n.parent();
+ while (p) {
+ if (p->state() == n.state()) {
+ return true;
+ }
+ p = p->parent();
+ }
+ return false;
+ }
+
void model_search::add_leaf(model_node& n) {
unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value;
++count;
- if (count == 1) {
+ if (count == 1 || is_repeated(n)) {
set_leaf(n);
}
else {
@@ -924,7 +947,7 @@ namespace pdr {
}
obj_map& model_search::cache(model_node const& n) {
- unsigned l = n.level();
+ unsigned l = n.orig_level();
if (l >= m_cache.size()) {
m_cache.resize(l + 1);
}
@@ -954,7 +977,6 @@ namespace pdr {
}
void model_search::erase_leaf(model_node& n) {
-
if (n.children().empty() && n.is_open()) {
std::deque::iterator
it = m_leaves.begin(),
@@ -1118,6 +1140,21 @@ namespace pdr {
}
}
+ void model_search::backtrack_level(bool uses_level, model_node& n) {
+ SASSERT(m_root);
+ if (uses_level && m_root->level() > n.level()) {
+ IF_VERBOSE(2, verbose_stream() << "Increase level " << n.level() << "\n";);
+ n.increase_level();
+ m_leaves.push_back(&n);
+ }
+ else {
+ model_node* p = n.parent();
+ if (p) {
+ set_leaf(*p);
+ }
+ }
+ }
+
// ----------------
// context
@@ -1142,6 +1179,8 @@ namespace pdr {
}
context::~context() {
+ reset_model_generalizers();
+ reset_core_generalizers();
reset();
}
@@ -1153,10 +1192,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 +1241,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 +1256,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));
}
@@ -1257,53 +1292,24 @@ namespace pdr {
pt->add_cover(lvl, property);
}
-
- class context::is_propositional_proc {
- ast_manager& m;
- arith_util a;
- bool m_is_propositional;
- public:
- is_propositional_proc(ast_manager& m):m(m), a(m), m_is_propositional(true) {}
- void operator()(expr* e) {
- if (m_is_propositional) {
-
- if (!m.is_bool(e) && !a.is_int_real(e)) {
- m_is_propositional = false;
- }
- else if (!is_app(e)) {
- m_is_propositional = false;
- }
- else if (to_app(e)->get_num_args() > 0 &&
- to_app(e)->get_family_id() != m.get_basic_family_id() &&
- to_app(e)->get_family_id() != a.get_family_id()) {
- m_is_propositional = false;
- }
- }
- }
- bool is_propositional() { return m_is_propositional; }
- };
-
- bool context::is_propositional() {
- 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());
- }
- return proc.is_propositional();
- }
-
- class context::is_bool_proc {
+ class context::classifier_proc {
ast_manager& m;
+ arith_util a;
bool m_is_bool;
+ bool m_is_bool_arith;
public:
- is_bool_proc(ast_manager& m):m(m), m_is_bool(true) {}
+ classifier_proc(ast_manager& m, datalog::rule_set& rules):
+ m(m), a(m), m_is_bool(true), m_is_bool_arith(true) {
+ classify(rules);
+ }
void operator()(expr* e) {
- if (m_is_bool) {
-
+ if (m_is_bool) {
if (!m.is_bool(e)) {
m_is_bool = false;
}
+ else if (is_var(e)) {
+ // no-op.
+ }
else if (!is_app(e)) {
m_is_bool = false;
}
@@ -1312,44 +1318,101 @@ namespace pdr {
m_is_bool = false;
}
}
+ if (m_is_bool_arith) {
+ if (!m.is_bool(e) && !a.is_int_real(e)) {
+ m_is_bool_arith = false;
+ }
+ else if (is_var(e)) {
+ // no-op
+ }
+ else if (!is_app(e)) {
+ m_is_bool_arith = false;
+ }
+ else if (to_app(e)->get_num_args() > 0 &&
+ to_app(e)->get_family_id() != m.get_basic_family_id() &&
+ to_app(e)->get_family_id() != a.get_family_id()) {
+ m_is_bool_arith = false;
+ }
+ }
+ }
+
+ bool is_bool() const { return m_is_bool; }
+
+ bool is_bool_arith() const { return m_is_bool_arith; }
+
+
+ private:
+
+ void classify(datalog::rule_set& rules) {
+ expr_fast_mark1 mark;
+ datalog::rule_set::iterator it = rules.begin(), end = rules.end();
+ for (; it != end; ++it) {
+ datalog::rule& r = *(*it);
+ classify_pred(mark, r.get_head());
+ unsigned utsz = r.get_uninterpreted_tail_size();
+ for (unsigned i = 0; i < utsz; ++i) {
+ classify_pred(mark, r.get_tail(i));
+ }
+ for (unsigned i = utsz; i < r.get_tail_size(); ++i) {
+ quick_for_each_expr(*this, mark, r.get_tail(i));
+ }
+ }
+ }
+
+ void classify_pred(expr_fast_mark1& mark, app* pred) {
+ for (unsigned i = 0; i < pred->get_num_args(); ++i) {
+ quick_for_each_expr(*this, mark, pred->get_arg(i));
+ }
}
- bool is_bool() { return m_is_bool; }
};
- bool context::is_bool() {
- expr_fast_mark1 mark;
- is_bool_proc proc(m);
- decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
- for (; proc.is_bool() && it != end; ++it) {
- quick_for_each_expr(proc, mark, it->m_value->transition());
- }
- 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();
+ classifier_proc classify(m, rules);
+ if (classify.is_bool_arith()) {
m_model_generalizers.push_back(alloc(bool_model_evaluation_generalizer, *this, m));
}
else {
m_model_generalizers.push_back(alloc(model_evaluation_generalizer, *this, m));
}
-
if (m_params.get_bool(":use-farkas-model", false)) {
m_model_generalizers.push_back(alloc(model_farkas_generalizer, *this));
}
-
if (m_params.get_bool(":use-precondition-generalizer", false)) {
m_model_generalizers.push_back(alloc(model_precond_generalizer, *this));
}
}
- 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();
+ classifier_proc classify(m, rules);
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) && !classify.is_bool()) {
+ if (m_params.get_bool(":inline-proof-mode", true)) {
+ 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;
+ }
+ else {
+ 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));
@@ -1588,10 +1651,7 @@ namespace pdr {
TRACE("pdr", tout << "invariant state: " << (uses_level?"":"(inductive) ") << mk_pp(ncube, m) << "\n";);
n.pt().add_property(ncube, uses_level?n.level():infty_level);
CASSERT("pdr",n.level() == 0 || check_invariant(n.level()-1));
- model_node* p = n.parent();
- if (p) {
- m_search.set_leaf(*p);
- }
+ m_search.backtrack_level(uses_level && m_params.get_bool(":flexible-trace", false), n);
break;
}
case l_undef: {
diff --git a/lib/pdr_context.h b/lib/pdr_context.h
index 801ee6103..f849fdbcd 100644
--- a/lib/pdr_context.h
+++ b/lib/pdr_context.h
@@ -139,6 +139,7 @@ namespace pdr {
lbool is_reachable(model_node& n, expr_ref_vector* core);
bool is_invariant(unsigned level, expr* co_state, bool inductive, bool& assumes_level, expr_ref_vector* core = 0);
+ bool check_inductive(unsigned level, expr_ref_vector& state, bool& assumes_level);
expr_ref get_formulas(unsigned level, bool add_axioms);
@@ -171,10 +172,11 @@ namespace pdr {
model_ref m_model;
ptr_vector m_children;
unsigned m_level;
+ unsigned m_orig_level;
bool m_closed;
public:
model_node(model_node* parent, expr_ref& state, pred_transformer& pt, unsigned level):
- m_parent(parent), m_pt(pt), m_state(state), m_model(0), m_level(level), m_closed(false) {
+ m_parent(parent), m_pt(pt), m_state(state), m_model(0), m_level(level), m_orig_level(level), m_closed(false) {
if (m_parent) {
m_parent->m_children.push_back(this);
SASSERT(m_parent->m_level == level+1);
@@ -183,6 +185,8 @@ namespace pdr {
}
void set_model(model_ref& m) { m_model = m; }
unsigned level() const { return m_level; }
+ unsigned orig_level() const { return m_orig_level; }
+ void increase_level() { ++m_level; }
expr* state() const { return m_state; }
ptr_vector const& children() { return m_children; }
pred_transformer& pt() const { return m_pt; }
@@ -232,6 +236,8 @@ namespace pdr {
model_node* next();
+ bool is_repeated(model_node& n) const;
+
void add_leaf(model_node& n); // add fresh node.
void set_leaf(model_node& n); // Set node as leaf, remove children.
@@ -245,6 +251,8 @@ namespace pdr {
expr_ref get_trace() const;
proof_ref get_proof_trace(context const& ctx) const;
+
+ void backtrack_level(bool uses_level, model_node& n);
};
struct model_exception { };
@@ -324,12 +332,9 @@ namespace pdr {
// Initialization
- class is_propositional_proc;
- bool is_propositional();
- class is_bool_proc;
- bool is_bool();
- void init_model_generalizers();
- void init_core_generalizers();
+ class classifier_proc;
+ 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);
@@ -340,6 +345,9 @@ namespace pdr {
void simplify_formulas();
+ void reset_model_generalizers();
+ void reset_core_generalizers();
+
public:
/**
diff --git a/lib/pdr_dl_interface.cpp b/lib/pdr_dl_interface.cpp
index 15d7755c1..4439d571f 100644
--- a/lib/pdr_dl_interface.cpp
+++ b/lib/pdr_dl_interface.cpp
@@ -184,34 +184,23 @@ void dl_interface::updt_params() {
void dl_interface::collect_params(param_descrs& p) {
p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
+ p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object");
+ p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)");
+ p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples by extending candidate trace within search area");
PRIVATE_PARAMS(p.insert(":use-farkas-model", CPK_BOOL, "PDR: (default false) enable using Farkas generalization through model propagation"););
PRIVATE_PARAMS(p.insert(":use-precondition-generalizer", CPK_BOOL, "PDR: (default false) enable generalizations from weakest pre-conditions"););
- PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL,
- "PDR: (default false) extract multiple cores for blocking states"););
- PRIVATE_PARAMS(p.insert(":use-farkas-properties", CPK_BOOL,
- "PDR: (default false) experimental Farkas lemma generation method"););
- PRIVATE_PARAMS(p.insert(":use-inductive-generalizer", CPK_BOOL,
- "PDR: (default true) generalize lemmas using induction strengthening"););
- PRIVATE_PARAMS(p.insert(":use-interpolants", CPK_BOOL,
- "PDR: (default false) use iZ3 interpolation for lemma generation"););
- PRIVATE_PARAMS(p.insert(":dump-interpolants", CPK_BOOL,
- "PDR: (default false) display interpolants"););
- p.insert(":cache-mode", CPK_UINT, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search");
+ PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states"););
+ PRIVATE_PARAMS(p.insert(":use-farkas-properties", CPK_BOOL, "PDR: (default false) experimental Farkas lemma generation method"););
+ PRIVATE_PARAMS(p.insert(":use-inductive-generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening"););
+ PRIVATE_PARAMS(p.insert(":use-interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation"););
+ PRIVATE_PARAMS(p.insert(":dump-interpolants", CPK_BOOL, "PDR: (default false) display interpolants"););
+ PRIVATE_PARAMS(p.insert(":cache-mode", CPK_UINT, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search"););
PRIVATE_PARAMS(p.insert(":inductive-reachability-check", CPK_BOOL,
"PDR: (default false) assume negation of the cube on the previous level when "
"checking for reachability (not only during cube weakening)"););
- PRIVATE_PARAMS(p.insert(":max-num-contexts", CPK_UINT,
- "PDR: (default 500) maximal number of contexts to create"););
- PRIVATE_PARAMS(p.insert(":try-minimize-core", CPK_BOOL,
- "PDR: (default false) try to reduce core size (before inductive minimization)"););
- PRIVATE_PARAMS(p.insert(":simplify-formulas-pre", CPK_BOOL,
- "PDR: (default false) simplify derived formulas before inductive propagation"););
- PRIVATE_PARAMS(p.insert(":simplify-formulas-post", CPK_BOOL,
- "PDR: (default false) simplify derived formulas after inductive propagation"););
- PRIVATE_PARAMS(p.insert(":slice", CPK_BOOL,
- "PDR: (default true) simplify clause set using slicing"););
- p.insert(":generate-proof-trace", CPK_BOOL,
- "PDR: (default false) trace for 'sat' answer as proof object");
-
-
+ PRIVATE_PARAMS(p.insert(":max-num-contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create"););
+ PRIVATE_PARAMS(p.insert(":try-minimize-core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)"););
+ PRIVATE_PARAMS(p.insert(":simplify-formulas-pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation"););
+ PRIVATE_PARAMS(p.insert(":simplify-formulas-post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation"););
+ PRIVATE_PARAMS(p.insert(":slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing"););
}
diff --git a/lib/pdr_farkas_learner.cpp b/lib/pdr_farkas_learner.cpp
index a9a6956c3..c5dfd62f3 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,12 @@ 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_simplifier(mk_arith_bounds_tactic(outer_mgr))
+ m_pr(PROOF_MODE),
+ p2o(m_pr, outer_mgr),
+ o2p(outer_mgr, m_pr)
{
- 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 +282,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 +296,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,17 +317,16 @@ 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()));
}
- simplify_lemmas(lemmas);
}
m_ctx->pop(1);
IF_VERBOSE(3, {
- for (unsigned i = 0; i < lemmas.size(); ++i) {
- verbose_stream() << "B': " << mk_pp(ilemmas[i].get(), m) << "\n";
+ for (unsigned i = 0; i < ilemmas.size(); ++i) {
+ verbose_stream() << "B': " << mk_pp(ilemmas[i].get(), m_pr) << "\n";
}
});
@@ -339,7 +335,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) {
@@ -360,10 +356,11 @@ namespace pdr {
// Perform simple subsumption check of lemmas.
//
void farkas_learner::simplify_lemmas(expr_ref_vector& lemmas) {
- goal_ref g(alloc(goal, lemmas.get_manager(), false, false, false));
+ ast_manager& m = lemmas.get_manager();
+ goal_ref g(alloc(goal, m, false, false, false));
TRACE("farkas_simplify_lemmas",
for (unsigned i = 0; i < lemmas.size(); ++i) {
- tout << mk_pp(lemmas[i].get(), lemmas.get_manager()) << "\n";
+ tout << mk_pp(lemmas[i].get(), m) << "\n";
});
for (unsigned i = 0; i < lemmas.size(); ++i) {
@@ -373,7 +370,8 @@ namespace pdr {
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
- (*m_simplifier)(g, result, mc, pc, core);
+ tactic_ref simplifier = mk_arith_bounds_tactic(m);
+ (*simplifier)(g, result, mc, pc, core);
lemmas.reset();
SASSERT(result.size() == 1);
goal* r = result[0];
@@ -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,13 +502,27 @@ 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) {
+
+#define INSERT(_x_) if (!lemma_set.contains(_x_)) { lemma_set.insert(_x_); lemmas.push_back(_x_); }
+
+ 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 pr(root, m);
- permute_unit_resolution(pr);
+ proof_utils::reduce_hypotheses(pr);
+ proof_utils::permute_unit_resolution(pr);
+ IF_VERBOSE(3, verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n";);
ptr_vector hyprefs;
obj_map hypmap;
+ obj_hashtable lemma_set;
ast_mark b_depend, a_depend, visited, b_closed;
expr_set* empty_set = alloc(expr_set);
hyprefs.push_back(empty_set);
@@ -565,21 +578,23 @@ namespace pdr {
#define IS_B_PURE(_p) (b_depend.is_marked(_p) && !a_depend.is_marked(_p) && hypmap.find(_p)->empty())
+
// 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)) {
- if (is_pure_expr(Bsymbs, m.get_fact(arg))) {
+ expr* fact = m.get_fact(arg);
+ if (is_pure_expr(Bsymbs, fact)) {
TRACE("farkas_learner",
tout << "Add: " << mk_pp(m.get_fact(arg), m) << "\n";
tout << mk_pp(arg, m) << "\n";
);
- lemmas.push_back(m.get_fact(arg));
+ INSERT(fact);
}
else {
- get_asserted(p, bs, b_closed, lemmas);
+ get_asserted(p, bs, b_closed, lemma_set, lemmas);
b_closed.mark(p, true);
}
}
@@ -592,7 +607,6 @@ namespace pdr {
b_depend.mark(p, true);
}
else {
- SASSERT(m.get_fact(p) == A);
a_depend.mark(p, true);
}
break;
@@ -621,7 +635,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 +643,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 +700,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));
@@ -699,7 +713,7 @@ namespace pdr {
expr_ref res(m);
combine_constraints(coeffs.size(), lits.c_ptr(), coeffs.c_ptr(), res);
TRACE("farkas_learner", tout << "Add: " << mk_pp(res, m) << "\n";);
- lemmas.push_back(res);
+ INSERT(res);
b_closed.mark(p, true);
}
}
@@ -709,9 +723,11 @@ namespace pdr {
}
std::for_each(hyprefs.begin(), hyprefs.end(), delete_proc());
+ simplify_lemmas(lemmas);
}
- void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, expr_ref_vector& lemmas) {
+ void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable& lemma_set, expr_ref_vector& lemmas) {
+ ast_manager& m = lemmas.get_manager();
ast_mark visited;
proof* p0 = p;
ptr_vector todo;
@@ -731,104 +747,18 @@ namespace pdr {
}
if (p->get_decl_kind() == PR_ASSERTED &&
bs.contains(m.get_fact(p))) {
+ expr* fact = m.get_fact(p);
TRACE("farkas_learner",
tout << mk_ll_pp(p0,m) << "\n";
tout << "Add: " << mk_pp(p,m) << "\n";);
- lemmas.push_back(m.get_fact(p));
+ INSERT(fact);
b_closed.mark(p, true);
}
}
}
- // permute unit resolution over Theory lemmas to track premises.
- void farkas_learner::permute_unit_resolution(proof_ref& pr) {
- expr_ref_vector refs(m);
- 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) {
- proof* pr2 = 0;
- proof_ref_vector parents(m);
- proof_ref prNew(pr);
- if (cache.find(pr, pr2)) {
- pr = pr2;
- return;
- }
- for (unsigned i = 0; i < m.get_num_parents(pr); ++i) {
- prNew = m.get_parent(pr, i);
- permute_unit_resolution(refs, cache, prNew);
- parents.push_back(prNew);
- }
-
- prNew = pr;
- if (pr->get_decl_kind() == PR_UNIT_RESOLUTION &&
- parents[0]->get_decl_kind() == PR_TH_LEMMA) {
- /*
- Unit resolution:
- T1: (or l_1 ... l_n l_1' ... l_m')
- T2: (not l_1)
- ...
- T(n+1): (not l_n)
- [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
- Th lemma:
- T1: (not l_1)
- ...
- Tn: (not l_n)
- [th-lemma T1 ... Tn]: (or l_{n+1} ... l_m)
-
- Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom.
-
- Implement conversion:
-
- T1 |- not l_1 ... Tn |- not l_n
- ------------------------------- TH_LEMMA
- (or k_1 .. k_m j_1 ... j_m) S1 |- not k_1 ... Sm |- not k_m
- -------------------------------------------------------------- UNIT_RESOLUTION
- (or j_1 .. j_m)
-
-
- |->
-
- T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m
- ---------------------------------------------------------------- TH_LEMMA
- (or j_1 .. j_m)
-
- */
- proof_ref_vector premises(m);
- proof* thLemma = parents[0].get();
- for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) {
- premises.push_back(m.get_parent(thLemma, i));
- }
- for (unsigned i = 1; i < parents.size(); ++i) {
- premises.push_back(parents[i].get());
- }
- parameter const* params = thLemma->get_decl()->get_parameters();
- unsigned num_params = thLemma->get_decl()->get_num_parameters();
- SASSERT(params[0].is_symbol());
- family_id tid = m.get_family_id(params[0].get_symbol());
- SASSERT(tid != null_family_id);
- prNew = m.mk_th_lemma(tid, m.get_fact(pr),
- premises.size(), premises.c_ptr(), num_params-1, params+1);
- }
- else {
- ptr_vector args;
- for (unsigned i = 0; i < parents.size(); ++i) {
- args.push_back(parents[i].get());
- }
- if (m.has_fact(pr)) {
- args.push_back(m.get_fact(pr));
- }
- prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr());
- }
-
- 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..e068b5537 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,10 +41,8 @@ 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;
static front_end_params get_proof_params(front_end_params& orig_params);
@@ -68,22 +64,14 @@ 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);
-
- void get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, expr_ref_vector& lemmas);
-
- void permute_unit_resolution(proof_ref& pr);
-
- void permute_unit_resolution(expr_ref_vector& refs, obj_map& cache, proof_ref& pr);
+ bool is_farkas_lemma(ast_manager& m, expr* e);
+
+ void get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable& lemma_set, expr_ref_vector& lemmas);
bool is_pure_expr(func_decl_set const& symbs, expr* e) const;
static void test();
- void simplify_lemmas(expr_ref_vector& lemmas);
-
public:
farkas_learner(front_end_params& params, ast_manager& m);
@@ -100,6 +88,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_generalizers.cpp b/lib/pdr_generalizers.cpp
index 445b60665..cddc2eb37 100644
--- a/lib/pdr_generalizers.cpp
+++ b/lib/pdr_generalizers.cpp
@@ -99,28 +99,26 @@ namespace pdr {
}
ast_manager& m = core.get_manager();
TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; } "\n";);
- unsigned num_failures = 0, i = 0, num_changes = 0;
- while (i < core.size() && (!m_failure_limit || num_failures <= m_failure_limit)) {
- expr_ref lit(m), state(m);
+ unsigned num_failures = 0, i = 0, old_core_size = core.size();
+ ptr_vector processed;
+
+ while (i < core.size() && 1 < core.size() && (!m_failure_limit || num_failures <= m_failure_limit)) {
+ expr_ref lit(m);
lit = core[i].get();
- core[i] = m.mk_true();
- state = m.mk_not(n.pt().get_pdr_manager().mk_and(core));
- bool assumes_level = false;
- if (n.pt().is_invariant(n.level(), state, true, assumes_level, 0)) {
+ core[i] = m.mk_true();
+ if (n.pt().check_inductive(n.level(), core, uses_level)) {
num_failures = 0;
- core[i] = core.back();
- core.pop_back();
- TRACE("pdr", tout << "Remove: " << mk_pp(lit, m) << "\n";);
- ++num_changes;
- uses_level = assumes_level;
+ for (i = 0; i < core.size() && processed.contains(core[i].get()); ++i);
}
else {
core[i] = lit;
+ processed.push_back(lit);
++num_failures;
++i;
}
}
- TRACE("pdr", tout << "changes: " << num_changes << " index: " << i << " size: " << core.size() << "\n";);
+ IF_VERBOSE(2, verbose_stream() << "old size: " << old_core_size << " new size: " << core.size() << "\n";);
+ TRACE("pdr", tout << "old size: " << old_core_size << " new size: " << core.size() << "\n";);
}
//
diff --git a/lib/pdr_prop_solver.cpp b/lib/pdr_prop_solver.cpp
index e41ff04b6..2908bf4f6 100644
--- a/lib/pdr_prop_solver.cpp
+++ b/lib/pdr_prop_solver.cpp
@@ -25,13 +25,15 @@ 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"
+#include "expr_replacer.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,70 +42,145 @@ namespace pdr {
prop_solver& s;
ast_manager& m;
expr_ref_vector m_atoms;
- obj_map m_fresh2expr;
- obj_map m_expr2fresh;
- unsigned m_num_fresh;
+ expr_ref_vector m_assumptions;
+ obj_map m_proxies2expr;
+ obj_map m_expr2proxies;
+ obj_hashtable m_implies;
+ unsigned m_num_proxies;
- app * mk_fresh(expr* atom) {
+ app * mk_proxy(expr* literal) {
app* res;
- SASSERT(!is_var(atom)); //it doesn't make sense to introduce names to variables
- if (m_expr2fresh.find(atom, res)) {
+ SASSERT(!is_var(literal)); //it doesn't make sense to introduce names to variables
+ if (m_expr2proxies.find(literal, res)) {
return res;
}
- SASSERT(s.m_fresh.size() >= m_num_fresh);
- if (m_num_fresh == s.m_fresh.size()) {
+ SASSERT(s.m_proxies.size() >= m_num_proxies);
+ if (m_num_proxies == s.m_proxies.size()) {
std::stringstream name;
- name << "pdr_proxy_" << s.m_fresh.size();
+ name << "pdr_proxy_" << s.m_proxies.size();
res = m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort());
- s.m_fresh.push_back(res);
+ s.m_proxies.push_back(res);
s.m_aux_symbols.insert(res->get_decl());
}
else {
- res = s.m_fresh[m_num_fresh].get();
+ res = s.m_proxies[m_num_proxies].get();
}
- ++m_num_fresh;
- m_expr2fresh.insert(atom, res);
- m_fresh2expr.insert(res, atom);
- expr_ref equiv(m.mk_eq(atom, res), m);
- s.m_ctx->assert_expr(equiv);
- TRACE("pdr_verbose", tout << "name asserted " << mk_pp(equiv, m) << "\n";);
+ ++m_num_proxies;
+ m_expr2proxies.insert(literal, res);
+ m_proxies2expr.insert(res, literal);
+ expr_ref implies(m.mk_or(m.mk_not(res), literal), m);
+ s.m_ctx->assert_expr(implies);
+ m_assumptions.push_back(implies);
+ m_implies.insert(implies);
+ TRACE("pdr_verbose", tout << "name asserted " << mk_pp(implies, 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_proxy(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_proxies(0) {
mk_safe(m_atoms);
- }
+ }
+
+ ~safe_assumptions() {
+ }
+
+ 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]; }
- ~safe_assumptions() {
- }
+ void undo_proxies(expr_ref_vector& es) {
+ expr_ref e(m);
+ expr* r;
+ for (unsigned i = 0; i < es.size(); ++i) {
+ e = es[i].get();
+ if (is_app(e) && m_proxies2expr.find(to_app(e), r)) {
+ es[i] = r;
+ }
+ }
+ }
+
+ void elim_proxies(expr_ref_vector& es) {
+ expr_substitution sub(m, false, m.proofs_enabled());
+ proof_ref pr(m);
+ if (m.proofs_enabled()) {
+ pr = m.mk_asserted(m.mk_true());
+ }
+ obj_map::iterator it = m_proxies2expr.begin(), end = m_proxies2expr.end();
+ for (; it != end; ++it) {
+ sub.insert(it->m_key, m.mk_true(), pr);
+ }
+ scoped_ptr rep = mk_default_expr_replacer(m);
+ rep->set_substitution(&sub);
+ replace_proxies(*rep, es);
+ }
+ private:
- expr_ref_vector const& atoms() const { return m_atoms; }
-
- 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;
- }
- }
- }
+ void replace_proxies(expr_replacer& rep, expr_ref_vector& es) {
+ expr_ref e(m);
+ for (unsigned i = 0; i < es.size(); ++i) {
+ e = es[i].get();
+ if (m_implies.contains(e)) {
+ e = m.mk_true();
+ }
+ else {
+ rep(e);
+ }
+ es[i] = e;
+ if (m.is_true(e)) {
+ es[i] = es.back();
+ es.pop_back();
+ --i;
+ }
+ }
+ }
};
@@ -116,7 +193,9 @@ namespace pdr {
m_ctx(pm.mk_fresh()),
m_pos_level_atoms(m),
m_neg_level_atoms(m),
- m_fresh(m),
+ m_proxies(m),
+ m_core(0),
+ m_subset_based_core(false),
m_in_level(false)
{
m_ctx->assert_expr(m_pm.get_background());
@@ -162,7 +241,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,15 +254,12 @@ namespace pdr {
lbool prop_solver::check_safe_assumptions(
- const expr_ref_vector& atoms,
- expr_ref_vector* core,
- model_ref * mdl,
- bool& assumes_level)
+ safe_assumptions& safe,
+ const expr_ref_vector& atoms)
{
- flet _model(m_fparams.m_model, mdl != 0);
+ flet _model(m_fparams.m_model, m_model != 0);
expr_ref_vector expr_atoms(m);
expr_atoms.append(atoms.size(), atoms.c_ptr());
- assumes_level = false;
if (m_in_level) {
push_level_atoms(m_current_level, expr_atoms);
@@ -195,94 +271,107 @@ namespace pdr {
tout << mk_pp(m_pm.mk_and(expr_atoms), m) << "\n";
tout << result << "\n";);
- if (result == l_true && mdl) {
- m_ctx->get_model(*mdl);
- TRACE("pdr_verbose", model_pp(tout, **mdl); );
+ if (result == l_true && m_model) {
+ m_ctx->get_model(*m_model);
+ TRACE("pdr_verbose", model_pp(tout, **m_model); );
}
-
- unsigned core_size = m_ctx->get_unsat_core_size();
-
- if (result == l_false && !core) {
+
+ if (result == l_false) {
+ unsigned core_size = m_ctx->get_unsat_core_size();
+ m_assumes_level = false;
for (unsigned i = 0; i < core_size; ++i) {
if (m_level_atoms_set.contains(m_ctx->get_unsat_core_expr(i))) {
- assumes_level = true;
+ m_assumes_level = true;
break;
}
}
}
- 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);
- SASSERT(is_app(core_expr));
-
- if (m_level_atoms_set.contains(core_expr)) {
- assumes_level = true;
- continue;
- }
- if (m_ctx->is_aux_predicate(core_expr)) {
- continue;
- }
- core->push_back(to_app(core_expr));
- }
- TRACE("pdr",
- tout << mk_pp(m_pm.mk_and(expr_atoms), m) << "\n";
- tout << "core_exprs: ";
- for (unsigned i = 0; i < core_size; ++i) {
- tout << mk_pp(m_ctx->get_unsat_core_expr(i), m) << " ";
- }
- tout << "\n";
- tout << "core: " << mk_pp(m_pm.mk_and(*core), m) << "\n";
- );
- SASSERT(expr_atoms.size() >= core->size());
+ if (result == l_false && m_core && m.proofs_enabled() && !m_subset_based_core) {
+ extract_theory_core(safe);
}
+ else if (result == l_false && m_core) {
+ extract_subset_core(safe);
+ SASSERT(expr_atoms.size() >= m_core->size());
+ }
+ m_core = 0;
+ m_model = 0;
+ m_subset_based_core = false;
return result;
}
- lbool prop_solver::check_assumptions(
- const expr_ref_vector & atoms,
- expr_ref_vector * core,
- model_ref * mdl,
- bool& assumes_level)
- {
- return check_assumptions_and_formula(atoms, m.mk_true(), core, mdl, assumes_level);
+ void prop_solver::extract_subset_core(safe_assumptions& safe) {
+ unsigned core_size = m_ctx->get_unsat_core_size();
+ m_core->reset();
+ for (unsigned i = 0; i < core_size; ++i) {
+ expr * core_expr = m_ctx->get_unsat_core_expr(i);
+ SASSERT(is_app(core_expr));
+
+ if (m_level_atoms_set.contains(core_expr)) {
+ continue;
+ }
+ if (m_ctx->is_aux_predicate(core_expr)) {
+ continue;
+ }
+ m_core->push_back(to_app(core_expr));
+ }
+
+ safe.undo_proxies(*m_core);
+
+ TRACE("pdr",
+ tout << "core_exprs: ";
+ for (unsigned i = 0; i < core_size; ++i) {
+ tout << mk_pp(m_ctx->get_unsat_core_expr(i), m) << " ";
+ }
+ tout << "\n";
+ tout << "core: " << mk_pp(m_pm.mk_and(*m_core), m) << "\n";
+ );
}
- lbool prop_solver::check_conjunction_as_assumptions(
- expr * conj,
- expr_ref_vector * core,
- model_ref * mdl,
- bool& assumes_level) {
+
+ void prop_solver::extract_theory_core(safe_assumptions& safe) {
+ 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.elim_proxies(lemmas);
+ fl.simplify_lemmas(lemmas); // redundant
+
+ IF_VERBOSE(2,
+ verbose_stream() << "Lemmas\n";
+ for (unsigned i = 0; i < lemmas.size(); ++i) {
+ verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
+ });
+
+ m_core->reset();
+ m_core->append(lemmas);
+ }
+
+ lbool prop_solver::check_assumptions(const expr_ref_vector & atoms)
+ {
+ return check_assumptions_and_formula(atoms, m.mk_true());
+ }
+
+ lbool prop_solver::check_conjunction_as_assumptions(expr * conj) {
expr_ref_vector asmp(m);
asmp.push_back(conj);
- return check_assumptions(asmp, core, mdl, assumes_level);
+ return check_assumptions(asmp);
}
- lbool prop_solver::check_assumptions_and_formula(
- const expr_ref_vector & atoms, expr * form,
- expr_ref_vector * core,
- model_ref * mdl,
- bool& assumes_level)
+ lbool prop_solver::check_assumptions_and_formula(const expr_ref_vector & atoms, expr * form)
{
pdr::smt_context::scoped _scoped(*m_ctx);
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);
- 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);
- 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);
- }
+ lbool res = check_safe_assumptions(safe, safe.atoms());
+
//
// 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..2b7c1af6d 100644
--- a/lib/pdr_prop_solver.h
+++ b/lib/pdr_prop_solver.h
@@ -33,6 +33,7 @@ Revision History:
namespace pdr {
class prop_solver {
+
private:
front_end_params& m_fparams;
ast_manager& m;
@@ -44,7 +45,11 @@ namespace pdr {
app_ref_vector m_pos_level_atoms; // atoms used to identify level
app_ref_vector m_neg_level_atoms; //
obj_hashtable m_level_atoms_set;
- app_ref_vector m_fresh; // predicates for assumptions
+ app_ref_vector m_proxies; // predicates for assumptions
+ expr_ref_vector* m_core;
+ model_ref* m_model;
+ bool m_subset_based_core;
+ bool m_assumes_level;
func_decl_set m_aux_symbols;
bool m_in_level;
unsigned m_current_level; // set when m_in_level
@@ -53,14 +58,17 @@ namespace pdr {
void push_level_atoms(unsigned level, expr_ref_vector & tgt) const;
void ensure_level(unsigned lvl);
+
+ class safe_assumptions;
+
+ void extract_theory_core(safe_assumptions& assumptions);
+
+ void extract_subset_core(safe_assumptions& assumptions);
lbool check_safe_assumptions(
- const expr_ref_vector & atoms,
- expr_ref_vector * core,
- model_ref * mdl,
- bool& assumes_level);
+ safe_assumptions& assumptions,
+ expr_ref_vector const& atoms);
- class safe_assumptions;
public:
prop_solver(pdr::manager& pm, symbol const& name);
@@ -71,6 +79,11 @@ namespace pdr {
m_aux_symbols.contains(s) ||
m_ctx->is_aux_predicate(s);
}
+
+ void set_core(expr_ref_vector* core) { m_core = core; }
+ void set_model(model_ref* mdl) { m_model = mdl; }
+ void set_subset_based_core(bool f) { m_subset_based_core = f; }
+ bool assumes_level() const { return m_assumes_level; }
void add_level();
unsigned level_cnt() const;
@@ -97,24 +110,16 @@ namespace pdr {
* If the conjunction of atoms is consistent with the solver state and o_model is non-zero,
* o_model will contain the "o" literals true in the assignment.
*/
- lbool check_assumptions(
- const expr_ref_vector & atoms,
- expr_ref_vector * core, model_ref * mdl,
- bool& assumes_level);
+ lbool check_assumptions(const expr_ref_vector & atoms);
- lbool check_conjunction_as_assumptions(
- expr * conj, expr_ref_vector * core,
- model_ref * mdl, bool& assumes_level);
+ lbool check_conjunction_as_assumptions(expr * conj);
/**
* Like check_assumptions, except it also asserts an extra formula
*/
lbool check_assumptions_and_formula(
const expr_ref_vector & atoms,
- expr * form,
- expr_ref_vector * core,
- model_ref * mdl,
- bool& assumes_level);
+ expr * form);
void collect_statistics(statistics& st) const;
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/pdr_util.cpp b/lib/pdr_util.cpp
index d3e73a2f4..04ad64851 100644
--- a/lib/pdr_util.cpp
+++ b/lib/pdr_util.cpp
@@ -206,50 +206,49 @@ void th_rewriter_model_evaluator::check_model(ptr_vector const & formulas,
m_rewriter.reset();
}
- //00 -- non-visited
- //01 -- X
- //10 -- false
- //11 -- true
-
-#define UNKNOWN(x) (!m1.is_marked(x) && !m2.is_marked(x))
-#define SET_UNKNOWN(x) { TRACE("pdr_verbose", tout << "unknown: " << mk_pp(x,m) << "\n";); m1.reset_mark(x); m2.reset_mark(x); }
-#define IS_X(x) (!m1.is_marked(x) && m2.is_marked(x))
-#define IS_FALSE(x) (m1.is_marked(x) && !m2.is_marked(x))
-#define IS_TRUE(x) (m1.is_marked(x) && m2.is_marked(x))
-#define SET_X(x) { SASSERT(UNKNOWN(x)); m2.mark(x); }
-#define SET_V(x) { SASSERT(UNKNOWN(x)); m1.mark(x); }
-#define SET_FALSE(x) { SASSERT(UNKNOWN(x)); m1.mark(x); }
-#define SET_TRUE(x) { SASSERT(UNKNOWN(x)); m1.mark(x); m2.mark(x); }
-#define SET_BOOL(x, v) { if (v) { SET_TRUE(x); } else { SET_FALSE(x); } }
-#define GET_VALUE(x) m_values.find(x)
-#define SET_VALUE(x,y) { SET_V(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << y << "\n";); m_values.insert(x, y); }
-
-void ternary_model_evaluator::add_model(expr* e) {
- expr* nlit, *var, *val;
- rational r;
- // SASSERT(UNKNOWN(e));
+bool ternary_model_evaluator::get_assignment(expr* e, expr*& var, expr*& val) {
if (m.is_eq(e, var, val)) {
if (!is_uninterp(var)) {
std::swap(var, val);
}
- if (m.is_true(val) && UNKNOWN(var)) {
- SET_TRUE(var);
- }
- else if (m.is_false(val) && UNKNOWN(var)) {
- SET_FALSE(var);
- }
- else if (m_arith.is_numeral(val, r) && UNKNOWN(var)) {
- SET_VALUE(var, r);
- }
- else {
- TRACE("pdr_verbose", tout << "no value for " << mk_pp(val, m) << "\n";);
+ if (m.is_true(val) || m.is_false(val) || m_arith.is_numeral(val)) {
+ return true;
}
+ TRACE("pdr_verbose", tout << "no value for " << mk_pp(val, m) << "\n";);
+ return false;
}
- else if (m.is_not(e, nlit)) {
- SET_FALSE(nlit);
+ else if (m.is_not(e, var)) {
+ val = m.mk_false();
+ return true;
}
else if (m.is_bool(e)) {
- SET_TRUE(e);
+ val = m.mk_true();
+ var = e;
+ return true;
+ }
+ else {
+ TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";);
+ return false;
+ }
+}
+
+
+void ternary_model_evaluator::add_model(expr* e) {
+ expr* var, *val;
+ rational r;
+ // SASSERT(is_unknown(e));
+ if (get_assignment(e, var, val)) {
+ if (is_unknown(var)) {
+ if (m.is_true(val)) {
+ set_true(var);
+ }
+ else if (m.is_false(val)) {
+ set_false(var);
+ }
+ else if (m_arith.is_numeral(val, r)) {
+ set_value(var, r);
+ }
+ }
}
else {
TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";);
@@ -257,19 +256,12 @@ void ternary_model_evaluator::add_model(expr* e) {
}
void ternary_model_evaluator::del_model(expr* e) {
- expr* nlit, *var, *val;
- if (m.is_eq(e, var, val)) {
- if (!is_uninterp(var)) {
- std::swap(var, val);
+ expr *var, *val;
+ if (get_assignment(e, var, val)) {
+ set_unknown(var);
+ if (!m.is_bool(var)) {
+ m_values.remove(var);
}
- SET_UNKNOWN(var);
- m_values.remove(var);
- }
- else if (m.is_not(e, nlit)) {
- SET_UNKNOWN(nlit);
- }
- else if (m.is_bool(e)) {
- SET_UNKNOWN(e);
}
else {
TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";);
@@ -280,7 +272,7 @@ void ternary_model_evaluator::setup_model(expr_ref_vector const& model) {
m_values.reset();
for (unsigned i = 0; i < model.size(); ++i) {
expr* e = model[i];
- if (UNKNOWN(e)) {
+ if (is_unknown(e)) {
add_model(e);
}
}
@@ -297,6 +289,19 @@ void ternary_model_evaluator::minimize_model(ptr_vector const & formulas,
tout << "formulas\n";
for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
);
+
+ prune_by_cone_of_influence(formulas, model);
+
+ // prune_by_probing(formulas, model);
+
+ m1.reset();
+ m2.reset();
+ m_values.reset();
+}
+
+
+void ternary_model_evaluator::prune_by_probing(ptr_vector const& formulas, expr_ref_vector& model) {
+ unsigned sz1 = model.size();
for (unsigned i = 0; i < model.size(); ) {
expr_ref removed(model[i].get(), m);
if (i + 1 < model.size()) {
@@ -308,10 +313,10 @@ void ternary_model_evaluator::minimize_model(ptr_vector const & formulas,
m2.set_level(m_level2);
bool formulas_hold = check_model(formulas);
+
m1.set_level(m_level1);
m2.set_level(m_level2);
-
-
+
if (!formulas_hold) {
// if we introduced unknown, we restore the removed element
add_model(removed);
@@ -327,9 +332,147 @@ void ternary_model_evaluator::minimize_model(ptr_vector const & formulas,
i++;
}
}
- m1.reset();
- m2.reset();
- m_values.reset();
+ TRACE("pdr", tout << sz1 << " ==> " << model.size() << "\n";);
+}
+
+void ternary_model_evaluator::prune_by_cone_of_influence(ptr_vector const & formulas, expr_ref_vector& model) {
+ ptr_vector todo, tocollect;
+ todo.append(formulas);
+ m_visited.reset();
+ m1.set_level(m_level1);
+ m2.set_level(m_level2);
+
+ VERIFY(check_model(formulas));
+
+ while (!todo.empty()) {
+ app* e = to_app(todo.back());
+ todo.pop_back();
+ if (m_visited.is_marked(e)) {
+ continue;
+ }
+ unsigned v = is_true(e);
+ SASSERT(m.is_bool(e));
+ SASSERT(is_true(e) || is_false(e));
+ unsigned sz = e->get_num_args();
+ expr* const* args = e->get_args();
+ if (e->get_family_id() == m.get_basic_family_id()) {
+ switch(e->get_decl_kind()) {
+ case OP_TRUE:
+ break;
+ case OP_FALSE:
+ break;
+ case OP_EQ:
+ case OP_IFF:
+ if (e->get_arg(0) == e->get_arg(1)) {
+ // no-op
+ }
+ else if (!m.is_bool(e->get_arg(0))) {
+ tocollect.push_back(e);
+ }
+ else {
+ todo.append(sz, args);
+ }
+ break;
+ case OP_DISTINCT:
+ tocollect.push_back(e);
+ break;
+ case OP_ITE:
+ if (args[1] == args[2]) {
+ //
+ }
+ else if (is_true(args[1]) && is_true(args[2])) {
+ todo.append(2, args+1);
+ }
+ else if (is_false(args[2]) && is_false(args[2])) {
+ todo.append(2, args+1);
+ }
+ else if (is_true(args[0])) {
+ todo.push_back(args[0]);
+ todo.push_back(args[1]);
+ }
+ else {
+ SASSERT(is_false(args[0]));
+ todo.push_back(args[0]);
+ todo.push_back(args[2]);
+ }
+ break;
+ case OP_AND:
+ if (v) {
+ todo.append(sz, args);
+ }
+ else {
+ unsigned i = 0;
+ for (; !is_false(args[i]) && i < sz; ++i);
+ if (i == sz) {
+ fatal_error(1);
+ }
+ VERIFY(i < sz);
+ todo.push_back(args[i]);
+ }
+ break;
+ case OP_OR:
+ if (v) {
+ unsigned i = 0;
+ for (; !is_true(args[i]) && i < sz; ++i);
+ if (i == sz) {
+ fatal_error(1);
+ }
+ VERIFY(i < sz);
+ todo.push_back(args[i]);
+ }
+ else {
+ todo.append(sz, args);
+ }
+ break;
+ case OP_XOR:
+ case OP_NOT:
+ todo.append(sz, args);
+ break;
+ case OP_IMPLIES:
+ if (v) {
+ if (is_true(args[1])) {
+ todo.push_back(args[1]);
+ }
+ else if (is_false(args[0])) {
+ todo.push_back(args[0]);
+ }
+ else {
+ UNREACHABLE();
+ }
+ }
+ else {
+ todo.append(sz, args);
+ }
+ break;
+ default:
+ UNREACHABLE();
+ }
+ }
+ else {
+ tocollect.push_back(e);
+ }
+ m_visited.mark(e, true);
+ }
+ m1.set_level(m_level1);
+ m2.set_level(m_level2);
+ m_visited.reset();
+ for (unsigned i = 0; i < tocollect.size(); ++i) {
+ for_each_expr(*this, m_visited, tocollect[i]);
+ }
+ unsigned sz1 = model.size();
+ for (unsigned i = 0; i < model.size(); ++i) {
+ expr* e = model[i].get(), *var, *val;
+ if (get_assignment(e, var, val)) {
+ if (!m_visited.is_marked(var)) {
+ del_model(e);
+ model[i] = model.back();
+ model.pop_back();
+ --i;
+ }
+ }
+ }
+ m_visited.reset();
+ TRACE("pdr", tout << sz1 << " ==> " << model.size() << "\n";);
}
@@ -353,7 +496,7 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) {
#define ARG1 curr->get_arg(0)
#define ARG2 curr->get_arg(1)
- if (!UNKNOWN(curr)) {
+ if (!is_unknown(curr)) {
todo.pop_back();
continue;
}
@@ -363,16 +506,16 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) {
bool all_set = true, some_x = false;
for (unsigned i = 0; !some_x && i < arity; ++i) {
expr* arg = curr->get_arg(i);
- if (UNKNOWN(arg)) {
+ if (is_unknown(arg)) {
todo.push_back(arg);
all_set = false;
}
- else if (IS_X(arg)) {
+ else if (is_x(arg)) {
some_x = true;
}
}
if (some_x) {
- SET_X(curr);
+ set_x(curr);
}
else if (!all_set) {
continue;
@@ -381,105 +524,105 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) {
switch(curr->get_decl_kind()) {
case OP_NUM:
VERIFY(m_arith.is_numeral(curr,r));
- SET_VALUE(curr, r);
+ set_value(curr, r);
break;
case OP_IRRATIONAL_ALGEBRAIC_NUM:
- SET_X(curr);
+ set_x(curr);
break;
case OP_LE:
- SET_BOOL(curr, GET_VALUE(ARG1) <= GET_VALUE(ARG2));
+ set_bool(curr, get_value(ARG1) <= get_value(ARG2));
break;
case OP_GE:
- SET_BOOL(curr, GET_VALUE(ARG1) >= GET_VALUE(ARG2));
+ set_bool(curr, get_value(ARG1) >= get_value(ARG2));
break;
case OP_LT:
- SET_BOOL(curr, GET_VALUE(ARG1) < GET_VALUE(ARG2));
+ set_bool(curr, get_value(ARG1) < get_value(ARG2));
break;
case OP_GT:
- SET_BOOL(curr, GET_VALUE(ARG1) > GET_VALUE(ARG2));
+ set_bool(curr, get_value(ARG1) > get_value(ARG2));
break;
case OP_ADD:
r = rational::zero();
for (unsigned i = 0; i < arity; ++i) {
- r += GET_VALUE(curr->get_arg(i));
+ r += get_value(curr->get_arg(i));
}
- SET_VALUE(curr, r);
+ set_value(curr, r);
break;
case OP_SUB:
- r = GET_VALUE(curr->get_arg(0));
+ r = get_value(curr->get_arg(0));
for (unsigned i = 1; i < arity; ++i) {
- r -= GET_VALUE(curr->get_arg(i));
+ r -= get_value(curr->get_arg(i));
}
- SET_VALUE(curr, r);
+ set_value(curr, r);
break;
case OP_UMINUS:
SASSERT(arity == 1);
- SET_VALUE(curr, GET_VALUE(curr->get_arg(0)));
+ set_value(curr, get_value(curr->get_arg(0)));
break;
case OP_MUL:
r = rational::one();
for (unsigned i = 0; i < arity; ++i) {
- r *= GET_VALUE(curr->get_arg(i));
+ r *= get_value(curr->get_arg(i));
}
- SET_VALUE(curr, r);
+ set_value(curr, r);
break;
case OP_DIV:
SASSERT(arity == 2);
- r = GET_VALUE(ARG2);
+ r = get_value(ARG2);
if (r.is_zero()) {
- SET_X(curr);
+ set_x(curr);
}
else {
- SET_VALUE(curr, GET_VALUE(ARG1) / r);
+ set_value(curr, get_value(ARG1) / r);
}
break;
case OP_IDIV:
SASSERT(arity == 2);
- r = GET_VALUE(ARG2);
+ r = get_value(ARG2);
if (r.is_zero()) {
- SET_X(curr);
+ set_x(curr);
}
else {
- SET_VALUE(curr, div(GET_VALUE(ARG1), r));
+ set_value(curr, div(get_value(ARG1), r));
}
break;
case OP_REM:
// rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2)
SASSERT(arity == 2);
- r = GET_VALUE(ARG2);
+ r = get_value(ARG2);
if (r.is_zero()) {
- SET_X(curr);
+ set_x(curr);
}
else {
- r2 = mod(GET_VALUE(ARG1), r);
+ r2 = mod(get_value(ARG1), r);
if (r.is_neg()) r2.neg();
- SET_VALUE(curr, r2);
+ set_value(curr, r2);
}
break;
case OP_MOD:
SASSERT(arity == 2);
- r = GET_VALUE(ARG2);
+ r = get_value(ARG2);
if (r.is_zero()) {
- SET_X(curr);
+ set_x(curr);
}
else {
- SET_VALUE(curr, mod(GET_VALUE(ARG1), r));
+ set_value(curr, mod(get_value(ARG1), r));
}
break;
case OP_TO_REAL:
SASSERT(arity == 1);
- SET_VALUE(curr, GET_VALUE(ARG1));
+ set_value(curr, get_value(ARG1));
break;
case OP_TO_INT:
SASSERT(arity == 1);
- SET_VALUE(curr, floor(GET_VALUE(ARG1)));
+ set_value(curr, floor(get_value(ARG1)));
break;
case OP_IS_INT:
SASSERT(arity == 1);
- SET_BOOL(curr, GET_VALUE(ARG1).is_int());
+ set_bool(curr, get_value(ARG1).is_int());
break;
case OP_POWER:
- SET_X(curr);
+ set_x(curr);
break;
default:
UNREACHABLE();
@@ -496,213 +639,217 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) {
// we're adding unknowns on the top of the todo stack, if there is none added,
// all arguments were known
bool has_x = false, has_false = false;
+ unsigned sz = todo.size();
for (unsigned j = 0; !has_false && j < arity; ++j) {
expr * arg = curr->get_arg(j);
- if (IS_FALSE(arg)) {
+ if (is_false(arg)) {
has_false = true;
}
- else if (IS_X(arg)) {
+ else if (is_x(arg)) {
has_x = true;
}
- else if (UNKNOWN(arg)) {
+ else if (is_unknown(arg)) {
todo.push_back(arg);
}
}
if (has_false) {
- SET_FALSE(curr);
+ todo.resize(sz);
+ set_false(curr);
}
else {
if (todo.back() != curr) {
continue;
}
else if (has_x) {
- SET_X(curr);
+ set_x(curr);
}
else {
- SET_TRUE(curr);
+ set_true(curr);
}
}
}
else if (m.is_or(curr)) {
bool has_x = false, has_true = false;
+ unsigned sz = todo.size();
for (unsigned j = 0; !has_true && j < arity; ++j) {
expr * arg = curr->get_arg(j);
- if (IS_TRUE(arg)) {
+ if (is_true(arg)) {
has_true = true;
}
- else if (IS_X(arg)) {
+ else if (is_x(arg)) {
has_x = true;
}
- else if (UNKNOWN(arg)) {
+ else if (is_unknown(arg)) {
todo.push_back(arg);
}
}
if (has_true) {
- SET_TRUE(curr);
+ todo.resize(sz);
+ set_true(curr);
}
else {
if (todo.back() != curr) {
continue;
}
else if (has_x) {
- SET_X(curr);
+ set_x(curr);
}
else {
- SET_FALSE(curr);
+ set_false(curr);
}
}
}
else if (m.is_not(curr, arg)) {
- if (UNKNOWN(arg)) {
+ if (is_unknown(arg)) {
todo.push_back(arg);
continue;
}
- if (IS_TRUE(arg)) {
- SET_FALSE(curr);
+ if (is_true(arg)) {
+ set_false(curr);
}
- else if (IS_FALSE(arg)) {
- SET_TRUE(curr);
+ else if (is_false(arg)) {
+ set_true(curr);
}
else {
- SASSERT(IS_X(arg));
- SET_X(curr);
+ SASSERT(is_x(arg));
+ set_x(curr);
}
}
else if (m.is_implies(curr, arg1, arg2)) {
- if (IS_FALSE(arg1) || IS_TRUE(arg2)) {
- SET_TRUE(curr);
+ if (is_false(arg1) || is_true(arg2)) {
+ set_true(curr);
}
- else if (UNKNOWN(arg1) || UNKNOWN(arg2)) {
- if (UNKNOWN(arg1)) { todo.push_back(arg1); }
- if (UNKNOWN(arg2)) { todo.push_back(arg2); }
+ else if (is_unknown(arg1) || is_unknown(arg2)) {
+ if (is_unknown(arg1)) { todo.push_back(arg1); }
+ if (is_unknown(arg2)) { todo.push_back(arg2); }
continue;
}
- else if (IS_TRUE(arg1) && IS_FALSE(arg2)) {
- SET_FALSE(curr);
+ else if (is_true(arg1) && is_false(arg2)) {
+ set_false(curr);
}
else {
- SASSERT(IS_X(arg1) || IS_X(arg2));
- SET_X(curr);
+ SASSERT(is_x(arg1) || is_x(arg2));
+ set_x(curr);
}
}
else if (m.is_iff(curr, arg1, arg2) ||
(m.is_eq(curr, arg1, arg2) && m.is_bool(arg1))) {
- if (IS_X(arg1) || IS_X(arg2)) {
- SET_X(curr);
+ if (is_x(arg1) || is_x(arg2)) {
+ set_x(curr);
}
- else if (UNKNOWN(arg1) || UNKNOWN(arg2)) {
- if (UNKNOWN(arg1)) { todo.push_back(arg1); }
- if (UNKNOWN(arg2)) { todo.push_back(arg2); }
+ else if (is_unknown(arg1) || is_unknown(arg2)) {
+ if (is_unknown(arg1)) { todo.push_back(arg1); }
+ if (is_unknown(arg2)) { todo.push_back(arg2); }
continue;
}
else {
- bool val = IS_TRUE(arg1)==IS_TRUE(arg2);
- SASSERT(val == (IS_FALSE(arg1)==IS_FALSE(arg2)));
+ bool val = is_true(arg1)==is_true(arg2);
+ SASSERT(val == (is_false(arg1)==is_false(arg2)));
if (val) {
- SET_TRUE(curr);
+ set_true(curr);
}
else {
- SET_FALSE(curr);
+ set_false(curr);
}
}
}
else if (m.is_ite(curr, argCond, argThen, argElse) && m.is_bool(argThen)) {
- if (IS_TRUE(argCond)) {
- if (IS_TRUE(argThen)) { SET_TRUE(curr); }
- else if (IS_FALSE(argThen)) { SET_FALSE(curr); }
- else if (IS_X(argThen)) { SET_X(curr); }
+ if (is_true(argCond)) {
+ if (is_true(argThen)) { set_true(curr); }
+ else if (is_false(argThen)) { set_false(curr); }
+ else if (is_x(argThen)) { set_x(curr); }
else {
todo.push_back(argThen);
continue;
}
}
- else if (IS_FALSE(argCond)) {
- if (IS_TRUE(argElse)) { SET_TRUE(curr); }
- else if (IS_FALSE(argElse)) { SET_FALSE(curr); }
- else if (IS_X(argElse)) { SET_X(curr); }
+ else if (is_false(argCond)) {
+ if (is_true(argElse)) { set_true(curr); }
+ else if (is_false(argElse)) { set_false(curr); }
+ else if (is_x(argElse)) { set_x(curr); }
else {
todo.push_back(argElse);
continue;
}
}
- else if (IS_TRUE(argThen) && IS_TRUE(argElse)) {
- SET_TRUE(curr);
+ else if (is_true(argThen) && is_true(argElse)) {
+ set_true(curr);
}
- else if (IS_FALSE(argThen) && IS_FALSE(argElse)) {
- SET_FALSE(curr);
+ else if (is_false(argThen) && is_false(argElse)) {
+ set_false(curr);
}
- else if (IS_X(argCond) && (IS_X(argThen) || IS_X(argElse)) ) {
- SET_X(curr);
- } else if (UNKNOWN(argCond) || UNKNOWN(argThen) || UNKNOWN(argElse)) {
- if (UNKNOWN(argCond)) { todo.push_back(argCond); }
- if (UNKNOWN(argThen)) { todo.push_back(argThen); }
- if (UNKNOWN(argElse)) { todo.push_back(argElse); }
+ else if (is_x(argCond) && (is_x(argThen) || is_x(argElse)) ) {
+ set_x(curr);
+ } else if (is_unknown(argCond) || is_unknown(argThen) || is_unknown(argElse)) {
+ if (is_unknown(argCond)) { todo.push_back(argCond); }
+ if (is_unknown(argThen)) { todo.push_back(argThen); }
+ if (is_unknown(argElse)) { todo.push_back(argElse); }
continue;
}
else {
- SASSERT(IS_X(argCond));
- SASSERT((IS_TRUE(argThen) && IS_FALSE(argElse)) ||
- (IS_FALSE(argThen) && IS_TRUE(argElse)));
- SET_X(curr);
+ SASSERT(is_x(argCond));
+ SASSERT((is_true(argThen) && is_false(argElse)) ||
+ (is_false(argThen) && is_true(argElse)));
+ set_x(curr);
}
}
else if (m.is_true(curr)) {
- SET_TRUE(curr);
+ set_true(curr);
}
else if (m.is_false(curr)) {
- SET_FALSE(curr);
+ set_false(curr);
}
else if (m.is_eq(curr, arg1, arg2) && arg1 == arg2) {
- SET_TRUE(curr);
+ set_true(curr);
}
else if (m.is_eq(curr, arg1, arg2)) {
- if (UNKNOWN(arg1)) {
+ if (is_unknown(arg1)) {
todo.push_back(arg1);
}
- if (UNKNOWN(arg2)) {
+ if (is_unknown(arg2)) {
todo.push_back(arg2);
}
if (curr != todo.back()) {
continue;
}
- if (IS_X(arg1) || IS_X(arg2)) {
- SET_X(curr);
+ if (is_x(arg1) || is_x(arg2)) {
+ set_x(curr);
}
else {
- SET_BOOL(curr, GET_VALUE(arg1) == GET_VALUE(arg2));
+ set_bool(curr, get_value(arg1) == get_value(arg2));
}
}
else if (m.is_ite(curr, argCond, argThen, argElse) && m_arith.is_int_real(argThen)) {
- if (IS_TRUE(argCond) || (argThen == argElse)) {
- if (UNKNOWN(argThen)) {
+ if (is_true(argCond) || (argThen == argElse)) {
+ if (is_unknown(argThen)) {
todo.push_back(argThen);
continue;
}
- if (IS_X(argThen)) {
- SET_X(curr);
+ if (is_x(argThen)) {
+ set_x(curr);
}
else {
- SET_VALUE(curr, GET_VALUE(argThen));
+ set_value(curr, get_value(argThen));
}
}
- else if (IS_FALSE(argCond)) {
- if (UNKNOWN(argElse)) {
+ else if (is_false(argCond)) {
+ if (is_unknown(argElse)) {
todo.push_back(argElse);
continue;
}
- if (IS_X(argElse)) {
- SET_X(curr);
+ if (is_x(argElse)) {
+ set_x(curr);
}
else {
- SET_VALUE(curr, GET_VALUE(argElse));
+ set_value(curr, get_value(argElse));
}
}
- else if (UNKNOWN(argCond)) {
+ else if (is_unknown(argCond)) {
todo.push_back(argCond);
continue;
}
else {
- SET_X(curr);
+ set_x(curr);
}
}
else {
@@ -711,27 +858,27 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) {
}
else {
TRACE("pdr_verbse", tout << "Not evaluated " << mk_pp(curr, m) << "\n";);
- SET_X(curr);
+ set_x(curr);
}
IF_VERBOSE(35,verbose_stream() << "assigned "< const & formulas, expr_ref_vector& model);
+ void prune_by_probing(ptr_vector const & formulas, expr_ref_vector& model);
+
+ //00 -- non-visited
+ //01 -- X
+ //10 -- false
+ //11 -- true
+ inline bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); }
+ inline void set_unknown(expr* x) { m1.reset_mark(x); m2.reset_mark(x); }
+ inline bool is_x(expr* x) { return !m1.is_marked(x) && m2.is_marked(x); }
+ inline bool is_false(expr* x) { return m1.is_marked(x) && !m2.is_marked(x); }
+ inline bool is_true(expr* x) { return m1.is_marked(x) && m2.is_marked(x); }
+ inline void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); }
+ inline void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
+ inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
+ inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); }
+ inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } }
+ inline rational const& get_value(expr* x) const { return m_values.find(x); }
+ inline void set_value(expr* x, rational const& v) { set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_values.insert(x,v); }
+
protected:
bool check_model(ptr_vector const & formulas);
@@ -222,6 +245,9 @@ protected:
public:
ternary_model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m) {}
virtual void minimize_model(ptr_vector const & formulas, expr_ref_vector & model);
+
+ // for_each_expr visitor.
+ void operator()(expr* e) {}
};
void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res);
diff --git a/lib/proof_utils.cpp b/lib/proof_utils.cpp
new file mode 100644
index 000000000..6143e6746
--- /dev/null
+++ b/lib/proof_utils.cpp
@@ -0,0 +1,479 @@
+#include "dl_util.h"
+#include "proof_utils.h"
+#include "ast_smt2_pp.h"
+
+class reduce_hypotheses {
+ typedef obj_hashtable expr_set;
+ ast_manager& m;
+ expr_ref_vector m_refs;
+ obj_map m_cache;
+ obj_map m_units;
+ ptr_vector m_units_trail;
+ unsigned_vector m_limits;
+ obj_map m_hypmap;
+ ptr_vector m_hyprefs;
+ ptr_vector m_literals;
+
+ void reset() {
+ m_refs.reset();
+ m_cache.reset();
+ m_units.reset();
+ m_units_trail.reset();
+ m_limits.reset();
+ std::for_each(m_hyprefs.begin(), m_hyprefs.end(), delete_proc());
+ m_hypmap.reset();
+ m_hyprefs.reset();
+ m_literals.reset();
+ }
+
+ void push() {
+ m_limits.push_back(m_units_trail.size());
+ }
+
+ void pop() {
+ unsigned sz = m_limits.back();
+ while (m_units_trail.size() > sz) {
+ m_units.remove(m_units_trail.back());
+ m_units_trail.pop_back();
+ }
+ m_limits.pop_back();
+ }
+
+ void get_literals(expr* clause) {
+ m_literals.reset();
+ if (m.is_or(clause)) {
+ m_literals.append(to_app(clause)->get_num_args(), to_app(clause)->get_args());
+ }
+ else {
+ m_literals.push_back(clause);
+ }
+ }
+
+ void add_hypotheses(proof* p) {
+ expr_set* hyps = 0;
+ bool inherited = false;
+ if (p->get_decl_kind() == PR_HYPOTHESIS) {
+ hyps = alloc(expr_set);
+ hyps->insert(m.get_fact(p));
+ m_hyprefs.push_back(hyps);
+ }
+ else {
+ for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+ expr_set* hyps1 = m_hypmap.find(m.get_parent(p, i));
+ if (hyps1) {
+ if (!hyps) {
+ hyps = hyps1;
+ inherited = true;
+ continue;
+ }
+ if (inherited) {
+ hyps = alloc(expr_set,*hyps);
+ m_hyprefs.push_back(hyps);
+ inherited = false;
+ }
+ datalog::set_union(*hyps, *hyps1);
+ }
+ }
+ }
+ m_hypmap.insert(p, hyps);
+ }
+
+ expr_ref complement_lit(expr* e) {
+ expr* e1;
+ if (m.is_not(e, e1)) {
+ return expr_ref(e1, m);
+ }
+ else {
+ return expr_ref(m.mk_not(e), m);
+ }
+ }
+
+ bool in_hypotheses(expr* e, expr_set* hyps) {
+ if (!hyps) {
+ return false;
+ }
+ expr_ref not_e = complement_lit(e);
+ return hyps->contains(not_e);
+ }
+
+ bool contains_hypothesis(proof* p) {
+ ptr_vector todo;
+ ast_mark visit;
+ todo.push_back(p);
+ while (!todo.empty()) {
+ p = todo.back();
+ todo.pop_back();
+ if (visit.is_marked(p)) {
+ continue;
+ }
+ visit.mark(p, true);
+ if (PR_HYPOTHESIS == p->get_decl_kind()) {
+ return true;
+ }
+ for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+ todo.push_back(m.get_parent(p, i));
+ }
+ }
+ return false;
+ }
+
+ bool is_closed(proof* p) {
+ expr_set* hyps = m_hypmap.find(p);
+ return !hyps || hyps->empty();
+ }
+
+public:
+ reduce_hypotheses(ast_manager& m): m(m), m_refs(m) {}
+
+ void operator()(proof_ref& pr) {
+ proof_ref tmp(m);
+ tmp = pr;
+ elim(pr);
+ reset();
+ CTRACE("proof_utils", contains_hypothesis(pr),
+ tout << "Contains hypothesis:\n";
+ tout << mk_ismt2_pp(tmp, m) << "\n====>\n";
+ tout << mk_ismt2_pp(pr, m) << "\n";);
+
+ }
+
+ void elim(proof_ref& p) {
+ proof_ref tmp(m);
+ proof* result = p.get();
+ if (m_cache.find(p, result)) {
+ p = result;
+ return;
+ }
+ switch(p->get_decl_kind()) {
+ case PR_HYPOTHESIS:
+ if (!m_units.find(m.get_fact(p), result)) {
+ result = p.get();
+ }
+ add_hypotheses(result);
+ break;
+ case PR_LEMMA: {
+ SASSERT(m.get_num_parents(p) == 1);
+ tmp = m.get_parent(p, 0);
+ elim(tmp);
+ get_literals(m.get_fact(p));
+ expr_set* hyps = m_hypmap.find(tmp);
+ expr_set* new_hyps = 0;
+ if (hyps) {
+ new_hyps = alloc(expr_set, *hyps);
+ }
+ for (unsigned i = 0; i < m_literals.size(); ++i) {
+ expr* e = m_literals[i];
+ if (!in_hypotheses(e, hyps)) {
+ m_literals[i] = m_literals.back();
+ m_literals.pop_back();
+ --i;
+ }
+ else {
+ SASSERT(new_hyps);
+ expr_ref not_e = complement_lit(e);
+ SASSERT(new_hyps->contains(not_e));
+ new_hyps->remove(not_e);
+ }
+ }
+ if (m_literals.empty()) {
+ result = tmp;
+ }
+ else {
+ expr_ref clause(m);
+ if (m_literals.size() == 1) {
+ clause = m_literals[0];
+ }
+ else {
+ clause = m.mk_or(m_literals.size(), m_literals.c_ptr());
+ }
+ tmp = m.mk_lemma(tmp, clause);
+ m_refs.push_back(tmp);
+ result = tmp;
+ }
+ if (new_hyps && new_hyps->empty()) {
+ dealloc(new_hyps);
+ new_hyps = 0;
+ }
+ m_hypmap.insert(result, new_hyps);
+ m_hyprefs.push_back(new_hyps);
+ TRACE("proof_utils",
+ tout << "New lemma: " << mk_pp(m.get_fact(p), m)
+ << "\n==>\n"
+ << mk_pp(m.get_fact(result), m) << "\n";
+ if (hyps) {
+ expr_set::iterator it = hyps->begin();
+ expr_set::iterator end = hyps->end();
+ for (; it != end; ++it) {
+ tout << "Hypothesis: " << mk_pp(*it, m) << "\n";
+ }
+ });
+
+ break;
+ }
+ case PR_UNIT_RESOLUTION: {
+ proof_ref_vector parents(m);
+ parents.push_back(m.get_parent(p, 0));
+ push();
+ bool found_false = false;
+ for (unsigned i = 1; i < m.get_num_parents(p); ++i) {
+ tmp = m.get_parent(p, i);
+ elim(tmp);
+ if (m.is_false(m.get_fact(tmp))) {
+ result = tmp;
+ found_false = true;
+ break;
+ }
+ SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
+ parents.push_back(tmp);
+ if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
+ m_units.insert(m.get_fact(tmp), tmp);
+ m_units_trail.push_back(m.get_fact(tmp));
+ }
+ }
+ if (found_false) {
+ pop();
+ break;
+ }
+ tmp = m.get_parent(p, 0);
+ elim(tmp);
+ parents[0] = tmp;
+ expr* clause = m.get_fact(tmp);
+ if (m.is_false(clause)) {
+ m_refs.push_back(tmp);
+ result = tmp;
+ pop();
+ break;
+ }
+ get_literals(clause);
+ for (unsigned i = 1; i < parents.size(); ++i) {
+ bool found = false;
+ for (unsigned j = 0; j < m_literals.size(); ++j) {
+ if (m.is_complement(m_literals[j], m.get_fact(parents[i].get()))) {
+ found = true;
+ break;
+ }
+ }
+ if (!found) {
+ // literal was removed as hypothesis.
+ parents[i] = parents.back();
+ parents.pop_back();
+ --i;
+ }
+ }
+ if (parents.size() == 1) {
+ result = parents[0].get();
+ }
+ else {
+ result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
+ m_refs.push_back(result);
+ add_hypotheses(result);
+ }
+ pop();
+ break;
+ }
+ default: {
+ ptr_buffer args;
+ bool change = false;
+ bool found_false = false;
+ for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+ tmp = m.get_parent(p, i);
+ elim(tmp);
+ if (m.is_false(m.get_fact(tmp))) {
+ result = tmp;
+ found_false = true;
+ break;
+ }
+ SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
+ change = change || (tmp != m.get_parent(p, i));
+ args.push_back(tmp);
+ }
+ if (found_false) {
+ break;
+ }
+ if (m.has_fact(p)) {
+ args.push_back(m.get_fact(p));
+ }
+ if (change) {
+ tmp = m.mk_app(p->get_decl(), args.size(), args.c_ptr());
+ m_refs.push_back(tmp);
+ }
+ else {
+ tmp = p;
+ }
+ result = tmp;
+ add_hypotheses(result);
+ break;
+ }
+ }
+ SASSERT(m_hypmap.contains(result));
+ m_cache.insert(p, result);
+ p = result;
+ }
+};
+
+void proof_utils::reduce_hypotheses(proof_ref& pr) {
+ class reduce_hypotheses reduce(pr.get_manager());
+ reduce(pr);
+ SASSERT(is_closed(pr.get_manager(), pr));
+}
+
+class proof_is_closed {
+ ast_manager& m;
+ ptr_vector m_literals;
+ ast_mark m_visit;
+
+ void reset() {
+ m_literals.reset();
+ m_visit.reset();
+ }
+
+ bool check(proof* p) {
+ // really just a partial check because nodes may be visited
+ // already under a different lemma scope.
+ if (m_visit.is_marked(p)) {
+ return true;
+ }
+ bool result = false;
+ m_visit.mark(p, true);
+ switch(p->get_decl_kind()) {
+ case PR_LEMMA: {
+ unsigned sz = m_literals.size();
+ expr* cls = m.get_fact(p);
+ m_literals.push_back(cls);
+ if (m.is_or(cls)) {
+ m_literals.append(to_app(cls)->get_num_args(), to_app(cls)->get_args());
+ }
+ SASSERT(m.get_num_parents(p) == 1);
+ result = check(m.get_parent(p, 0));
+ m_literals.resize(sz);
+ break;
+ }
+ case PR_HYPOTHESIS: {
+ expr* fact = m.get_fact(p);
+ for (unsigned i = 0; i < m_literals.size(); ++i) {
+ if (m.is_complement(m_literals[i], fact)) {
+ result = true;
+ break;
+ }
+ }
+ break;
+ }
+ default:
+ result = true;
+ for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+ if (!check(m.get_parent(p, i))) {
+ result = false;
+ break;
+ }
+ }
+ break;
+ }
+
+ return result;
+ }
+
+public:
+ proof_is_closed(ast_manager& m): m(m) {}
+
+ bool operator()(proof *p) {
+ bool ok = check(p);
+ reset();
+ return ok;
+ }
+};
+
+bool proof_utils::is_closed(ast_manager& m, proof* p) {
+ proof_is_closed checker(m);
+ return checker(p);
+}
+
+
+static void 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);
+ if (cache.find(pr, pr2)) {
+ pr = pr2;
+ return;
+ }
+
+ for (unsigned i = 0; i < m.get_num_parents(pr); ++i) {
+ prNew = m.get_parent(pr, i);
+ permute_unit_resolution(refs, cache, prNew);
+ parents.push_back(prNew);
+ }
+
+ prNew = pr;
+ if (pr->get_decl_kind() == PR_UNIT_RESOLUTION &&
+ parents[0]->get_decl_kind() == PR_TH_LEMMA) {
+ /*
+ Unit resolution:
+ T1: (or l_1 ... l_n l_1' ... l_m')
+ T2: (not l_1)
+ ...
+ T(n+1): (not l_n)
+ [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
+ Th lemma:
+ T1: (not l_1)
+ ...
+ Tn: (not l_n)
+ [th-lemma T1 ... Tn]: (or l_{n+1} ... l_m)
+
+ Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom.
+
+ Implement conversion:
+
+ T1 |- not l_1 ... Tn |- not l_n
+ ------------------------------- TH_LEMMA
+ (or k_1 .. k_m j_1 ... j_m) S1 |- not k_1 ... Sm |- not k_m
+ -------------------------------------------------------------- UNIT_RESOLUTION
+ (or j_1 .. j_m)
+
+
+ |->
+
+ T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m
+ ---------------------------------------------------------------- TH_LEMMA
+ (or j_1 .. j_m)
+
+ */
+ proof_ref_vector premises(m);
+ proof* thLemma = parents[0].get();
+ for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) {
+ premises.push_back(m.get_parent(thLemma, i));
+ }
+ for (unsigned i = 1; i < parents.size(); ++i) {
+ premises.push_back(parents[i].get());
+ }
+ parameter const* params = thLemma->get_decl()->get_parameters();
+ unsigned num_params = thLemma->get_decl()->get_num_parameters();
+ SASSERT(params[0].is_symbol());
+ family_id tid = m.get_family_id(params[0].get_symbol());
+ SASSERT(tid != null_family_id);
+ prNew = m.mk_th_lemma(tid, m.get_fact(pr),
+ premises.size(), premises.c_ptr(), num_params-1, params+1);
+ }
+ else {
+ ptr_vector args;
+ for (unsigned i = 0; i < parents.size(); ++i) {
+ args.push_back(parents[i].get());
+ }
+ if (m.has_fact(pr)) {
+ args.push_back(m.get_fact(pr));
+ }
+ prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr());
+ }
+
+ cache.insert(pr, prNew);
+ refs.push_back(prNew);
+ pr = prNew;
+}
+
+
+// permute unit resolution over Theory lemmas to track premises.
+void proof_utils::permute_unit_resolution(proof_ref& pr) {
+ expr_ref_vector refs(pr.get_manager());
+ obj_map cache;
+ ::permute_unit_resolution(refs, cache, pr);
+}
diff --git a/lib/proof_utils.h b/lib/proof_utils.h
new file mode 100644
index 000000000..a193f6821
--- /dev/null
+++ b/lib/proof_utils.h
@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ proof_utils.h
+
+Abstract:
+
+ Utilities for transforming proofs.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2012-10-12.
+
+Revision History:
+
+--*/
+#ifndef _PROOF_UTILS_H_
+#define _PROOF_UTILS_H_
+
+class proof_utils {
+public:
+ /**
+ \brief reduce the set of hypotheses used in the proof.
+ */
+ static void reduce_hypotheses(proof_ref& pr);
+
+ /**
+ \brief Check that a proof does not contain open hypotheses.
+ */
+ static bool is_closed(ast_manager& m, proof* p);
+
+ /**
+ \brief Permute unit resolution rule with th-lemma
+ */
+ static void permute_unit_resolution(proof_ref& pr);
+
+};
+
+#endif _PROOF_UTILS_H_
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) {