mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-23 23:42:33 +00:00
Code Activity

disable term enumeration by default

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-10 14:23:40 -07:00
parent 1d425e55cd
commit 382abb786a
7 changed files with 33 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/seq_regex.cpp
View file

@ -872,7 +872,9 @@ namespace smt {
lits.push_back(~lit);
if (!m.is_true(cond)) {
expr_ref ncond(mk_not(m, cond), m);
lits.push_back(th.mk_literal(mk_forall(m, hd, ncond)));
expr_ref facond = mk_forall(m, hd, ncond);
ctx.internalize(facond, true); // make sure fa is internalized, and assumed in positive polarity only.
lits.push_back(th.mk_literal(facond));
}
expr_ref is_empty1 = sk().mk_is_empty(r, re().mk_union(u, r), n);
lits.push_back(th.mk_literal(is_empty1));

2
src/smt/smt_context.h
View file

@ -983,6 +983,8 @@ namespace smt {
void internalize(expr * n, bool gate_ctx, unsigned generation);
enode *non_ground_internalize(expr *e);
clause * mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k = CLS_AUX, clause_del_eh * del_eh = nullptr);
void mk_clause(literal l1, literal l2, justification * j);

22
src/smt/smt_internalizer.cpp
View file

@ -419,6 +419,28 @@ namespace smt {
internalize_rec(n, gate_ctx);
}
enode *context::non_ground_internalize(expr *e) {
if (e_internalized(e))
return get_enode(e);
if (is_ground(e)) {
internalize(e, false);
return get_enode(e);
}
for (auto arg : subterms::ground(expr_ref(e, m))) {
if ((is_forall(arg) || is_exists(arg)) && !e_internalized(arg)) {
expr_ref fn(m.mk_fresh_const("proxy-expr", e->get_sort()), m);
expr_ref eq(m.mk_eq(fn, e), m);
assert_expr(eq);
internalize_assertions();
if (!e_internalized(fn))
internalize(fn, false);
return get_enode(fn);
}
}
internalize(e, false);
return get_enode(e);
}
void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) {
internalize_deep(exprs, num_exprs);
for (unsigned i = 0; i < num_exprs; ++i)

3
src/smt/smt_theory.cpp
View file

@ -152,7 +152,8 @@ namespace smt {
expr_ref e(_e, m);
bool is_not = m.is_not(_e, _e);
if (!ctx.e_internalized(_e)) {
ctx.internalize(_e, is_quantifier(_e));
auto n = ctx.non_ground_internalize(_e);
_e = n->get_expr();
}
literal lit = ctx.get_literal(_e);
ctx.mark_as_relevant(lit);

13
src/smt/theory_array_full.cpp
View file

@ -626,17 +626,8 @@ namespace smt {
for (unsigned i = 0; i < lam->get_num_decls(); ++i)
args.push_back(mk_epsilon(lam->get_decl_sort(i)).first);
expr_ref val(mk_select(args), m);
ctx.get_rewriter()(val);
if (has_quantifiers(val)) {
expr_ref fn(m.mk_fresh_const("lambda-body", val->get_sort()), m);
expr_ref eq(m.mk_eq(fn, val), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
val = fn;
}
ctx.internalize(def, false);
ctx.internalize(val.get(), false);
return try_assign_eq(val.get(), def);
auto val_e = ctx.non_ground_internalize(val);
return try_assign_eq(val_e->get_expr(), def);
}
bool theory_array_full::instantiate_choice_axiom(enode* ch) {