3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

fix relevancy bug for recfun

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-30 07:19:57 -08:00
parent 39bfdbd8c0
commit 657ed4db7a
5 changed files with 14 additions and 4 deletions

View file

@ -106,10 +106,13 @@ namespace euf {
SASSERT(!find(f));
force_push();
enode *n = mk_enode(f, generation, num_args, args);
SASSERT(n->class_size() == 1);
if (num_args == 0 && m.is_unique_value(f))
n->mark_interpreted();
if (num_args == 0)
if (m_on_make)
m_on_make(n);
if (num_args == 0)
return n;
if (m.is_eq(f)) {
n->set_is_equality();

View file

@ -168,6 +168,7 @@ namespace euf {
stats m_stats;
bool m_uses_congruence { false };
std::function<void(enode*,enode*)> m_on_merge;
std::function<void(enode*)> m_on_make;
std::function<void(expr*,expr*,expr*)> m_used_eq;
std::function<void(app*,app*)> m_used_cc;
std::function<void(std::ostream&, void*)> m_display_justification;
@ -277,6 +278,7 @@ namespace euf {
void set_bool_var(enode* n, unsigned v) { n->set_bool_var(v); }
void set_on_merge(std::function<void(enode* root,enode* other)>& on_merge) { m_on_merge = on_merge; }
void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; }
void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
void set_display_justification(std::function<void (std::ostream&, void*)> & d) { m_display_justification = d; }

View file

@ -57,7 +57,12 @@ namespace q {
[&](euf::enode* root, euf::enode* other) {
on_merge(root, other);
};
std::function<void(euf::enode*)> _on_make =
[&](euf::enode* n) {
m_mam->relevant_eh(n, false);
};
ctx.get_egraph().set_on_merge(_on_merge);
ctx.get_egraph().set_on_make(_on_make);
m_mam = mam::mk(ctx, *this);
}
@ -230,7 +235,6 @@ namespace q {
m_mam->on_merge(root, other);
if (m_lazy_mam)
m_lazy_mam->on_merge(root, other);
m_mam->relevant_eh(other, false);
}
// watch only nodes introduced in bindings or ground arguments of functions

View file

@ -296,9 +296,12 @@ namespace smt {
}
literal theory_recfun::mk_literal(expr* e) {
bool is_not = m.is_not(e, e);
ctx.internalize(e, false);
literal lit = ctx.get_literal(e);
ctx.mark_as_relevant(lit);
if (is_not)
lit.neg();
return lit;
}

View file

@ -16,7 +16,6 @@ Author:
--*/
#include "util/gparams.h"
#include "util/zstring.h"
#include "util/trace.h"
static bool is_hex_digit(char ch, unsigned& d) {
if ('0' <= ch && ch <= '9') {
@ -148,7 +147,6 @@ std::string zstring::encode() const {
}
}
_flush();
TRACE("seq", tout << "encode " << strm.str() << "\n";);
return strm.str();
}