na

src/sat/smt/q_ematch.cpp

@@ -21,10 +21,11 @@ Todo:
 - insert instantiations into priority queue 
 - cache instantiations and substitutions
 - nested quantifiers
-- non-cnf quantifiers
+- non-cnf quantifiers (handled in q_solver)
 
 --*/
 
+#include "ast/ast_util.h"
 #include "ast/rewriter/var_subst.h"
 #include "solver/solver.h"
 #include "sat/smt/sat_th.h"
@@ -365,9 +366,31 @@ namespace q {
         return propagated;
     }
 
+    /**
+     * basic clausifier, assumes q has been normalized.
+     */
     ematch::clause* ematch::clausify(quantifier* q) {
-        NOT_IMPLEMENTED_YET();
-        return nullptr;
+        clause* cl = alloc(clause);
+        expr_ref_vector ors(m);        
+        if (is_forall(q)) 
+            flatten_or(q->get_expr(), ors);
+        else {
+            flatten_and(q->get_expr(), ors);
+            for (unsigned i = 0; i < ors.size(); ++i)
+                ors[i] = mk_not(m, ors.get(i));
+        }
+        for (expr* arg : ors) {
+            bool sign = m.is_not(arg, arg);
+            expr* l, *r;
+            if (!m.is_eq(arg, l, r) || is_ground(arg)) {
+                l = arg;
+                r = sign ? m.mk_false() : m.mk_true();
+                sign = false;
+            }
+            cl->m_lits.push_back(lit(expr_ref(l, m), expr_ref(r, m), sign));
+        }
+        cl->m_q = q;
+        return cl;
     }
 
     /**
@@ -389,6 +412,7 @@ namespace q {
         pop_clause(ematch& em): em(em) {}
         void undo(euf::solver& ctx) override {
             em.m_q2clauses.remove(em.m_clauses.back()->m_q);
+            dealloc(em.m_clauses.back());
             em.m_clauses.pop_back();
         }
     };

src/sat/smt/q_ematch.h

@@ -45,7 +45,7 @@ namespace q {
             expr_ref lhs;
             expr_ref rhs;
             bool     sign;
-            lit(expr_ref& lhs, expr_ref& rhs, bool sign):
+            lit(expr_ref const& lhs, expr_ref const& rhs, bool sign):
                 lhs(lhs), rhs(rhs), sign(sign) {}
             
         };

src/sat/smt/q_solver.cpp

@@ -29,6 +29,7 @@ namespace q {
     solver::solver(euf::solver& ctx, family_id fid) :
         th_euf_solver(ctx, ctx.get_manager().get_family_name(fid), fid),
         m_mbqi(ctx,  *this),
+        m_ematch(ctx, *this),
         m_expanded(ctx.get_manager())
     {
     }
@@ -48,17 +49,24 @@ namespace q {
 
         if (l.sign() == is_forall(e)) 
             add_clause(~l, skolemize(q));
-        else 
+        else {
             ctx.push_vec(m_universal, l);
+            if (ctx.get_config().m_ematching)
+                m_ematch.add(q);
+        }
         m_stats.m_num_quantifier_asserts++;
     }
 
     sat::check_result solver::check() {
+        if (ctx.get_config().m_ematching) 
+            if (!m_ematch())
+                return sat::check_result::CR_CONTINUE;
+
         if (ctx.get_config().m_mbqi) {
             switch (m_mbqi()) {
             case l_true:  return sat::check_result::CR_DONE;
             case l_false: return sat::check_result::CR_CONTINUE;
-            case l_undef: return sat::check_result::CR_GIVEUP;
+            case l_undef: break;
             }
         }
         return sat::check_result::CR_GIVEUP;
@@ -79,7 +87,7 @@ namespace q {
     }
 
     bool solver::unit_propagate() {
-        return false;
+        return ctx.get_config().m_ematching && m_ematch.propagate();
     }
 
     euf::theory_var solver::mk_var(euf::enode* n) {
@@ -231,6 +239,42 @@ namespace q {
             }
             return m_expanded;
         }
+
+#if 0
+        m_expanded.reset();
+        m_expanded2.reset();
+        if (is_forall(q)) 
+            flatten_or(q->get_expr(), m_expanded2);
+        else if (is_exists(q)) 
+            flatten_and(q->get_expr(), m_expanded2);
+        else
+            UNREACHABLE();
+        for (unsigned i = m_expanded2.size(); i-- > 0; ) {
+            expr* lit = m_expanded2.get(i);
+            if (!is_ground(lit) && is_and(lit) && is_forall(q)) {
+
+                // get free vars of lit
+                // create fresh predicate over free vars
+                // replace in expanded, pack and push on m_expanded
+                
+                expr_ref p(m);
+                // TODO introduce fresh p.
+                flatten_and(lit, m_expanded);
+                for (unsigned i = m_expanded.size(); i-- > 0; ) {
+                    tmp = m.mk_or(m.mk_not(p), m_expanded.get(i));
+                    expr_ref tmp(m.update_quantifier(q, tmp), m);
+                    ctx.get_rewriter()(tmp);
+                    m_expanded[i] = tmp;
+                }
+                m_expanded2[i] = p;
+                tmp = m.mk_or(m_expanded2);
+                expr_ref tmp(m.update_quantifier(q, tmp), m);
+                ctx.get_rewriter()(tmp);                
+                m_expanded.push_back(tmp);
+                return m_expanded;
+            }
+        }
+#endif
         m_expanded.reset();
         m_expanded.push_back(q);
         return m_expanded;

src/sat/smt/q_solver.h

@@ -20,6 +20,7 @@ Author:
 #include "ast/ast_trail.h"
 #include "sat/smt/sat_th.h"
 #include "sat/smt/q_mbi.h"
+#include "sat/smt/q_ematch.h"
 
 namespace euf {
     class solver;
@@ -40,6 +41,7 @@ namespace q {
 
         stats                  m_stats;
         mbqi                   m_mbqi;
+        ematch                 m_ematch;
 
         flat_table             m_flat;
         sat::literal_vector    m_universal;

src/smt/theory_char.cpp

@@ -15,7 +15,6 @@ Author:
 
 --*/
 
-#include "ast/bv_decl_plugin.h"
 #include "smt/theory_char.h"
 #include "smt/smt_context.h"
 #include "smt/smt_model_generator.h"