enable propagation

src/sat/smt/q_ematch.cpp

@@ -31,6 +31,7 @@ Done:
 #include "ast/ast_util.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/rewriter/rewriter_def.h"
+#include "ast/normal_forms/pull_quant.h"
 #include "solver/solver.h"
 #include "sat/smt/sat_th.h"
 #include "sat/smt/euf_solver.h"
@@ -116,12 +117,16 @@ namespace q {
     }
 
     quantifier_ref ematch::nnf_skolem(quantifier* q) {
+        SASSERT(is_forall(q));
         expr_ref r(m);
         proof_ref p(m);
         m_new_defs.reset();
         m_new_proofs.reset();
         m_nnf(q, m_new_defs, m_new_proofs, r, p);
-        SASSERT(is_quantifier(r));
+        SASSERT(is_forall(r));
+        pull_quant pull(m);
+        pull(r, r, p);
+        SASSERT(is_forall(r));
         for (expr* d : m_new_defs)
             m_qs.add_unit(m_qs.mk_literal(d));
         CTRACE("q", r != q, tout << mk_pp(q, m) << " -->\n" << r << "\n" << m_new_defs << "\n";);
@@ -301,7 +306,7 @@ namespace q {
         TRACE("q", b->display(ctx, tout << "on-binding " << mk_pp(q, m) << "\n") << "\n";);
 
 
-        if (false && propagate(false, _binding, max_generation, c, new_propagation))
+        if (propagate(false, _binding, max_generation, c, new_propagation))
             return;
 
         binding::push_to_front(c.m_bindings, b);
@@ -310,6 +315,10 @@ namespace q {
     }
 
     bool ematch::propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& propagated) {
+        if (!m_enable_propagate)
+            return false;
+        if (ctx.s().inconsistent())
+            return true;
         TRACE("q", c.display(ctx, tout) << "\n";);
         unsigned idx = UINT_MAX;
         m_evidence.reset();
@@ -337,7 +346,7 @@ namespace q {
             propagate(ev == l_false, idx, j_idx);
         else
             m_prop_queue.push_back(prop(ev == l_false, idx, j_idx));
-        propagated = true;
+        propagated = true;        
         return true;
     }
 
@@ -576,7 +585,7 @@ namespace q {
 
 
     bool ematch::unit_propagate() {
-        return false;
+        // return false;
         return ctx.get_config().m_ematching && propagate(false);
     }
 
@@ -595,7 +604,7 @@ namespace q {
                 continue;
 
             do {                
-                if (false && propagate(true, b->m_nodes, b->m_max_generation, c, propagated)) 
+                if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated)) 
                     to_remove.push_back(b);
                 else if (flush) {
                     instantiate(*b);
@@ -648,7 +657,7 @@ namespace q {
     void ematch::collect_statistics(statistics& st) const {
         m_inst_queue.collect_statistics(st);
         st.update("q redundant", m_stats.m_num_redundant);
-        st.update("q units",     m_stats.m_num_propagations);
+        st.update("q unit propagations",     m_stats.m_num_propagations);
         st.update("q conflicts", m_stats.m_num_conflicts);
         st.update("q delayed bindings", m_stats.m_num_delayed_bindings);
     }

src/sat/smt/q_ematch.h

@@ -89,6 +89,7 @@ namespace q {
         unsigned                      m_qhead = 0;
         unsigned_vector               m_clause_queue;
         euf::enode_pair_vector        m_evidence;
+        bool                          m_enable_propagate = true;
 
         euf::enode* const* copy_nodes(clause& c, euf::enode* const* _binding);
         binding* tmp_binding(clause& c, app* pat, euf::enode* const* _binding);

src/sat/smt/q_mam.cpp

@@ -3095,7 +3095,7 @@ namespace q {
         void add_candidate(code_tree * t, enode * app) {
             if (!t)
                 return;
-            TRACE("q", tout << "candidate " << t << " " << ctx.bpp(app) << "\n";);
+            TRACE("q", tout << "candidate " << ctx.bpp(app) << "\n";);
             if (!t->has_candidates()) {
                 ctx.push(push_back_trail<code_tree*, false>(m_to_match));
                 m_to_match.push_back(t);

src/sat/smt/q_mbi.cpp

@@ -155,7 +155,7 @@ namespace q {
         unsigned inc = 1;
         while (true) {
             ::solver::scoped_push _sp(*m_solver);
-            add_universe_restriction(q, *qb);
+            add_universe_restriction(*qb);
             m_solver->assert_expr(qb->mbody);
             ++m_stats.m_num_checks;
             lbool r = m_solver->check_sat(0, nullptr);
@@ -217,17 +217,17 @@ namespace q {
             qlit.neg();
         ctx.rewrite(proj);
         TRACE("q", tout << "project: " << proj << "\n";);
+        IF_VERBOSE(11, verbose_stream() << "mbi:\n" << mk_pp(q, m) << "\n" << proj << "\n");
         ++m_stats.m_num_instantiations;        
         unsigned generation = ctx.get_max_generation(proj);    
         m_instantiations.push_back(instantiation_t(qlit, proj, generation));
     }
 
-    void mbqi::add_universe_restriction(quantifier* q, q_body& qb) {
+    void mbqi::add_universe_restriction(q_body& qb) {
-        unsigned sz = q->get_num_decls();
+        for (app* v : qb.vars) {
-        for (unsigned i = 0; i < sz; ++i) {
+            sort* s = v->get_sort();
-            sort* s = q->get_decl_sort(i);
             if (m_model->has_uninterpreted_sort(s))
-                restrict_to_universe(qb.vars.get(i), m_model->get_universe(s));
+                restrict_to_universe(v, m_model->get_universe(s));
         }
     }
 

src/sat/smt/q_mbi.h

@@ -83,7 +83,7 @@ namespace q {
         q_body* specialize(quantifier* q);
         q_body* q2body(quantifier* q);
         expr_ref solver_project(model& mdl, q_body& qb, expr_ref_vector& eqs, bool use_inst);
-        void add_universe_restriction(quantifier* q, q_body& qb);
+        void add_universe_restriction(q_body& qb);
         void add_domain_eqs(model& mdl, q_body& qb);
         void add_domain_bounds(model& mdl, q_body& qb);
         void eliminate_nested_vars(expr_ref_vector& fmls, q_body& qb);

src/sat/smt/q_queue.cpp

@@ -146,7 +146,7 @@ namespace q {
                 
         unsigned gen = get_new_gen(f, ent.m_cost);
         bool new_propagation = false;
-        if (false && em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
+        if (em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
             return;
 
 

src/sat/smt/q_solver.cpp

@@ -19,6 +19,7 @@ Author:
 #include "ast/well_sorted.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/normal_forms/pull_quant.h"
+#include "ast/rewriter/inj_axiom.h"
 #include "sat/smt/q_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/sat_th.h"
@@ -69,9 +70,12 @@ namespace q {
 
         if (ctx.get_config().m_mbqi) {
             switch (m_mbqi()) {
-            case l_true:  return sat::check_result::CR_DONE;
+            case l_true:  
-            case l_false: return sat::check_result::CR_CONTINUE;
+                return sat::check_result::CR_DONE;
-            case l_undef: break;
+            case l_false: 
+                return sat::check_result::CR_CONTINUE;
+            case l_undef: 
+                break;
             }
         }
         return sat::check_result::CR_GIVEUP;
@@ -166,13 +170,18 @@ namespace q {
 
     quantifier* solver::flatten(quantifier* q) {
         quantifier* q_flat = nullptr;
-        if (!has_quantifiers(q->get_expr())) 
-            return q;
         if (m_flat.find(q, q_flat))
             return q_flat;
+
+        expr_ref new_q(m);
         proof_ref pr(m);
-        expr_ref  new_q(m);
+        if (!has_quantifiers(q->get_expr())) {
-        if (is_forall(q)) {
+            if (!ctx.get_config().m_refine_inj_axiom)
+                return q;
+            if (!simplify_inj_axiom(m, q, new_q))
+                return q;
+        }
+        else if (is_forall(q)) {
             pull_quant pull(m);
             pull(q, new_q, pr);
             SASSERT(is_well_sorted(m, new_q));