diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp index af5dbe54d..4f8f27fca 100644 --- a/lib/pdr_context.cpp +++ b/lib/pdr_context.cpp @@ -1303,9 +1303,6 @@ namespace pdr { 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)); } @@ -1689,32 +1686,60 @@ namespace pdr { Goal is to find phi0(x0), phi1(x1) such that: - phi(x) & phi0(x0) & phi1(x1) => psi(x0, x1, x) + phi(x) & phi0(x0) & phi1(x1) => psi(x0, x1, x) + + or at least (ignoring psi alltogether): + + phi(x) & phi0(x0) & phi1(x1) => T(x0, x1, x) Strategy: - - perform cheap existential quantifier elimination on - exists x . T(x0,x1,x) & phi(x) - (e.g., destructive equality resolution) + - Extract literals from T & phi using ternary simulation with M. + - resulting formula is Phi. + + - perform cheap existential quantifier elimination on + Phi <- exists x . Phi(x0,x1,x) + (e.g., destructive equality resolution) + + - Sub-strategy 1: rename remaining x to fresh variables. + - Sub-strategy 2: replace remaining x to M(x). + + - For each literal L in result: + + - if L is x0 pure, add L to L0 + - if L is x1 pure, add L to L1 + - if L mixes x0, x1, add x1 = M(x1) to L1, add L(x1 |-> M(x1)) to L0 + + - Create sub-goals for L0 and L1. - - pull equalities that use - - */ void context::create_children2(model_node& n, expr* psi) { SASSERT(n.level() > 0); - + + pred_transformer& pt = n.pt(); model_core const& M = n.model(); - datalog::rule const& r = n.pt().find_rule(M); - expr* T = n.pt().get_transition(r); + datalog::rule const& r = pt.find_rule(M); + expr* T = pt.get_transition(r); expr* phi = n.state(); - expr_ref_vector Ts(m); - datalog::flatten_and(T, Ts); + ternary_model_evaluator tmev(m); + expr_ref_vector mdl(m); + ptr_vector forms; + forms.push_back(T); + forms.push_back(phi); + datalog::flatten_and(psi, mdl); + expr_ref_vector Phi = tmev.minimize_literals(forms, mdl); ptr_vector preds; - n.pt().find_predecessors(r, preds); - n.pt().remove_predecessors(Ts); + pt.find_predecessors(r, preds); + pt.remove_predecessors(Phi); + + expr_ref_vector vars(m); + unsigned sig_size = pt.head()->get_arity(); + for (unsigned i = 0; i < sig_size; ++i) { + vars.push_back(m.mk_const(m_pm.o2n(pt.sig(i), 0))); + } + // TBD: reduce_vars(vars, Phi); // TBD ... TRACE("pdr", m_search.display(tout);); diff --git a/lib/pdr_context.h b/lib/pdr_context.h index b2cd17f84..ce01c3100 100644 --- a/lib/pdr_context.h +++ b/lib/pdr_context.h @@ -70,10 +70,10 @@ namespace pdr { ptr_vector m_rules; // rules used to derive transformer prop_solver m_solver; // solver context vector m_levels; // level formulas - expr_ref_vector m_invariants; // properties that are invariant. - obj_map m_prop2level; // map property to level where it occurs. + expr_ref_vector m_invariants; // properties that are invariant. + obj_map m_prop2level; // map property to level where it occurs. obj_map m_tag2rule; // map tag predicate to rule. - rule2expr m_rule2tag; // map rule to predicate tag. + rule2expr m_rule2tag; // map rule to predicate tag. qinst_map m_rule2qinst; // map tag to quantifier instantiation. rule2inst m_rule2inst; // map rules to instantiations of indices rule2expr m_rule2transition; // map rules to transition diff --git a/lib/pdr_dl_interface.cpp b/lib/pdr_dl_interface.cpp index d7952fec3..d26ce5a4d 100644 --- a/lib/pdr_dl_interface.cpp +++ b/lib/pdr_dl_interface.cpp @@ -202,7 +202,6 @@ void dl_interface::collect_params(param_descrs& p) { 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"); p.insert(":unfold-rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring"); - 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-inductive-generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening");); diff --git a/lib/pdr_generalizers.cpp b/lib/pdr_generalizers.cpp index d3db59d39..6de57b39f 100644 --- a/lib/pdr_generalizers.cpp +++ b/lib/pdr_generalizers.cpp @@ -121,10 +121,6 @@ namespace pdr { TRACE("pdr", tout << "old size: " << old_core_size << " new size: " << core.size() << "\n";); } - // - // extract multiple cores from unreachable state. - // - void core_multi_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { UNREACHABLE(); @@ -567,78 +563,4 @@ namespace pdr { uses_level = true; } } - - - // - // cube => n.state() & formula - // so n.state() & cube & ~formula is unsat - // so weaken cube while result is still unsat. - // - void model_farkas_generalizer::operator()(model_node& n, expr_ref_vector& cube) { - ast_manager& m = n.pt().get_manager(); - manager& pm = n.pt().get_pdr_manager(); - front_end_params& p = m_ctx.get_fparams(); - farkas_learner learner(p, m); - expr_ref A0(m), A(m), B(m), state(m); - expr_ref_vector states(m); - - A0 = n.pt().get_formulas(n.level(), true); - - // extract substitution for next-state variables. - expr_substitution sub(m); - solve_for_next_vars(A0, n, sub); - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - (*rep)(A0); - A0 = m.mk_not(A0); - - state = n.state(); - (*rep)(state); - - datalog::flatten_and(state, states); - - ptr_vector preds; - n.pt().find_predecessors(n.model(), preds); - - TRACE("pdr", for (unsigned i = 0; i < cube.size(); ++i) tout << mk_pp(cube[i].get(), m) << "\n";); - - for (unsigned i = 0; i < preds.size(); ++i) { - pred_transformer& pt = m_ctx.get_pred_transformer(preds[i]); - SASSERT(pt.head() == preds[i]); - expr_ref_vector lemmas(m), o_cube(m), other(m), o_state(m), other_state(m); - pm.partition_o_atoms(cube, o_cube, other, i); - pm.partition_o_atoms(states, o_state, other_state, i); - TRACE("pdr", - tout << "cube:\n"; - for (unsigned i = 0; i < cube.size(); ++i) tout << mk_pp(cube[i].get(), m) << "\n"; - tout << "o_cube:\n"; - for (unsigned i = 0; i < o_cube.size(); ++i) tout << mk_pp(o_cube[i].get(), m) << "\n"; - tout << "other:\n"; - for (unsigned i = 0; i < other.size(); ++i) tout << mk_pp(other[i].get(), m) << "\n"; - tout << "o_state:\n"; - for (unsigned i = 0; i < o_state.size(); ++i) tout << mk_pp(o_state[i].get(), m) << "\n"; - tout << "other_state:\n"; - for (unsigned i = 0; i < other_state.size(); ++i) tout << mk_pp(other_state[i].get(), m) << "\n"; - ); - A = m.mk_and(A0, pm.mk_and(other), pm.mk_and(other_state)); - B = m.mk_and(pm.mk_and(o_cube), pm.mk_and(o_state)); - - TRACE("pdr", - tout << "A: " << mk_pp(A, m) << "\n"; - tout << "B: " << mk_pp(B, m) << "\n";); - - if (learner.get_lemma_guesses(A, B, lemmas)) { - cube.append(lemmas); - cube.append(o_state); - TRACE("pdr", - tout << "New lemmas:\n"; - for (unsigned i = 0; i < lemmas.size(); ++i) { - tout << mk_pp(lemmas[i].get(), m) << "\n"; - } - ); - } - } - TRACE("pdr", for (unsigned i = 0; i < cube.size(); ++i) tout << mk_pp(cube[i].get(), m) << "\n";); - } - }; diff --git a/lib/pdr_generalizers.h b/lib/pdr_generalizers.h index 22d9784c7..5a1d9a0e4 100644 --- a/lib/pdr_generalizers.h +++ b/lib/pdr_generalizers.h @@ -57,13 +57,6 @@ namespace pdr { virtual void operator()(model_node& n, expr_ref_vector& cube); }; - class model_farkas_generalizer : public model_generalizer { - public: - model_farkas_generalizer(context& ctx) : model_generalizer(ctx) {} - virtual ~model_farkas_generalizer() {} - virtual void operator()(model_node& n, expr_ref_vector& cube); - }; - class model_evaluation_generalizer : public model_generalizer { th_rewriter_model_evaluator m_model_evaluator; public: diff --git a/lib/pdr_util.cpp b/lib/pdr_util.cpp index 04ad64851..5deb2a189 100644 --- a/lib/pdr_util.cpp +++ b/lib/pdr_util.cpp @@ -299,6 +299,35 @@ void ternary_model_evaluator::minimize_model(ptr_vector const & formulas, m_values.reset(); } +expr_ref_vector ternary_model_evaluator::minimize_literals(ptr_vector const& formulas, expr_ref_vector const& model) { + + setup_model(model); + + expr_ref_vector result(m); + ptr_vector tocollect; + m_visited.reset(); + m1.set_level(m_level1); + m2.set_level(m_level2); + + VERIFY(check_model(formulas)); + collect(formulas, tocollect); + for (unsigned i = 0; i < tocollect.size(); ++i) { + expr* e = tocollect[i]; + SASSERT(m.is_bool(e)); + SASSERT(is_true(e) || is_false(e)); + if (is_true(e)) { + result.push_back(e); + } + else { + result.push_back(m.mk_not(e)); + } + } + m_visited.reset(); + m1.reset(); + m2.reset(); + m_values.reset(); + return result; +} void ternary_model_evaluator::prune_by_probing(ptr_vector const& formulas, expr_ref_vector& model) { unsigned sz1 = model.size(); @@ -335,8 +364,112 @@ void ternary_model_evaluator::prune_by_probing(ptr_vector const& formulas, TRACE("pdr", tout << sz1 << " ==> " << model.size() << "\n";); } -void ternary_model_evaluator::prune_by_cone_of_influence(ptr_vector const & formulas, expr_ref_vector& model) { - ptr_vector todo, tocollect; +void ternary_model_evaluator::process_formula(app* e, ptr_vector todo, ptr_vector& tocollect) { + SASSERT(m.is_bool(e)); + SASSERT(is_true(e) || is_false(e)); + unsigned v = is_true(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); + } +} + +void ternary_model_evaluator::collect(ptr_vector const& formulas, ptr_vector& tocollect) { + ptr_vector todo; todo.append(formulas); m_visited.reset(); m1.set_level(m_level1); @@ -347,115 +480,19 @@ void ternary_model_evaluator::prune_by_cone_of_influence(ptr_vector const while (!todo.empty()) { app* e = to_app(todo.back()); todo.pop_back(); - if (m_visited.is_marked(e)) { - continue; + if (!m_visited.is_marked(e)) { + process_formula(e, todo, tocollect); + m_visited.mark(e, true); } - 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(); +} + +void ternary_model_evaluator::prune_by_cone_of_influence(ptr_vector const & formulas, expr_ref_vector& model) { + ptr_vector tocollect; + collect(formulas, tocollect); for (unsigned i = 0; i < tocollect.size(); ++i) { for_each_expr(*this, m_visited, tocollect[i]); } diff --git a/lib/pdr_util.h b/lib/pdr_util.h index f3cddd130..8372f6fcc 100644 --- a/lib/pdr_util.h +++ b/lib/pdr_util.h @@ -214,6 +214,9 @@ class ternary_model_evaluator : public model_evaluator_base { void del_model(expr* e); bool get_assignment(expr* e, expr*& var, expr*& val); + + void collect(ptr_vector const& formulas, ptr_vector& tocollect); + void process_formula(app* e, ptr_vector todo, ptr_vector& tocollect); void prune_by_cone_of_influence(ptr_vector const & formulas, expr_ref_vector& model); void prune_by_probing(ptr_vector const & formulas, expr_ref_vector& model); @@ -246,6 +249,13 @@ public: ternary_model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m) {} virtual void minimize_model(ptr_vector const & formulas, expr_ref_vector & model); + /** + \brief extract literals from formulas that satisfy formulas. + + \pre model satisfies formulas + */ + expr_ref_vector minimize_literals(ptr_vector const & formulas, expr_ref_vector const & model); + // for_each_expr visitor. void operator()(expr* e) {} };