lifting iff to binary

src/sat/smt/euf_solver.cpp

@@ -488,10 +488,8 @@ namespace euf {
             return sat::check_result::CR_CONTINUE;
         if (m_qsolver)
             apply_solver(m_qsolver);
-        if (num_nodes < m_egraph.num_nodes()) {
-            IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n");
+        if (num_nodes < m_egraph.num_nodes()) 
             return sat::check_result::CR_CONTINUE;
-        }
         TRACE("after_search", s().display(tout););
         if (give_up)
             return sat::check_result::CR_GIVEUP;

src/sat/smt/q_ematch.cpp

@@ -427,33 +427,11 @@ namespace q {
             expr_ref body(mk_not(m, q->get_expr()), m);
             q = m.update_quantifier(q, forall_k, body);
         }        
-        expr_ref_vector ors(m);        
+        expr_ref_vector ors(m);
         flatten_or(q->get_expr(), ors);
-        for (expr* arg : ors) {
-            bool sign = m.is_not(arg, arg);
-            expr* l, *r;
-            if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) {
-                l = to_app(arg)->get_arg(0);
-                r = to_app(arg)->get_arg(1);
-                sign = !sign;
-            }
-            else if (!m.is_eq(arg, l, r) || is_ground(arg)) {
-                l = arg;
-                r = sign ? m.mk_false() : m.mk_true();
-                sign = false;
-            }
-            if (m.is_true(l) || m.is_false(l))
-                std::swap(l, r);
-            if (sign && m.is_false(r)) {
-                r = m.mk_true();
-                sign = false;
-            }
-            else if (sign && m.is_true(r)) {
-                r = m.mk_false();
-                sign = false;
-            }
-            cl->m_lits.push_back(lit(expr_ref(l, m), expr_ref(r, m), sign));
-        }
+        for (expr* arg : ors) 
+            cl->m_lits.push_back(clausify_literal(arg));
+
         if (q->get_num_patterns() == 0) {
             expr_ref tmp(m);
             m_infer_patterns(q, tmp); 
@@ -468,6 +446,41 @@ namespace q {
         return cl;
     }
 
+    lit ematch::clausify_literal(expr* arg) {
+        bool sign = m.is_not(arg, arg);
+        expr* _l, *_r;
+        expr_ref l(m), r(m);
+
+        // convert into equality or equivalence
+        if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) {
+            l = to_app(arg)->get_arg(0);
+            r = to_app(arg)->get_arg(1);
+            sign = !sign;
+        }
+        else if (!is_ground(arg) && m.is_eq(arg, _l, _r)) {
+            l = _l;
+            r = _r;
+        }
+        else {
+            l = arg;
+            r = sign ? m.mk_false() : m.mk_true();
+            sign = false;
+        }
+
+        // convert Boolean disequalities into equality
+        if (m.is_true(l) || m.is_false(l))
+            std::swap(l, r);
+        if (sign && m.is_false(r)) {
+            r = m.mk_true();
+            sign = false;
+        }
+        else if (sign && m.is_true(r)) {
+            r = m.mk_false();
+            sign = false;
+        }
+        return lit(l, r, sign);
+    }
+
     /**
      * Attach ground subterms of patterns so they appear shared.
      */

src/sat/smt/q_ematch.h

@@ -112,6 +112,7 @@ namespace q {
 
         void attach_ground_pattern_terms(expr* pat);
         clause* clausify(quantifier* q);
+        lit clausify_literal(expr* arg);
 
         fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation);
         void set_tmp_binding(fingerprint& fp);

src/sat/smt/q_eval.cpp

@@ -171,10 +171,10 @@ namespace q {
     }
 
     euf::enode* eval::operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence) {
-        if (is_ground(e))
-            return ctx.get_egraph().find(e);
         if (m_mark.is_marked(e))
             return m_eval[e->get_id()];
+        if (is_ground(e))
+            return ctx.get_egraph().find(e);
         ptr_buffer<expr> todo;
         ptr_buffer<euf::enode> args;
         todo.push_back(e);

src/sat/smt/q_solver.cpp

@@ -232,6 +232,14 @@ namespace q {
         else
             UNREACHABLE();
 
+        expr* a, *b;
+        if (m_expanded.size() == 1 && m.is_iff(m_expanded.get(0), a, b)) {
+            expr_ref f1(m.mk_implies(a, b), m);
+            expr_ref f2(m.mk_implies(b, a), m);
+            m_expanded.reset();
+            m_expanded.push_back(f1);
+            m_expanded.push_back(f2);
+        }
         if (m_expanded.size() > 1) {
             for (unsigned i = m_expanded.size(); i-- > 0; ) {
                 expr_ref tmp(m.update_quantifier(q, m_expanded.get(i)), m);