mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge branch 'working' of //z3-1/z3 into working

Browse source
This commit is contained in:
Leonardo de Moura 2012-10-15 10:08:02 -07:00
parent 4efe38a71d bdad4e3bcb
commit f7f2a77504
21 changed files with 1394 additions and 592 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
lib/ast.cpp
View file

@ -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));
}
}

4
lib/ast.h
View file

@ -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); }

14
lib/ast_smt_pp.cpp
View file

@ -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 << ")";

8
lib/dl_bmc_engine.cpp
View file

@ -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;
}

3
lib/dl_check_table.cpp
View file

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

2
lib/lib.vcxproj
View file

@ -736,6 +736,7 @@
<ClCompile Include="propagate_ineqs_tactic.cpp" />
<ClCompile Include="proof_checker.cpp" />
<ClCompile Include="proof_converter.cpp" />
<ClCompile Include="proof_utils.cpp" />
<ClCompile Include="proto_model.cpp" />
<ClCompile Include="pdecl.cpp" />
<ClCompile Include="pull_ite_tree.cpp" />
@ -1151,6 +1152,7 @@
<ClInclude Include="preprocessor.h" />
<ClInclude Include="preprocessor_params.h" />
<ClInclude Include="proof_checker.h" />
<ClInclude Include="proof_utils.h" />
<ClInclude Include="pull_ite_tree.h" />
<ClInclude Include="pull_quant.h" />
<ClInclude Include="push_app_ite.h" />

242
lib/pdr_context.cpp
View file

@ -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<func_decl> 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<expr, unsigned>& 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<model_node*>::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<model_generalizer>());
std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc<core_generalizer>());
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<model_generalizer>());
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<core_generalizer>());
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: {

22
lib/pdr_context.h
View file

@ -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<model_node> 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<model_node> 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:
/**

39
lib/pdr_dl_interface.cpp
View file

@ -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"););
}

186
lib/pdr_farkas_learner.cpp
View file

@ -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<equality_expander_cfg> 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<equality_expander_cfg> 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<expr_set> hyprefs;
obj_map<expr, expr_set*> hypmap;
obj_hashtable<expr> 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<expr_set>());
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<expr>& lemma_set, expr_ref_vector& lemmas) {
ast_manager& m = lemmas.get_manager();
ast_mark visited;
proof* p0 = p;
ptr_vector<proof> 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<proof,proof*> cache;
permute_unit_resolution(refs, cache, pr);
}
void farkas_learner::permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>& 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<expr> 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;

30
lib/pdr_farkas_learner.h
View file

@ -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> 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<smt::solver> m_ctx;
scoped_ptr<tactic> 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<proof,proof*>& 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<expr>& 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);

24
lib/pdr_generalizers.cpp
View file

@ -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<expr> 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";);
}
//

319
lib/pdr_prop_solver.cpp
View file

@ -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<app,expr *> m_fresh2expr;
obj_map<expr, app*> m_expr2fresh;
unsigned m_num_fresh;
expr_ref_vector m_assumptions;
obj_map<app,expr *> m_proxies2expr;
obj_map<expr, app*> m_expr2proxies;
obj_hashtable<expr> 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<func_decl> 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<app,expr*>::iterator it = m_proxies2expr.begin(), end = m_proxies2expr.end();
for (; it != end; ++it) {
sub.insert(it->m_key, m.mk_true(), pr);
}
scoped_ptr<expr_replacer> 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<bool> _model(m_fparams.m_model, mdl != 0);
flet<bool> _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<expr> 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

39
lib/pdr_prop_solver.h
View file

@ -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<expr> 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;

4
lib/pdr_smt_context_manager.cpp
View file

@ -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) {}

3
lib/pdr_smt_context_manager.h
View file

@ -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.

497
lib/pdr_util.cpp
View file

@ -206,50 +206,49 @@ void th_rewriter_model_evaluator::check_model(ptr_vector<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> const & formulas, expr_ref_vector& model) {
ptr_vector<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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 "<<mk_pp(curr_e,m)
<<(IS_TRUE(curr_e) ? "true" : IS_FALSE(curr_e) ? "false" : "unknown") << "\n";);
SASSERT(!UNKNOWN(curr));
<<(is_true(curr_e) ? "true" : is_false(curr_e) ? "false" : "unknown") << "\n";);
SASSERT(!is_unknown(curr));
todo.shrink(pre_curr_depth);
}
bool has_unknown = false;
for (unsigned i = 0; i < formulas.size(); ++i) {
expr * form = formulas[i];
SASSERT(!UNKNOWN(form));
SASSERT(!is_unknown(form));
TRACE("pdr_verbose",
tout << "formula is " << (IS_TRUE(form) ? "true" : IS_FALSE(form) ? "false" : "unknown") << "\n" <<mk_pp(form, m)<< "\n";);
tout << "formula is " << (is_true(form) ? "true" : is_false(form) ? "false" : "unknown") << "\n" <<mk_pp(form, m)<< "\n";);
if (IS_FALSE(form)) {
if (is_false(form)) {
IF_VERBOSE(2, verbose_stream() << "formula false in model: "<<mk_pp(form, m) << "\n";);
UNREACHABLE();
}
if (IS_X(form)) {
if (is_x(form)) {
has_unknown = true;
}
}

26
lib/pdr_util.h
View file

@ -207,10 +207,33 @@ class ternary_model_evaluator : public model_evaluator_base {
ast_fast_mark2 m2;
unsigned m_level1;
unsigned m_level2;
expr_mark m_visited;
void setup_model(expr_ref_vector const& model);
void add_model(expr* e);
void del_model(expr* e);
bool get_assignment(expr* e, expr*& var, expr*& val);
void prune_by_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model);
void prune_by_probing(ptr_vector<expr> 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<expr> 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<expr> 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);

479
lib/proof_utils.cpp Normal file
View file

@ -0,0 +1,479 @@
#include "dl_util.h"
#include "proof_utils.h"
#include "ast_smt2_pp.h"
class reduce_hypotheses {
typedef obj_hashtable<expr> expr_set;
ast_manager& m;
expr_ref_vector m_refs;
obj_map<proof,proof*> m_cache;
obj_map<expr, proof*> m_units;
ptr_vector<expr> m_units_trail;
unsigned_vector m_limits;
obj_map<proof, expr_set*> m_hypmap;
ptr_vector<expr_set> m_hyprefs;
ptr_vector<expr> 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<expr_set>());
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<proof> 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<expr> 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<expr> 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<proof,proof*>& 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<expr> 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<proof,proof*> cache;
::permute_unit_resolution(refs, cache, pr);
}

41
lib/proof_utils.h Normal file
View file

@ -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_

1
lib/unit_subsumption_tactic.cpp
View file

@ -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) {