experiment with delayed disequalities

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/smt/euf_solver.cpp

@@ -172,7 +172,7 @@ namespace euf {
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
     }
 
-    void solver::init_search() {        
+    void solver::init_search() {
         TRACE("before_search", s().display(tout););
         m_reason_unknown.clear();
         for (auto* s : m_solvers)

src/sat/smt/q_solver.cpp

@@ -45,10 +45,15 @@ namespace q {
         quantifier* q = to_quantifier(e);
 
         if (l.sign() == is_forall(e)) {
+            if (m_quantifiers_are_positive && is_forall(e))
+                return;
             sat::literal lit = skolemize(q);
             add_clause(~l, lit);
             return;
         }
+        if (m_quantifiers_are_positive && is_exists(e))
+            return;
+
         quantifier* q_flat = nullptr;
         if (!m_flat.find(q, q_flat)) {
             if (expand(q)) {
@@ -141,10 +146,37 @@ namespace q {
         return mk_literal(body);
     }
 
+    class insert_skolem : public trail {
+        obj_map<quantifier, expr_ref_vector*>& sk;
+        quantifier* q;
+    public:
+        insert_skolem(obj_map<quantifier, expr_ref_vector*>& sk, quantifier* q):
+            sk(sk),
+            q(q)
+        {}
+        void undo() override {
+            dealloc(sk[q]);
+            sk.remove(q);
+        }
+    };
+
     sat::literal solver::skolemize(quantifier* q) {
+        expr_ref_vector* sk = nullptr;
         std::function<expr* (quantifier*, unsigned)> mk_var = [&](quantifier* q, unsigned i) {
-            return m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i));
+            expr * t = nullptr;
+            if (sk->size() <= i) {
+                t = m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i));
+                sk->push_back(t);
+            }
+            else
+                t = sk->get(i);                
+            return t;
         };
+        if (!m_skolems.find(q, sk)) {
+            sk = alloc(expr_ref_vector, m);
+            m_skolems.insert(q, sk);
+            ctx.push(insert_skolem(m_skolems, q));
+        }
         return instantiate(q, is_forall(q), mk_var);
     }
 

src/sat/smt/q_solver.h

@@ -68,6 +68,8 @@ namespace q {
         obj_map<sort, expr*>   m_unit_table;
         expr_ref_vector        m_expanded;
         der_rewriter           m_der;
+        bool                   m_quantifiers_are_positive = false;
+        obj_map<quantifier, expr_ref_vector*> m_skolems;
 
         sat::literal instantiate(quantifier* q, bool negate, std::function<expr* (quantifier*, unsigned)>& mk_var);
         sat::literal skolemize(quantifier* q);

src/smt/theory_arith_core.h

@@ -1466,7 +1466,6 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::restart_eh() {
-        return;
         m_arith_eq_adapter.restart_eh();
     }
 

src/smt/theory_lra.cpp

@@ -1304,17 +1304,60 @@ public:
         TRACE("arith", tout << "eq " << v1 << " == " << v2 << "\n";);
         if (!is_int(v1) && !is_real(v1)) 
             return;
-        m_arith_eq_adapter.new_eq_eh(v1, v2);
+
+        if (true) {
+            enode* n1 = get_enode(v1);
+            enode* n2 = get_enode(v2);
+            lpvar w1 = register_theory_var_in_lar_solver(v1);
+            lpvar w2 = register_theory_var_in_lar_solver(v2);
+            auto cs = lp().add_equality(w1, w2);            
+            add_eq_constraint(cs.first, n1, n2);
+            add_eq_constraint(cs.second, n1, n2);
+        }
+        else {        
+            m_arith_eq_adapter.new_eq_eh(v1, v2);
+        }
     }
 
     bool use_diseqs() const {
         return true;
     }
 
+    svector<std::pair<theory_var, theory_var>> m_diseqs;
+    unsigned m_diseqs_qhead = 0;
+
     void new_diseq_eh(theory_var v1, theory_var v2) {
         TRACE("arith", tout << "v" << v1 << " != " << "v" << v2 << "\n";);
         ++m_stats.m_assert_diseq;
-        m_arith_eq_adapter.new_diseq_eh(v1, v2);
+        if (false) {
+            if (is_eq(v1, v2)) {
+                m_arith_eq_adapter.new_diseq_eh(v1, v2);
+            }
+            else {
+                m_diseqs.push_back({v1, v2});
+                ctx().push_trail(push_back_vector(m_diseqs));
+            }
+        }
+        else 
+            m_arith_eq_adapter.new_diseq_eh(v1, v2);
+    }
+
+    bool delayed_diseqs() {
+        if (m_diseqs_qhead == m_diseqs.size())
+            return false;
+        verbose_stream() << m_diseqs_qhead << " out of " << m_diseqs.size() << "\n";
+        ctx().push_trail(value_trail(m_diseqs_qhead));
+        bool has_eq = false;
+        while (m_diseqs_qhead < m_diseqs.size()) {
+            auto [v1,v2] = m_diseqs[m_diseqs_qhead];
+            if (is_eq(v1, v2)) {
+                verbose_stream() << "bad diseq " << m_diseqs_qhead << "\n";
+                m_arith_eq_adapter.new_diseq_eh(v1, v2);
+                has_eq = true;
+            }
+            ++m_diseqs_qhead;
+        }
+        return has_eq;
     }
 
     void apply_sort_cnstr(enode* n, sort*) {
@@ -1361,7 +1404,6 @@ public:
     }
 
     void restart_eh() {
-        return;
         m_arith_eq_adapter.restart_eh();
     }
 
@@ -1800,6 +1842,10 @@ public:
         TRACE("arith", display(tout););
         random_update();
         m_model_eqs.reset();
+
+        if (delayed_diseqs())
+            return true;
+        
                         
         theory_var sz = static_cast<theory_var>(th.get_num_vars());            
         unsigned old_sz = m_assume_eq_candidates.size();
@@ -1943,7 +1989,7 @@ public:
 
     final_check_status final_check_eh() {
 
-        //        verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n";
+        // verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n";
         //ctx().display(verbose_stream());
         //exit(0);