mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
working on quantifiers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4f7dd08c38
commit
8612c89c54
|
@ -67,8 +67,13 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
|
|||
buffer << s << k;
|
||||
return symbol(buffer.str().c_str());
|
||||
}
|
||||
|
||||
buffer << mk_smt2_quoted_symbol(s);
|
||||
|
||||
if (is_smt2_quoted_symbol(s)) {
|
||||
buffer << mk_smt2_quoted_symbol(s);
|
||||
}
|
||||
else {
|
||||
buffer << s;
|
||||
}
|
||||
if (k > 0) {
|
||||
buffer << k;
|
||||
}
|
||||
|
|
|
@ -38,12 +38,43 @@ namespace datalog {
|
|||
m_refs.reset();
|
||||
}
|
||||
|
||||
app_ref mk_extract_quantifiers::ensure_app(expr* e) {
|
||||
if (is_app(e)) {
|
||||
return app_ref(to_app(e), m);
|
||||
}
|
||||
else {
|
||||
return app_ref(m.mk_eq(e, m.mk_true()), m);
|
||||
}
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers::ensure_predicate(expr* e, unsigned& max_var, app_ref_vector& tail) {
|
||||
SASSERT(is_app(e));
|
||||
SASSERT(to_app(e)->get_decl()->get_family_id() == null_family_id);
|
||||
app* a = to_app(e);
|
||||
expr_ref_vector args(m);
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
expr* arg = a->get_arg(i);
|
||||
if (is_var(arg) || m.is_value(arg)) {
|
||||
args.push_back(arg);
|
||||
}
|
||||
else {
|
||||
expr_ref new_var(m);
|
||||
new_var = m.mk_var(++max_var, m.get_sort(arg));
|
||||
args.push_back(new_var);
|
||||
tail.push_back(m.mk_eq(new_var, arg));
|
||||
}
|
||||
}
|
||||
tail.push_back(m.mk_app(a->get_decl(), args.size(), args.c_ptr()));
|
||||
}
|
||||
|
||||
|
||||
void mk_extract_quantifiers::extract(rule& r, rule_set& new_rules) {
|
||||
expr_ref_vector tail(m);
|
||||
app_ref_vector tail(m);
|
||||
quantifier_ref_vector quantifiers(m);
|
||||
unsigned utsz = r.get_uninterpreted_tail_size();
|
||||
unsigned tsz = r.get_tail_size();
|
||||
var_counter vc(true);
|
||||
unsigned max_var = vc.get_max_var(r);
|
||||
for (unsigned i = 0; i < utsz; ++i) {
|
||||
tail.push_back(r.get_tail(i));
|
||||
if (r.is_neg_tail(i)) {
|
||||
|
@ -51,21 +82,37 @@ namespace datalog {
|
|||
return;
|
||||
}
|
||||
}
|
||||
var_subst vs(m, true);
|
||||
for (unsigned i = utsz; i < tsz; ++i) {
|
||||
app* t = r.get_tail(i);
|
||||
expr_ref_vector conjs(m);
|
||||
datalog::flatten_and(t, conjs);
|
||||
quantifier_ref qe(m);
|
||||
expr_ref qe(m);
|
||||
quantifier* q = 0;
|
||||
for (unsigned j = 0; j < conjs.size(); ++j) {
|
||||
expr* e = conjs[j].get();
|
||||
if (rule_manager::is_forall(m, e, q)) {
|
||||
quantifiers.push_back(q);
|
||||
qe = m.mk_exists(q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), q->get_expr());
|
||||
tail.push_back(qe);
|
||||
expr_ref_vector sub(m);
|
||||
ptr_vector<sort> fv;
|
||||
unsigned num_decls = q->get_num_decls();
|
||||
get_free_vars(q, fv);
|
||||
for (unsigned k = 0; k < fv.size(); ++k) {
|
||||
unsigned idx = fv.size()-k-1;
|
||||
if (!fv[idx]) {
|
||||
fv[idx] = m.mk_bool_sort();
|
||||
}
|
||||
sub.push_back(m.mk_var(idx, fv[idx]));
|
||||
}
|
||||
for (unsigned k = 0; k < num_decls; ++k) {
|
||||
sub.push_back(m.mk_var(num_decls+max_var-k, q->get_decl_sort(k)));
|
||||
}
|
||||
max_var += num_decls;
|
||||
vs(q->get_expr(), sub.size(), sub.c_ptr(), qe);
|
||||
ensure_predicate(qe, max_var, tail);
|
||||
}
|
||||
else {
|
||||
tail.push_back(e);
|
||||
tail.push_back(ensure_app(e));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -73,16 +120,16 @@ namespace datalog {
|
|||
new_rules.add_rule(&r);
|
||||
}
|
||||
else {
|
||||
expr_ref fml(m);
|
||||
rule_ref_vector rules(rm);
|
||||
fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), r.get_head());
|
||||
rm.mk_rule(fml, rules, r.name());
|
||||
rule_ref new_rule(rm);
|
||||
std::cout << mk_pp(r.get_head(), m) << " :- \n";
|
||||
for (unsigned i = 0; i < tail.size(); ++i) {
|
||||
std::cout << " " << mk_pp(tail[i].get(), m) << "\n";
|
||||
}
|
||||
new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name(), false);
|
||||
quantifier_ref_vector* qs = alloc(quantifier_ref_vector, quantifiers);
|
||||
m_refs.push_back(qs);
|
||||
for (unsigned i = 0; i < rules.size(); ++i) {
|
||||
m_quantifiers.insert(rules[i].get(), qs);
|
||||
new_rules.add_rule(rules[i].get());
|
||||
}
|
||||
new_rules.add_rule(new_rule);
|
||||
m_quantifiers.insert(new_rule, qs);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -37,6 +37,10 @@ namespace datalog {
|
|||
|
||||
void extract(rule& r, rule_set& new_rules);
|
||||
|
||||
app_ref ensure_app(expr* e);
|
||||
|
||||
void ensure_predicate(expr* e, unsigned& max_var, app_ref_vector& tail);
|
||||
|
||||
public:
|
||||
/**
|
||||
\brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
|
||||
|
|
|
@ -731,17 +731,15 @@ namespace pdr {
|
|||
TRACE("pdr", model_smt2_pp(tout, m, get_model(), 0););
|
||||
func_decl* f = p.head();
|
||||
unsigned arity = f->get_arity();
|
||||
model_ref model = get_model_ptr();
|
||||
expr_ref_vector args(m);
|
||||
func_decl_ref v(m);
|
||||
expr_ref v(m);
|
||||
model_evaluator mev(m);
|
||||
|
||||
for (unsigned i = 0; i < arity; ++i) {
|
||||
v = pm.o2n(p.sig(i),0);
|
||||
expr* e = get_model().get_const_interp(v);
|
||||
if (e) {
|
||||
args.push_back(e);
|
||||
}
|
||||
else {
|
||||
args.push_back(m.mk_const(v));
|
||||
}
|
||||
v = m.mk_const(pm.o2n(p.sig(i),0));
|
||||
expr_ref e = mev.eval(model, v);
|
||||
args.push_back(e);
|
||||
}
|
||||
return expr_ref(m.mk_app(f, args.size(), args.c_ptr()), m);
|
||||
}
|
||||
|
@ -1833,7 +1831,7 @@ namespace pdr {
|
|||
pr = m.mk_asserted(m.mk_true());
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
if (smt::is_value_sort(m, vars[i].get())) {
|
||||
VERIFY (M->eval(vars[i].get(), tmp, true));
|
||||
tmp = mev.eval(M, vars[i].get());
|
||||
sub.insert(vars[i].get(), tmp, pr);
|
||||
}
|
||||
}
|
||||
|
@ -1866,7 +1864,7 @@ namespace pdr {
|
|||
for (unsigned j = 1; j < indices.size(); ++j) {
|
||||
ptr_vector<app> const& vs = vars[indices[j]];
|
||||
for (unsigned k = 0; k < vs.size(); ++k) {
|
||||
M->eval(vs[k]->get_decl(), tmp);
|
||||
tmp = mev.eval(M, vs[k]);
|
||||
sub.insert(vs[k], tmp, pr);
|
||||
child_states[indices[j]].push_back(m.mk_eq(vs[k], tmp));
|
||||
}
|
||||
|
|
|
@ -19,12 +19,13 @@ Revision History:
|
|||
|
||||
#include "pdr_quantifiers.h"
|
||||
#include "pdr_context.h"
|
||||
#include "model_smt2_pp.h"
|
||||
#include "ast_smt2_pp.h"
|
||||
#include "qe.h"
|
||||
#include "var_subst.h"
|
||||
#include "dl_rule_set.h"
|
||||
#include "ast_smt2_pp.h"
|
||||
#include "model_smt2_pp.h"
|
||||
#include "ast_smt_pp.h"
|
||||
#include "expr_abstract.h"
|
||||
|
||||
|
||||
namespace pdr {
|
||||
|
@ -104,21 +105,34 @@ namespace pdr {
|
|||
}
|
||||
|
||||
void quantifier_model_checker::apply_binding(quantifier* q, expr_ref_vector& binding) {
|
||||
|
||||
datalog::scoped_no_proof _scp(m);
|
||||
|
||||
app_ref_vector& var_inst = m_current_pt->get_inst(m_current_rule);
|
||||
expr_substitution sub(m);
|
||||
for (unsigned i = 0; i < var_inst.size(); ++i) {
|
||||
expr* v = var_inst[i].get();
|
||||
sub.insert(v, m.mk_var(i, m.get_sort(v)));
|
||||
}
|
||||
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
|
||||
rep->set_substitution(&sub);
|
||||
|
||||
TRACE("pdr", tout << mk_pp(q, m) << "\n";
|
||||
tout << "binding\n";
|
||||
for (unsigned i = 0; i < binding.size(); ++i) {
|
||||
tout << mk_pp(binding[i].get(), m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
tout << "inst\n";
|
||||
for (unsigned i = 0; i < var_inst.size(); ++i) {
|
||||
tout << mk_pp(var_inst[i].get(), m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
|
||||
|
||||
expr_ref e(m);
|
||||
var_subst vs(m, false);
|
||||
inv_var_shifter invsh(m);
|
||||
vs(q->get_expr(), binding.size(), binding.c_ptr(), e);
|
||||
(*rep)(e);
|
||||
invsh(e, q->get_num_decls(), e);
|
||||
expr_abstract(m, 0, var_inst.size(), (expr*const*)var_inst.c_ptr(), e, e);
|
||||
TRACE("pdr", tout << mk_pp(e, m) << "\n";);
|
||||
m_instantiated_rules.push_back(m_current_rule);
|
||||
m_instantiations.push_back(to_app(e));
|
||||
TRACE("pdr", tout << mk_pp(e, m) << "\n";);
|
||||
}
|
||||
|
||||
|
||||
|
@ -187,6 +201,7 @@ namespace pdr {
|
|||
expr_ref_vector fmls(m);
|
||||
front_end_params fparams;
|
||||
fparams.m_proof_mode = PGM_COARSE;
|
||||
fparams.m_mbqi = true;
|
||||
// TBD: does not work on integers: fparams.m_mbqi = true;
|
||||
|
||||
fmls.push_back(m_A.get());
|
||||
|
@ -364,6 +379,12 @@ namespace pdr {
|
|||
for (unsigned i = 0; i < m_Bs.size(); ++i) {
|
||||
tout << mk_pp((*qis)[i].get(), m) << "\n" << mk_pp(m_Bs[i].get(), m) << "\n";
|
||||
}
|
||||
ast_smt_pp pp(m);
|
||||
pp.add_assumption(m_A);
|
||||
for (unsigned i = 0; i < m_Bs.size(); ++i) {
|
||||
pp.add_assumption(m_Bs[i].get());
|
||||
}
|
||||
pp.display_smt2(tout, m.mk_true());
|
||||
);
|
||||
|
||||
find_instantiations(*qis, level);
|
||||
|
@ -406,6 +427,7 @@ namespace pdr {
|
|||
m_quantifiers.remove(r);
|
||||
datalog::rule_ref_vector rules(rule_m);
|
||||
expr_ref rule(m.mk_implies(m.mk_and(body.size(), body.c_ptr()), r->get_head()), m);
|
||||
std::cout << mk_pp(rule, m) << "\n";
|
||||
rule_m.mk_rule(rule, rules, r->name());
|
||||
for (unsigned i = 0; i < rules.size(); ++i) {
|
||||
new_rules.add_rule(rules[i].get());
|
||||
|
|
|
@ -549,7 +549,7 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
|
||||
bool model_evaluator::extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref else_case) {
|
||||
bool model_evaluator::extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case) {
|
||||
SASSERT(m_array.is_array(a));
|
||||
|
||||
while (m_array.is_store(a)) {
|
||||
|
@ -582,6 +582,9 @@ namespace pdr {
|
|||
stores.push_back(store);
|
||||
}
|
||||
else_case = g->get_else();
|
||||
if (!else_case) {
|
||||
return false;
|
||||
}
|
||||
if (!is_ground(else_case)) {
|
||||
return false;
|
||||
}
|
||||
|
@ -903,6 +906,32 @@ namespace pdr {
|
|||
return !has_x;
|
||||
}
|
||||
|
||||
expr_ref model_evaluator::eval(model_ref& model, expr* e) {
|
||||
expr_ref result(m);
|
||||
m_model = model;
|
||||
VERIFY(m_model->eval(e, result, true));
|
||||
if (m_array.is_array(e)) {
|
||||
vector<expr_ref_vector> stores;
|
||||
expr_ref_vector args(m);
|
||||
expr_ref else_case(m);
|
||||
if (extract_array_func_interp(result, stores, else_case)) {
|
||||
result = m_array.mk_const_array(m.get_sort(e), else_case);
|
||||
while (!stores.empty() && stores.back().back() == else_case) {
|
||||
stores.pop_back();
|
||||
}
|
||||
for (unsigned i = stores.size(); i > 0; ) {
|
||||
--i;
|
||||
args.resize(1);
|
||||
args[0] = result;
|
||||
args.append(stores[i]);
|
||||
result = m_array.mk_store(args.size(), args.c_ptr());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
|
||||
ast_manager& m = fml.get_manager();
|
||||
|
|
|
@ -103,7 +103,7 @@ namespace pdr {
|
|||
|
||||
bool check_model(ptr_vector<expr> const & formulas);
|
||||
|
||||
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref else_case);
|
||||
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case);
|
||||
|
||||
public:
|
||||
model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {}
|
||||
|
@ -127,6 +127,8 @@ namespace pdr {
|
|||
for_each_expr visitor.
|
||||
*/
|
||||
void operator()(expr* e) {}
|
||||
|
||||
expr_ref eval(model_ref& mdl, expr* e);
|
||||
};
|
||||
|
||||
/**
|
||||
|
|
Loading…
Reference in a new issue