mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

add handling of quantifiers #5612

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-10-20 12:27:56 -04:00
parent 839a0852fe
commit 13da6a02a6
4 changed files with 27 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_context.h
View file

@ -1192,7 +1192,6 @@ namespace smt {
bool more_than_k_unassigned_literals(clause * cls, unsigned k);
void internalize_assertions();
void asserted_inconsistent();
@ -1609,6 +1608,8 @@ namespace smt {
void assert_expr(expr * e, proof * pr);
void internalize_assertions();
void push();
void pop(unsigned num_scopes);

2
src/smt/smt_enode.cpp
View file

@ -50,7 +50,7 @@ namespace smt {
n->m_lbl_hash = -1;
n->m_proof_is_logged = false;
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
for (unsigned i = 0; i < num_args; i++) {
enode * arg = app2enode[owner->get_arg(i)->get_id()];
n->m_args[i] = arg;
SASSERT(n->get_arg(i) == arg);

2
src/smt/theory_datatype.cpp
View file

@ -297,7 +297,7 @@ namespace smt {
TRACE("datatype", tout << "internalizing term:\n" << mk_pp(term, m) << "\n";);
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(term->get_arg(i), false);
ctx.internalize(term->get_arg(i), has_quantifiers(term));
// the internalization of the arguments may trigger the internalization of term.
if (ctx.e_internalized(term))
return true;

39
src/smt/theory_recfun.cpp
View file

@ -246,18 +246,22 @@ namespace smt {
literal theory_recfun::mk_eq_lit(expr* l, expr* r) {
literal lit;
if (m.is_true(r) || m.is_false(r)) {
std::swap(l, r);
}
if (m.is_true(l)) {
lit = mk_literal(r);
}
else if (m.is_false(l)) {
lit = ~mk_literal(r);
}
else {
lit = mk_eq(l, r, false);
if (has_quantifiers(l) || has_quantifiers(r)) {
expr_ref eq1(m.mk_eq(l, r), m);
expr_ref fn(m.mk_fresh_const("rec-eq", m.mk_bool_sort()), m);
expr_ref eq(m.mk_eq(fn, eq1), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
lit = mk_literal(fn);
}
else if (m.is_true(r) || m.is_false(r))
std::swap(l, r);
else if (m.is_true(l))
lit = mk_literal(r);
else if (m.is_false(l))
lit = ~mk_literal(r);
else
lit = mk_eq(l, r, false);
ctx.mark_as_relevant(lit);
return lit;
}
@ -282,14 +286,12 @@ namespace smt {
auto & vars = e.m_def->get_vars();
expr_ref lhs(e.m_lhs, m);
unsigned depth = get_depth(e.m_lhs);
expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
literal lit = mk_eq_lit(lhs, rhs);
std::function<literal(void)> fn = [&]() { return lit; };
scoped_trace_stream _tr(*this, fn);
ctx.mk_th_axiom(get_id(), 1, &lit);
TRACEFN("macro expansion yields " << pp_lit(ctx, lit));
if (has_quantifiers(rhs))
throw default_exception("quantified formulas in recursive functions are not supported");
}
/**
@ -377,6 +379,13 @@ namespace smt {
unsigned depth = get_depth(e.m_pred);
expr_ref lhs(u().mk_fun_defined(d, args), m);
expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
if (has_quantifiers(rhs)) {
expr_ref fn(m.mk_fresh_const("rec-eq", m.mk_bool_sort()), m);
expr_ref eq(m.mk_eq(fn, rhs), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
rhs = fn;
}
literal_vector clause;
for (auto & g : e.m_cdef->get_guards()) {
expr_ref guard = apply_args(depth, vars, args, g);
@ -394,8 +403,6 @@ namespace smt {
std::function<literal_vector(void)> fn = [&]() { return clause; };
scoped_trace_stream _tr(*this, fn);
ctx.mk_th_axiom(get_id(), clause);
if (has_quantifiers(rhs))
throw default_exception("quantified formulas in recursive functions are not supported");
}
final_check_status theory_recfun::final_check_eh() {