mirror of
https://github.com/Z3Prover/z3
synced 2025-08-11 05:30:51 +00:00
experiments wtih QHC
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
63b7f7ecd6
commit
d318aab7d1
9 changed files with 379 additions and 291 deletions
|
|
@ -19,6 +19,12 @@ Revision History:
|
|||
|
||||
#include"dl_mk_extract_quantifiers.h"
|
||||
#include"ast_pp.h"
|
||||
#include"dl_bmc_engine.h"
|
||||
#include"smt_quantifier.h"
|
||||
#include"smt_context.h"
|
||||
#include"for_each_expr.h"
|
||||
#include "expr_abstract.h"
|
||||
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
@ -27,24 +33,16 @@ namespace datalog {
|
|||
rule_transformer::plugin(101, false),
|
||||
m_ctx(ctx),
|
||||
m(ctx.get_manager()),
|
||||
rm(ctx.get_rule_manager())
|
||||
rm(ctx.get_rule_manager()),
|
||||
m_query_pred(m)
|
||||
{}
|
||||
|
||||
mk_extract_quantifiers::~mk_extract_quantifiers() {
|
||||
for (unsigned i = 0; i < m_refs.size(); ++i) {
|
||||
dealloc(m_refs[i]);
|
||||
}
|
||||
m_quantifiers.reset();
|
||||
m_refs.reset();
|
||||
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::set_query(func_decl* q) {
|
||||
m_query_pred = q;
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers::ensure_predicate(expr* e, unsigned& max_var, app_ref_vector& tail) {
|
||||
|
|
@ -67,85 +65,305 @@ namespace datalog {
|
|||
tail.push_back(m.mk_app(a->get_decl(), args.size(), args.c_ptr()));
|
||||
}
|
||||
|
||||
class mk_extract_quantifiers::collect_insts {
|
||||
ast_manager& m;
|
||||
ptr_vector<expr> m_binding;
|
||||
vector<expr_ref_vector> m_bindings;
|
||||
ptr_vector<quantifier> m_quantifiers;
|
||||
public:
|
||||
collect_insts(ast_manager& m): m(m) { }
|
||||
|
||||
void operator()(expr* n) {
|
||||
expr* not_q_or_i, *e1, *e2, *e3;
|
||||
if (m.is_quant_inst(n, not_q_or_i, m_binding)) {
|
||||
VERIFY(m.is_or(not_q_or_i, e1, e2));
|
||||
VERIFY(m.is_not(e1, e3));
|
||||
SASSERT(is_quantifier(e3));
|
||||
m_quantifiers.push_back(to_quantifier(e3));
|
||||
m_bindings.push_back(expr_ref_vector(m,m_binding.size(), m_binding.c_ptr()));
|
||||
m_binding.reset();
|
||||
}
|
||||
else if ((m.is_rewrite(n, e1, e2) ||
|
||||
(m.is_rewrite_star(n) &&
|
||||
(e3 = to_app(n)->get_arg(to_app(n)->get_num_args()-1),
|
||||
e1 = to_app(e3)->get_arg(0),
|
||||
e2 = to_app(e3)->get_arg(1),
|
||||
true))) &&
|
||||
is_quantifier(e1) && m.is_false(e2)) {
|
||||
quantifier* q = to_quantifier(e1);
|
||||
m_quantifiers.push_back(q);
|
||||
m_bindings.push_back(expr_ref_vector(m));
|
||||
expr_ref_vector& b = m_bindings.back();
|
||||
for (unsigned i = 0; i < q->get_num_decls(); ++i) {
|
||||
b.push_back(m.mk_fresh_const("V", q->get_decl_sort(i)));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void reset() {
|
||||
m_quantifiers.reset();
|
||||
m_bindings.reset();
|
||||
}
|
||||
|
||||
unsigned size() const { return m_quantifiers.size(); }
|
||||
ptr_vector<quantifier> const& quantifiers() const { return m_quantifiers; }
|
||||
vector<expr_ref_vector> const& bindings() const { return m_bindings; }
|
||||
};
|
||||
|
||||
|
||||
/*
|
||||
* forall y . P1(x,y) &
|
||||
* forall y . P2(x,y) &
|
||||
* Body[x] &
|
||||
* ~H[x]
|
||||
* forall y . y != binding1 => ~ P1(x,y)
|
||||
* forall y . y != binding2 => ~ P2(x,y)
|
||||
*/
|
||||
void mk_extract_quantifiers::extract(rule& r, rule_set& new_rules) {
|
||||
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)) {
|
||||
new_rules.add_rule(&r);
|
||||
return;
|
||||
expr_ref_vector conjs(m);
|
||||
quantifier_ref_vector qs(m);
|
||||
for (unsigned i = utsz; i < r.get_tail_size(); ++i) {
|
||||
conjs.push_back(r.get_tail(i));
|
||||
}
|
||||
datalog::flatten_and(conjs);
|
||||
for (unsigned j = 0; j < conjs.size(); ++j) {
|
||||
expr* e = conjs[j].get();
|
||||
quantifier* q;
|
||||
if (rule_manager::is_forall(m, e, q)) {
|
||||
qs.push_back(q);
|
||||
conjs[j] = conjs.back();
|
||||
conjs.pop_back();
|
||||
--j;
|
||||
}
|
||||
}
|
||||
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);
|
||||
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);
|
||||
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(ensure_app(e));
|
||||
}
|
||||
}
|
||||
}
|
||||
if (quantifiers.empty()) {
|
||||
if (qs.empty()) {
|
||||
new_rules.add_rule(&r);
|
||||
}
|
||||
else {
|
||||
rule_ref new_rule(rm);
|
||||
TRACE("dl",
|
||||
tout << mk_pp(r.get_head(), m) << " :- \n";
|
||||
for (unsigned i = 0; i < tail.size(); ++i) {
|
||||
tout << " " << 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);
|
||||
new_rules.add_rule(new_rule);
|
||||
m_quantifiers.insert(new_rule, qs);
|
||||
expr_ref fml(m);
|
||||
expr_ref_vector bindings(m);
|
||||
obj_map<quantifier, expr_ref_vector*> insts;
|
||||
for (unsigned i = 0; i < qs.size(); ++i) {
|
||||
insts.insert(qs[i].get(), alloc(expr_ref_vector, m));
|
||||
}
|
||||
|
||||
unsigned max_inst = 10; // TODO configuration.
|
||||
|
||||
for (unsigned i = 0; i < max_inst; ++i) {
|
||||
app_ref_vector sub(m);
|
||||
rule2formula(r, insts, fml, sub);
|
||||
bool new_binding = find_instantiations_proof_based(fml, sub, insts, bindings);
|
||||
if (!new_binding) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref_vector fmls(m);
|
||||
for (unsigned i = 0; i < utsz; ++i) {
|
||||
fmls.push_back(r.get_tail(i));
|
||||
}
|
||||
fmls.append(bindings);
|
||||
fmls.append(conjs);
|
||||
fml = m.mk_implies(m.mk_and(fmls.size(), fmls.c_ptr()), r.get_head());
|
||||
TRACE("dl", tout << "new rule\n" << mk_pp(fml, m) << "\n";);
|
||||
rule_ref_vector rules(rm);
|
||||
rm.mk_rule(fml, rules, r.name());
|
||||
for (unsigned i = 0; i < rules.size(); ++i) {
|
||||
new_rules.add_rule(rules[i].get());
|
||||
m_quantifiers.insert(rules[i].get(), alloc(quantifier_ref_vector, qs));
|
||||
}
|
||||
obj_map<quantifier, expr_ref_vector*>::iterator it = insts.begin(), end = insts.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->m_value);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers::rule2formula(
|
||||
rule& r,
|
||||
obj_map<quantifier, expr_ref_vector*> const& insts,
|
||||
expr_ref& fml,
|
||||
app_ref_vector& sub)
|
||||
{
|
||||
expr_ref body(m);
|
||||
expr_ref_vector fmls(m);
|
||||
ptr_vector<sort> sorts;
|
||||
var_subst vs(m, false);
|
||||
obj_map<quantifier, expr_ref_vector*>::iterator it = insts.begin(), end = insts.end();
|
||||
for (; it != end; ++it) {
|
||||
quantifier* q = it->m_key;
|
||||
expr_ref_vector& eqs = *it->m_value;
|
||||
expr_ref_vector disj(m);
|
||||
disj.append(eqs);
|
||||
disj.push_back(m.mk_not(q->get_expr()));
|
||||
body = m.mk_or(disj.size(), disj.c_ptr());
|
||||
fml = m.update_quantifier(q, body);
|
||||
fmls.push_back(fml);
|
||||
}
|
||||
fml = m.mk_or(fmls.size(), fmls.c_ptr());
|
||||
fmls.reset();
|
||||
fmls.push_back(fml);
|
||||
for (unsigned i = 0; i < r.get_tail_size(); ++i) {
|
||||
SASSERT(!r.is_neg_tail(i));
|
||||
fmls.push_back(r.get_tail(i));
|
||||
}
|
||||
fmls.push_back(m.mk_not(r.get_head()));
|
||||
fml = m.mk_and(fmls.size(), fmls.c_ptr());
|
||||
|
||||
get_free_vars(fml, sorts);
|
||||
for (unsigned i = 0; i < sorts.size(); ++i) {
|
||||
if (!sorts[i]) {
|
||||
sorts[i] = m.mk_bool_sort();
|
||||
}
|
||||
sub.push_back(m.mk_const(symbol(i), sorts[i]));
|
||||
}
|
||||
vs(fml, sub.size(), (expr*const*)sub.c_ptr(), fml);
|
||||
}
|
||||
|
||||
bool mk_extract_quantifiers::find_instantiations_proof_based(
|
||||
expr* fml,
|
||||
app_ref_vector const& var_inst,
|
||||
obj_map<quantifier, expr_ref_vector*>& insts,
|
||||
expr_ref_vector& bindings)
|
||||
{
|
||||
datalog::scoped_fine_proof _scp(m);
|
||||
smt_params fparams;
|
||||
fparams.m_mbqi = true; // false
|
||||
fparams.m_soft_timeout = 1000;
|
||||
smt::kernel solver(m, fparams);
|
||||
solver.assert_expr(fml);
|
||||
IF_VERBOSE(1, verbose_stream() << "check\n";);
|
||||
lbool result = solver.check();
|
||||
IF_VERBOSE(1, verbose_stream() << "checked\n";);
|
||||
TRACE("dl", tout << result << "\n";);
|
||||
if (result != l_false) {
|
||||
return false;
|
||||
}
|
||||
|
||||
map<symbol, quantifier*, symbol_hash_proc, symbol_eq_proc> qid_map;
|
||||
quantifier* q;
|
||||
|
||||
obj_map<quantifier, expr_ref_vector*>::iterator it = insts.begin(), end = insts.end();
|
||||
for (; it != end; ++it) {
|
||||
q = it->m_key;
|
||||
qid_map.insert(q->get_qid(), q);
|
||||
}
|
||||
|
||||
proof* p = solver.get_proof();
|
||||
TRACE("dl", tout << mk_pp(p, m) << "\n";);
|
||||
collect_insts collector(m);
|
||||
for_each_expr(collector, p);
|
||||
ptr_vector<quantifier> const& quants = collector.quantifiers();
|
||||
|
||||
for (unsigned i = 0; i < collector.size(); ++i) {
|
||||
symbol qid = quants[i]->get_qid();
|
||||
if (!qid_map.find(qid, q)) {
|
||||
TRACE("dl", tout << "Could not find quantifier " << mk_pp(quants[i], m) << "\n";);
|
||||
continue;
|
||||
}
|
||||
expr_ref_vector const& binding = collector.bindings()[i];
|
||||
|
||||
TRACE("dl", tout << "Instantiating:\n" << mk_pp(quants[i], m) << "\n";
|
||||
for (unsigned j = 0; j < binding.size(); ++j) {
|
||||
tout << mk_pp(binding[j], m) << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
|
||||
expr_ref_vector instantiation(m);
|
||||
for (unsigned j = 0; j < binding.size(); ++j) {
|
||||
instantiation.push_back(binding[j]);
|
||||
}
|
||||
add_binding(var_inst, bindings, q, instantiation, insts);
|
||||
}
|
||||
|
||||
return collector.size() > 0;
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers::add_binding(
|
||||
app_ref_vector const& var_inst,
|
||||
expr_ref_vector& bindings,
|
||||
quantifier* q,
|
||||
expr_ref_vector const& instantiation,
|
||||
obj_map<quantifier, expr_ref_vector*>& insts)
|
||||
{
|
||||
if (instantiation.size() == q->get_num_decls()) {
|
||||
// Full binding.
|
||||
apply_binding(var_inst, bindings, q, instantiation, insts);
|
||||
}
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers::apply_binding(
|
||||
app_ref_vector const& var_inst,
|
||||
expr_ref_vector& bindings,
|
||||
quantifier* q,
|
||||
expr_ref_vector const& instantiation,
|
||||
obj_map<quantifier, expr_ref_vector*>& insts)
|
||||
{
|
||||
datalog::scoped_no_proof _scp(m);
|
||||
expr_ref e(m);
|
||||
expr_ref_vector eqs(m);
|
||||
var_subst vs(m, false);
|
||||
inv_var_shifter invsh(m);
|
||||
vs(q->get_expr(), instantiation.size(), instantiation.c_ptr(), e);
|
||||
invsh(e, q->get_num_decls(), e);
|
||||
expr_ref_vector inst(m);
|
||||
inst.append(var_inst.size(), (expr*const*)var_inst.c_ptr());
|
||||
inst.reverse();
|
||||
expr_abstract(m, 0, inst.size(), inst.c_ptr(), e, e);
|
||||
bindings.push_back(e);
|
||||
for (unsigned i = 0; i < instantiation.size(); ++i) {
|
||||
e = instantiation[i];
|
||||
e = m.mk_eq(m.mk_var(i, q->get_decl_sort(i)), e);
|
||||
eqs.push_back(e);
|
||||
}
|
||||
e = m.mk_and(eqs.size(), eqs.c_ptr());
|
||||
insts.find(q)->push_back(e);
|
||||
|
||||
TRACE("dl", tout << mk_pp(q, m) << "\n";
|
||||
tout << "instantiation: ";
|
||||
for (unsigned i = 0; i < instantiation.size(); ++i) {
|
||||
tout << mk_pp(instantiation[i], m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
tout << "inst: ";
|
||||
for (unsigned i = 0; i < var_inst.size(); ++i) {
|
||||
tout << mk_pp(var_inst[i], m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
tout << mk_pp(bindings.back(), m) << "\n";
|
||||
tout << "eqs: " << mk_pp(e, m) << "\n";
|
||||
);
|
||||
}
|
||||
|
||||
|
||||
void mk_extract_quantifiers::reset() {
|
||||
obj_map<rule const, quantifier_ref_vector*>::iterator it = m_quantifiers.begin(),
|
||||
end = m_quantifiers.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->m_value);
|
||||
}
|
||||
m_has_quantifiers = false;
|
||||
m_quantifiers.reset();
|
||||
}
|
||||
|
||||
rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
m_quantifiers.reset();
|
||||
rule_set* rules = alloc(rule_set, m_ctx);
|
||||
reset();
|
||||
rule_set::iterator it = source.begin(), end = source.end();
|
||||
for (; !m_has_quantifiers && it != end; ++it) {
|
||||
m_has_quantifiers = (*it)->has_quantifiers();
|
||||
}
|
||||
if (!m_has_quantifiers) {
|
||||
return 0;
|
||||
}
|
||||
|
||||
rule_set* rules = alloc(rule_set, m_ctx);
|
||||
it = source.begin();
|
||||
for (; it != end; ++it) {
|
||||
extract(**it, *rules);
|
||||
}
|
||||
if (m_quantifiers.empty()) {
|
||||
dealloc(rules);
|
||||
rules = 0;
|
||||
}
|
||||
return rules;
|
||||
|
||||
return rules;
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue