diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp index 8dbb766a9..552f8231e 100644 --- a/lib/pdr_context.cpp +++ b/lib/pdr_context.cpp @@ -914,7 +914,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); } @@ -1108,6 +1108,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 @@ -1604,10 +1619,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",true), n); break; } case l_undef: { diff --git a/lib/pdr_context.h b/lib/pdr_context.h index 3fdb067d6..42572bb1e 100644 --- a/lib/pdr_context.h +++ b/lib/pdr_context.h @@ -171,10 +171,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 +184,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; } @@ -245,6 +248,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 { }; diff --git a/lib/pdr_dl_interface.cpp b/lib/pdr_dl_interface.cpp index 900ee89c0..85b73e362 100644 --- a/lib/pdr_dl_interface.cpp +++ b/lib/pdr_dl_interface.cpp @@ -184,35 +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 true) 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"); - 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)"); - - + 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 5586fa2ca..c5dfd62f3 100644 --- a/lib/pdr_farkas_learner.cpp +++ b/lib/pdr_farkas_learner.cpp @@ -227,8 +227,7 @@ namespace pdr { : m_proof_params(get_proof_params(params)), m_pr(PROOF_MODE), p2o(m_pr, outer_mgr), - o2p(outer_mgr, m_pr), - m_simplifier(mk_arith_bounds_tactic(outer_mgr)) + o2p(outer_mgr, m_pr) { m_pr.register_decl_plugins(); m_ctx = alloc(smt::solver, m_pr, m_proof_params); @@ -322,7 +321,6 @@ namespace pdr { for (unsigned i = 0; i < ilemmas.size(); ++i) { lemmas.push_back(p2o(ilemmas[i].get())); } - simplify_lemmas(lemmas); } m_ctx->pop(1); @@ -358,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) { @@ -369,9 +368,10 @@ namespace pdr { } model_converter_ref mc; proof_converter_ref pc; - expr_dependency_ref core(lemmas.get_manager()); + 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]; @@ -502,6 +502,9 @@ namespace pdr { units under Farkas. */ + +#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); @@ -514,11 +517,12 @@ namespace pdr { proof_ref pr(root, m); proof_utils::reduce_hypotheses(pr); - IF_VERBOSE(3, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(pr, m) << "\n";); 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); @@ -574,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(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); } } @@ -707,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); } } @@ -717,9 +723,10 @@ 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; @@ -740,10 +747,11 @@ 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); } } diff --git a/lib/pdr_farkas_learner.h b/lib/pdr_farkas_learner.h index c0303777c..e068b5537 100644 --- a/lib/pdr_farkas_learner.h +++ b/lib/pdr_farkas_learner.h @@ -43,7 +43,6 @@ class farkas_learner { front_end_params m_proof_params; ast_manager m_pr; scoped_ptr m_ctx; - scoped_ptr m_simplifier; static front_end_params get_proof_params(front_end_params& orig_params); @@ -67,7 +66,7 @@ class farkas_learner { bool is_farkas_lemma(ast_manager& m, expr* e); - void get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, expr_ref_vector& lemmas); + void 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; diff --git a/lib/pdr_generalizers.cpp b/lib/pdr_generalizers.cpp index a7f1922b4..655a98967 100644 --- a/lib/pdr_generalizers.cpp +++ b/lib/pdr_generalizers.cpp @@ -100,7 +100,7 @@ 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)) { + while (i < core.size() && 1 < core.size() && (!m_failure_limit || num_failures <= m_failure_limit)) { expr_ref lit(m), state(m); lit = core[i].get(); core[i] = m.mk_true(); @@ -111,16 +111,18 @@ namespace pdr { core[i] = core.back(); core.pop_back(); TRACE("pdr", tout << "Remove: " << mk_pp(lit, m) << "\n";); + IF_VERBOSE(3, verbose_stream() << "remove: " << mk_pp(lit, m) << "\n";); ++num_changes; uses_level = uses_level_tmp; } else { + IF_VERBOSE(3, verbose_stream() << "keep: " << mk_pp(lit, m) << "\n";); core[i] = lit; ++num_failures; ++i; } } - IF_VERBOSE(1, verbose_stream() << "changes: " << num_changes << " size: " << core.size() << "\n";); + IF_VERBOSE(2, verbose_stream() << "changes: " << num_changes << " size: " << core.size() << "\n";); TRACE("pdr", tout << "changes: " << num_changes << " index: " << i << " size: " << core.size() << "\n";); }