mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-24 19:06:21 +00:00
Code Activity

LRA tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-06 08:32:21 -08:00
commit 37a75622a9
15 changed files with 882 additions and 474 deletions
Download patch file Download diff file Expand all files Collapse all files

95
src/muz_qe/horn_tactic.cpp
View file

@ -21,15 +21,20 @@ Revision History:
#include"proof_converter.h"
#include"horn_tactic.h"
#include"dl_context.h"
#include"expr_replacer.h"
#include"dl_rule_transformer.h"
#include"dl_mk_slice.h"
class horn_tactic : public tactic {
struct imp {
ast_manager& m;
bool m_is_simplify;
datalog::context m_ctx;
smt_params m_fparams;
imp(ast_manager & m, params_ref const & p):
imp(bool t, ast_manager & m, params_ref const & p):
m(m),
m_is_simplify(t),
m_ctx(m, m_fparams) {
updt_params(p);
}
@ -180,6 +185,9 @@ class horn_tactic : public tactic {
expr_ref_vector queries(m);
std::stringstream msg;
m_ctx.reset();
m_ctx.ensure_opened();
for (unsigned i = 0; i < sz; i++) {
f = g->form(i);
formula_kind k = get_formula_kind(f);
@ -196,7 +204,7 @@ class horn_tactic : public tactic {
}
}
if (queries.size() != 1) {
if (queries.size() != 1 || m_is_simplify) {
q = m.mk_fresh_const("query", m.mk_bool_sort());
register_predicate(q);
for (unsigned i = 0; i < queries.size(); ++i) {
@ -208,8 +216,26 @@ class horn_tactic : public tactic {
}
SASSERT(queries.size() == 1);
q = queries[0].get();
if (m_is_simplify) {
simplify(q, g, result, mc, pc);
}
else {
verify(q, g, result, mc, pc);
}
}
void verify(expr* q,
goal_ref const& g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc) {
lbool is_reachable = m_ctx.query(q);
g->inc_depth();
bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled();
result.push_back(g.get());
switch (is_reachable) {
case l_true: {
@ -237,19 +263,68 @@ class horn_tactic : public tactic {
TRACE("horn", g->display(tout););
SASSERT(g->is_well_sorted());
}
void simplify(expr* q,
goal_ref const& g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc) {
expr_ref fml(m);
bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled();
if (produce_models) {
mc = datalog::mk_skip_model_converter();
}
if (produce_proofs) {
pc = datalog::mk_skip_proof_converter();
}
func_decl* query_pred = to_app(q)->get_decl();
m_ctx.set_output_predicate(query_pred);
m_ctx.get_rules(); // flush adding rules.
m_ctx.apply_default_transformation(mc, pc);
if (m_ctx.get_params().slice()) {
datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice);
m_ctx.transform_rules(transformer, mc, pc);
}
expr_substitution sub(m);
sub.insert(q, m.mk_false());
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
rep->set_substitution(&sub);
g->inc_depth();
g->reset();
result.push_back(g.get());
datalog::rule_set const& rules = m_ctx.get_rules();
datalog::rule_set::iterator it = rules.begin(), end = rules.end();
for (; it != end; ++it) {
datalog::rule* r = *it;
r->to_formula(fml);
(*rep)(fml);
g->assert_expr(fml);
}
}
};
bool m_is_simplify;
params_ref m_params;
statistics m_stats;
imp * m_imp;
public:
horn_tactic(ast_manager & m, params_ref const & p):
horn_tactic(bool t, ast_manager & m, params_ref const & p):
m_is_simplify(t),
m_params(p) {
m_imp = alloc(imp, m, p);
m_imp = alloc(imp, t, m, p);
}
virtual tactic * translate(ast_manager & m) {
return alloc(horn_tactic, m, m_params);
return alloc(horn_tactic, m_is_simplify, m, m_params);
}
virtual ~horn_tactic() {
@ -293,7 +368,7 @@ public:
m_imp = 0;
}
dealloc(d);
d = alloc(imp, m, m_params);
d = alloc(imp, m_is_simplify, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
@ -308,6 +383,10 @@ protected:
};
tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(horn_tactic, m, p));
return clean(alloc(horn_tactic, false, m, p));
}
tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(horn_tactic, true, m, p));
}

5
src/muz_qe/horn_tactic.h
View file

@ -27,4 +27,9 @@ tactic * mk_horn_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("horn", "apply tactic for horn clauses.", "mk_horn_tactic(m, p)")
*/
tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("horn-simplify", "simplify horn clauses.", "mk_horn_simplify_tactic(m, p)")
*/
#endif

183
src/muz_qe/pdr_context.cpp
View file

@ -410,6 +410,15 @@ namespace pdr {
add_property(result, level);
}
void pred_transformer::propagate_to_infinity(unsigned invariant_level) {
expr_ref inv = get_formulas(invariant_level, false);
add_property(inv, infty_level);
// cleanup
for (unsigned i = invariant_level; i < m_levels.size(); ++i) {
m_levels[i].reset();
}
}
lbool pred_transformer::is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level) {
TRACE("pdr",
tout << "is-reachable: " << head()->get_name() << " level: " << n.level() << "\n";
@ -723,6 +732,7 @@ namespace pdr {
m_closed = true;
}
<<<<<<< HEAD
expr_ref model_node::get_trace(context const& ctx) {
pred_transformer& p = pt();
ast_manager& m = p.get_manager();
@ -736,6 +746,8 @@ namespace pdr {
return fml;
}
=======
>>>>>>> bdc675b1dfef87fcffeb7f3e5143128492d3bd89
static bool is_ini(datalog::rule const& r) {
return r.get_uninterpreted_tail_size() == 0;
}
@ -954,95 +966,80 @@ namespace pdr {
return out;
}
/**
Extract trace comprising of constraints
and predicates that are satisfied from facts to the query.
The resulting trace
*/
expr_ref model_search::get_trace(context const& ctx) const {
pred_transformer& pt = get_root().pt();
ast_manager& m = pt.get_manager();
manager& pm = pt.get_pdr_manager();
expr_ref_vector rules(m);
expr_ref_vector binding(m);
ptr_vector<model_node> todo;
datalog::rule_ref r0(rm), r1(rm), r2(rm);
datalog::context& dctx = ctx.get_context();
datalog::rule_manager& rm = dctx.get_rule_manager();
expr_ref_vector constraints(m), predicates(m);
expr_ref tmp(m);
ptr_vector<model_node> children;
unsigned deltas[2];
datalog::rule_ref rule(rm), r0(rm);
model_node* n = m_root;
todo.push_back(n);
while (!todo.empty()) {
n = todo.back();
ptr_vector<model_node> const& chs = n->children();
rls.push_back(0);
for (unsigned i = 0; i < chs.size(); ++i) {
todo.push_back(chs[i]);
datalog::var_counter& vc = rm.get_var_counter();
substitution subst(m);
unifier unif(m);
rule = n->get_rule();
unsigned max_var = vc.get_max_var(*rule);
predicates.push_back(rule->get_head());
children.append(n);
bool first = true;
while (!children.empty()) {
SASSERT(children.size() == predicates.size());
expr_ref_vector binding(m);
n = children.back();
children.pop_back();
n->mk_instantiate(r0, rule, binding);
max_var = std::max(max_var, vc.get_max_var(*rule));
subst.reset();
subst.reserve(2, max_var+1);
deltas[0] = 0;
deltas[1] = max_var+1;
VERIFY(unif(predicates.back(), rule->get_head(), subst));
for (unsigned i = 0; i < constraints.size(); ++i) {
subst.apply(2, deltas, expr_offset(constraints[i].get(), 0), tmp);
dctx.get_rewriter()(tmp);
constraints[i] = tmp;
}
if (!chs.empty()) {
continue;
for (unsigned i = 0; i < predicates.size(); ++i) {
subst.apply(2, deltas, expr_offset(predicates[i].get(), 0), tmp);
predicates[i] = tmp;
}
expr_ref fml0(m);
binding.reset();
n->mk_instantiate(r0, r1, binding);
r0->to_formula(fml0);
datalog::rule_ref reduced_rule(rm), r3(rm);
reduced_rule = rls[0];
// check if binding is identity.
bool binding_is_id = true;
for (unsigned i = 0; binding_is_id && i < binding.size(); ++i) {
expr* v = binding[i].get();
binding_is_id = is_var(v) && to_var(v)->get_idx() == i;
if (!first) {
constraints.push_back(predicates.back());
}
if (rls.size() > 1 || !binding_is_id) {
expr_ref tmp(m);
vector<expr_ref_vector> substs;
svector<std::pair<unsigned,unsigned> > positions;
substs.push_back(binding); // TODO base substitution.
for (unsigned i = 1; i < rls.size(); ++i) {
datalog::rule& src = *rls[i];
bool unified = unifier.unify_rules(*reduced_rule, 0, src);
if (!unified) {
IF_VERBOSE(0,
verbose_stream() << "Could not unify rules: ";
reduced_rule->display(dctx, verbose_stream());
src.display(dctx, verbose_stream()););
}
expr_ref_vector sub1 = unifier.get_rule_subst(*reduced_rule, true);
TRACE("pdr",
for (unsigned k = 0; k < sub1.size(); ++k) {
tout << mk_pp(sub1[k].get(), m) << " ";
}
tout << "\n";
);
for (unsigned j = 0; j < substs.size(); ++j) {
for (unsigned k = 0; k < substs[j].size(); ++k) {
var_subst(m, false)(substs[j][k].get(), sub1.size(), sub1.c_ptr(), tmp);
substs[j][k] = tmp;
}
while (substs[j].size() < sub1.size()) {
substs[j].push_back(sub1[substs[j].size()].get());
}
}
positions.push_back(std::make_pair(i,0));
substs.push_back(unifier.get_rule_subst(src, false));
VERIFY(unifier.apply(*reduced_rule.get(), 0, src, r3));
reduced_rule = r3;
first = false;
predicates.pop_back();
for (unsigned i = 0; i < rule->get_uninterpreted_tail_size(); ++i) {
subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
predicates.push_back(tmp);
}
for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) {
subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
dctx.get_rewriter()(tmp);
if (!m.is_true(tmp)) {
constraints.push_back(tmp);
}
expr_ref fml_concl(m);
reduced_rule->to_formula(fml_concl);
p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs);
}
cache.insert(n->state(), p1);
rules.insert(n->state(), reduced_rule);
trail.push_back(p1);
rules_trail.push_back(reduced_rule);
todo.pop_back();
}
while (!nodes.empty()) {
model_node* current = nodes.back();
nodes.pop_back();
rules.push_back(current->get_trace(ctx));
nodes.append(current->children());
}
return expr_ref(m.mk_and(rules.size(), rules.c_ptr()), m);
for (unsigned i = 0; i < constraints.size(); ++i) {
max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
}
for (unsigned i = 0; i < predicates.size(); ++i) {
max_var = std::max(vc.get_max_var(predicates[i].get()), max_var);
}
children.append(n->children());
}
return pm.mk_and(constraints);
}
proof_ref model_search::get_proof_trace(context const& ctx) const {
@ -1434,6 +1431,8 @@ namespace pdr {
if (!m_params.validate_result()) {
return;
}
std::stringstream msg;
switch(m_last_result) {
case l_true: {
proof_ref pr = get_proof();
@ -1441,7 +1440,8 @@ namespace pdr {
expr_ref_vector side_conditions(m);
bool ok = checker.check(pr, side_conditions);
if (!ok) {
IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";);
msg << "proof validation failed";
throw default_exception(msg.str());
}
for (unsigned i = 0; i < side_conditions.size(); ++i) {
expr* cond = side_conditions[i].get();
@ -1452,9 +1452,8 @@ namespace pdr {
solver.assert_expr(tmp);
lbool res = solver.check();
if (res != l_false) {
IF_VERBOSE(0, verbose_stream() << "rule validation failed\n";
verbose_stream() << mk_pp(cond, m) << "\n";
);
msg << "rule validation failed when checking: " << mk_pp(cond, m);
throw default_exception(msg.str());
}
}
break;
@ -1497,14 +1496,15 @@ namespace pdr {
names.push_back(symbol(i));
}
sorts.reverse();
tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp);
if (!sorts.empty()) {
tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp);
}
smt::kernel solver(m, get_fparams());
solver.assert_expr(tmp);
lbool res = solver.check();
if (res != l_false) {
IF_VERBOSE(0, verbose_stream() << "rule validation failed\n";
verbose_stream() << mk_pp(tmp, m) << "\n";
);
msg << "rule validation failed when checking: " << mk_pp(tmp, m);
throw default_exception(msg.str());
}
}
}
@ -1597,6 +1597,14 @@ namespace pdr {
inductive_property ex(m, mc, rs);
verbose_stream() << ex.to_string();
});
// upgrade invariants that are known to be inductive.
decl2rel::iterator it = m_rels.begin (), end = m_rels.end ();
for (; m_inductive_lvl > 0 && it != end; ++it) {
if (it->m_value->head() != m_query_pred) {
it->m_value->propagate_to_infinity (m_inductive_lvl);
}
}
validate();
return l_false;
}
@ -2006,6 +2014,7 @@ namespace pdr {
}
st.update("PDR num unfoldings", m_stats.m_num_nodes);
st.update("PDR max depth", m_stats.m_max_depth);
st.update("PDR inductive level", m_inductive_lvl);
m_pm.collect_statistics(st);
for (unsigned i = 0; i < m_core_generalizers.size(); ++i) {

2
src/muz_qe/pdr_context.h
View file

@ -138,6 +138,7 @@ namespace pdr {
ptr_vector<app>& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); }
bool propagate_to_next_level(unsigned level);
void propagate_to_infinity(unsigned level);
void add_property(expr * lemma, unsigned lvl); // add property 'p' to state at level.
lbool is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level);
@ -223,7 +224,6 @@ namespace pdr {
void set_rule(datalog::rule const* r) { m_rule = r; }
datalog::rule* get_rule();
expr_ref get_trace(context const& ctx);
void mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding);
std::ostream& display(std::ostream& out, unsigned indent);