mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 10:26:16 +00:00
Code Activity

fix #6865

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-18 16:51:58 -07:00
parent a8c4384536
commit c3b344ec47
1 changed files with 7 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/qe/mbp/mbp_basic_tg.cpp
View file

@ -47,36 +47,27 @@ struct mbp_basic_tg::impl {
//they contain variables/are c-ground //they contain variables/are c-ground
bool apply() { bool apply() {
if (!m_use_mdl) return false; if (!m_use_mdl) return false;
expr *term, *c, *th, *el; expr *c, *th, *el;
expr_ref nterm(m); expr_ref nterm(m);
bool progress = false; bool progress = false;
TRACE("mbp_tg", tout << "Iterating over terms of tg";); TRACE("mbp_tg", tout << "Iterating over terms of tg";);
// Not resetting terms because get_terms calls resize on terms // Not resetting terms because get_terms calls resize on terms
m_tg.get_terms(terms, false); m_tg.get_terms(terms, false);
for (unsigned i = 0; i < terms.size(); i++) { for (expr* term : terms) {
term = terms.get(i); if (is_seen(term))
// Unsupported operators continue;
SASSERT(!m.is_and(term));
SASSERT(!m.is_or(term));
SASSERT(!m.is_distinct(term));
SASSERT(!m.is_implies(term));
if (is_seen(term)) continue;
if (m.is_ite(term, c, th, el)) { if (m.is_ite(term, c, th, el)) {
mark_seen(term); mark_seen(term);
progress = true; progress = true;
if (m_mdl.is_true(c)) { if (m_mdl.is_true(c)) {
m_tg.add_lit(c); m_tg.add_lit(c);
m_tg.add_eq(term, th); m_tg.add_eq(term, th);
} else { }
if (m.is_not(c)) else {
nterm = to_app(c)->get_arg(0); nterm = mk_not(m, c);
else
nterm = m.mk_not(c);
m_tg.add_lit(nterm); m_tg.add_lit(nterm);
m_tg.add_eq(term, el); m_tg.add_eq(term, el);
} }
continue;
} }
} }
return progress; return progress;