mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
probably won't fix #6127
recfun decl plugin does not get copied so recursive functions are lost when cloning. Fix is risky and use case is limited to threads + recursive definitions
This commit is contained in:
parent
ac8aaed1d4
commit
6ed2b444b5
|
@ -43,32 +43,32 @@ namespace smt {
|
|||
|
||||
char const * theory_recfun::get_name() const { return "recfun"; }
|
||||
|
||||
theory* theory_recfun::mk_fresh(context* new_ctx) {
|
||||
theory* theory_recfun::mk_fresh(context* new_ctx) {
|
||||
return alloc(theory_recfun, *new_ctx);
|
||||
}
|
||||
|
||||
bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
|
||||
TRACE("recfun", tout << mk_pp(atom, m) << " " << u().has_defs() << "\n");
|
||||
if (!u().has_defs()) {
|
||||
// if (u().is_defined(atom))
|
||||
// throw default_exception("recursive atom definition is out of scope");
|
||||
return false;
|
||||
}
|
||||
for (expr * arg : *atom) {
|
||||
for (expr * arg : *atom)
|
||||
ctx.internalize(arg, false);
|
||||
}
|
||||
if (!ctx.e_internalized(atom)) {
|
||||
if (!ctx.e_internalized(atom))
|
||||
ctx.mk_enode(atom, false, true, true);
|
||||
}
|
||||
if (!ctx.b_internalized(atom)) {
|
||||
bool_var v = ctx.mk_bool_var(atom);
|
||||
ctx.set_var_theory(v, get_id());
|
||||
}
|
||||
if (!ctx.relevancy() && u().is_defined(atom)) {
|
||||
if (!ctx.b_internalized(atom))
|
||||
ctx.set_var_theory(ctx.mk_bool_var(atom), get_id());
|
||||
if (!ctx.relevancy() && u().is_defined(atom))
|
||||
push_case_expand(atom);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool theory_recfun::internalize_term(app * term) {
|
||||
if (!u().has_defs()) {
|
||||
// if (u().is_defined(term))
|
||||
// throw default_exception("recursive term definition is out of scope");
|
||||
return false;
|
||||
}
|
||||
for (expr* e : *term) {
|
||||
|
|
Loading…
Reference in a new issue