From 5fe2ff84e9cac0ecabe2a7d86cdf36691f69dce4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Nov 2022 19:45:16 +0700 Subject: [PATCH] change functionality to not track ite terms for congruence closure --- src/sat/smt/euf_internalize.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 792ffcf1d..a1d383e45 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -468,12 +468,13 @@ namespace euf { euf::enode* solver::mk_enode(expr* e, unsigned num, enode* const* args) { + // + // Don't track congruences of Boolean connectives or arguments. + // The assignments to associated literals is sufficient + // + if (si.is_bool_op(e)) num = 0; - - enode* n = m_egraph.mk(e, m_generation, num, args); - if (si.is_bool_op(e)) - m_egraph.set_cgc_enabled(n, false); // // (if p th el) (non-Boolean case) produces clauses @@ -484,6 +485,10 @@ namespace euf { // if (m.is_ite(e)) num = 0; + + enode* n = m_egraph.mk(e, m_generation, num, args); + if (si.is_bool_op(e)) + m_egraph.set_cgc_enabled(n, false); // // To track congruences of Boolean children under non-Boolean