mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
working on expansion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
3a837037d4
commit
8459401b6e
|
@ -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<expr> 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<func_decl> 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););
|
||||
|
|
|
@ -70,10 +70,10 @@ namespace pdr {
|
|||
ptr_vector<datalog::rule> m_rules; // rules used to derive transformer
|
||||
prop_solver m_solver; // solver context
|
||||
vector<expr_ref_vector> m_levels; // level formulas
|
||||
expr_ref_vector m_invariants; // properties that are invariant.
|
||||
obj_map<expr, unsigned> m_prop2level; // map property to level where it occurs.
|
||||
expr_ref_vector m_invariants; // properties that are invariant.
|
||||
obj_map<expr, unsigned> m_prop2level; // map property to level where it occurs.
|
||||
obj_map<expr, datalog::rule const*> 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
|
||||
|
|
|
@ -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"););
|
||||
|
|
|
@ -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<expr_replacer> 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<func_decl> 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";);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
@ -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:
|
||||
|
|
249
lib/pdr_util.cpp
249
lib/pdr_util.cpp
|
@ -299,6 +299,35 @@ void ternary_model_evaluator::minimize_model(ptr_vector<expr> const & formulas,
|
|||
m_values.reset();
|
||||
}
|
||||
|
||||
expr_ref_vector ternary_model_evaluator::minimize_literals(ptr_vector<expr> const& formulas, expr_ref_vector const& model) {
|
||||
|
||||
setup_model(model);
|
||||
|
||||
expr_ref_vector result(m);
|
||||
ptr_vector<expr> 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<expr> const& formulas, expr_ref_vector& model) {
|
||||
unsigned sz1 = model.size();
|
||||
|
@ -335,8 +364,112 @@ void ternary_model_evaluator::prune_by_probing(ptr_vector<expr> const& formulas,
|
|||
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;
|
||||
void ternary_model_evaluator::process_formula(app* e, ptr_vector<expr> todo, ptr_vector<expr>& 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<expr> const& formulas, ptr_vector<expr>& tocollect) {
|
||||
ptr_vector<expr> 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<expr> 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<expr> const & formulas, expr_ref_vector& model) {
|
||||
ptr_vector<expr> tocollect;
|
||||
collect(formulas, tocollect);
|
||||
for (unsigned i = 0; i < tocollect.size(); ++i) {
|
||||
for_each_expr(*this, m_visited, tocollect[i]);
|
||||
}
|
||||
|
|
|
@ -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<expr> const& formulas, ptr_vector<expr>& tocollect);
|
||||
void process_formula(app* e, ptr_vector<expr> todo, ptr_vector<expr>& tocollect);
|
||||
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);
|
||||
|
||||
|
@ -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<expr> 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<expr> const & formulas, expr_ref_vector const & model);
|
||||
|
||||
// for_each_expr visitor.
|
||||
void operator()(expr* e) {}
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue