Complete euf project with eq and diseq on pure representatives

src/qe/qe_mbi.cpp

@@ -33,18 +33,18 @@ Notes:
   Sketch of approach by example:
 
        A: s <= 2a <= t     & f(a) = q
-       
+
        B: t <= 2b <= s + 1 & f(b) != q
 
   1. Extract arithmetic consequences of A over shared vocabulary.
 
-       A -> s <= t & (even(t) | s < t) 
+       A -> s <= t & (even(t) | s < t)
- 
+
   2a. Send to B, have B solve shared variables with EUF_B.
         epsilon b . B & A_pure
-        epsilon b . t <= 2b <= s + 1 & s <= t & (even(t) | s < t) 
+        epsilon b . t <= 2b <= s + 1 & s <= t & (even(t) | s < t)
-        = t <= s + 1 & (even(t) | t <= s) & s <= t & (even(t) | s < t) 
+        = t <= s + 1 & (even(t) | t <= s) & s <= t & (even(t) | s < t)
-        = even(t) & t = s 
+        = even(t) & t = s
         b := t div 2
 
       B & A_pure -> B[b/t div 2] = f(t div 2) != q & t <= s + 1
@@ -53,13 +53,13 @@ Notes:
       A & B_pure -> false
 
       Invoke the ping-pong principle to extract interpolant.
-      
+
   2b. Solve for shared variables with EUF.
 
-    epsilon a . A 
+    epsilon a . A
   = a := (s + 1) div 2 & s < t & f((s + 1) div 2) = q
 
-  3b. Send to B. Produces core 
+  3b. Send to B. Produces core
           s < t & f((s + 1) div 2) = q
 
   4b Solve again in arithmetic for shared variables with EUF.
@@ -71,7 +71,7 @@ Notes:
     Send to B, produces core (s != t | f(t div 2) != q)
 
   5b. There is no longer a solution for A. A is unsat.
-      
+
 --*/
 
 #include "ast/ast_util.h"
@@ -138,7 +138,7 @@ namespace qe {
 
     void prop_mbi_plugin::block(expr_ref_vector const& lits) {
         m_solver->assert_expr(mk_not(mk_and(lits)));
-    }    
+    }
 
     // -------------------------------
     // euf_mbi, TBD
@@ -158,8 +158,8 @@ namespace qe {
         void operator()(expr*) {}
     };
 
-    euf_mbi_plugin::euf_mbi_plugin(solver* s, solver* sNot): 
+    euf_mbi_plugin::euf_mbi_plugin(solver* s, solver* sNot):
-        m(s->get_manager()), 
+        m(s->get_manager()),
         m_atoms(m),
         m_solver(s),
         m_dual_solver(sNot) {
@@ -205,11 +205,11 @@ namespace qe {
                 // use the dual solver to find a 'small' implicant
                 m_dual_solver->get_unsat_core(core);
                 TRACE("qe", tout << "core: " << core << "\n";);
-                // project the implicant onto vars 
+                // project the implicant onto vars
                 tg.set_vars(vars, false);
                 tg.add_lits(core);
-                lits.reset();                
+                lits.reset();
-                lits.append(tg.project());
+                lits.append(tg.project(*mdl));
                 TRACE("qe", tout << "project: " << lits << "\n";);
                 return mbi_sat;
             case l_undef:
@@ -232,8 +232,8 @@ namespace qe {
 
     void euf_mbi_plugin::block(expr_ref_vector const& lits) {
         m_solver->assert_expr(mk_not(mk_and(lits)));
-    }    
+    }
-    
+
 
     /** --------------------------------------------------------------
      * ping-pong interpolation of Gurfinkel & Vizel
@@ -255,7 +255,7 @@ namespace qe {
             auto* t2 = turn ? &b : &a;
             mbi_result next_res = (*t1)(vars, lits, mdl);
             switch (next_res) {
-            case mbi_sat:     
+            case mbi_sat:
                 if (last_res == mbi_sat) {
                     itp = nullptr;
                     return l_true;
@@ -264,7 +264,7 @@ namespace qe {
                 break; // continue
             case mbi_unsat: {
                 if (lits.empty()) {
-                    // TBD, either a => itp and itp => !b 
+                    // TBD, either a => itp and itp => !b
                     // or          b => itp and itp => !a
                     itp = mk_and(itps[!turn]);
                     return l_false;
@@ -282,7 +282,7 @@ namespace qe {
             case mbi_augment:
                 break;
             case mbi_undef:
-                return l_undef;                    
+                return l_undef;
             }
             turn = !turn;
             last_res = next_res;
@@ -319,4 +319,3 @@ namespace qe {
         }
     }
 };
-

src/qe/qe_term_graph.cpp

@@ -24,6 +24,7 @@ Notes:
 #include "ast/for_each_expr.h"
 #include "ast/occurs.h"
 #include "qe/qe_term_graph.h"
+#include "model/model_evaluator.h"
 
 namespace qe {
 
@@ -546,6 +547,7 @@ namespace qe {
             u_map<expr*> m_term2app;
             u_map<expr*> m_root2rep;
 
+            model_ref m_model;
             expr_ref_vector m_pinned;  // tracks expr in the maps
 
             expr* mk_pure(term const& t) {
@@ -565,6 +567,7 @@ namespace qe {
                 return pure;
             }
 
+
             bool is_better_rep(expr *t1, expr *t2) {
                 if (!t2) return t1 != nullptr;
                 return m.is_unique_value(t1) && !m.is_unique_value(t2);
@@ -740,20 +743,49 @@ namespace qe {
                 return is_uninterp_const(rhs) && !occurs(rhs, lhs);
             }
 
+            /// Add equalities and disequalities for all pure representatives
+            /// based on their equivalence in the model
+            void model_complete(expr_ref_vector &res) {
+                if (!m_model) return;
+                obj_map<expr,expr*> val2rep;
+                model_evaluator mev(*m_model);
+                for (auto &kv : m_root2rep) {
+                    expr *rep = kv.m_value;
+                    expr_ref val(m);
+                    expr *u = nullptr;
+                    if (!mev.eval(rep, val)) continue;
+                    if (val2rep.find(val, u)) {
+                        res.push_back(m.mk_eq(u, rep));
+                    }
+                    else {
+                        val2rep.insert(val, rep);
+                    }
+                }
+                ptr_buffer<expr> reps;
+                for (auto &kv : val2rep) {
+                    reps.push_back(kv.m_value);
+                }
+                res.push_back(m.mk_distinct(reps.size(), reps.c_ptr()));
+            }
+
         public:
             projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {}
 
+            void set_model(model &mdl) { m_model = &mdl; }
+
             void reset() {
                 m_tg.reset_marks();
                 m_term2app.reset();
                 m_root2rep.reset();
                 m_pinned.reset();
+                m_model.reset();
             }
             expr_ref_vector project() {
                 expr_ref_vector res(m);
                 purify();
                 mk_lits(res);
                 mk_pure_equalities(res);
+                model_complete(res);
                 reset();
                 return res;
             }
@@ -780,6 +812,13 @@ namespace qe {
         return p.project();
     }
 
+    expr_ref_vector term_graph::project(model &mdl) {
+        m_is_var.reset_solved();
+        projector p(*this);
+        p.set_model(mdl);
+        return p.project();
+    }
+
     expr_ref_vector term_graph::solve() {
         // reset solved vars so that they are not considered pure by projector
         m_is_var.reset_solved();

src/qe/qe_term_graph.h

@@ -23,6 +23,7 @@ Notes:
 #include "util/plugin_manager.h"
 #include "qe/qe_solve_plugin.h"
 #include "qe/qe_vartest.h"
+#include "model/model.h"
 
 namespace qe {
 
@@ -85,8 +86,6 @@ namespace qe {
         void display(std::ostream &out);
 
         bool is_pure_def(expr* atom, expr *& v);
-        void solve_for_vars();
-
 
     public:
         term_graph(ast_manager &m);
@@ -111,9 +110,10 @@ namespace qe {
          * onto the vocabulary of decls (if exclude is false) or outside the
          * vocabulary of decls (if exclude is true).
          */
-         expr_ref_vector project();
+        expr_ref_vector project();
-         expr_ref_vector solve();
+        expr_ref_vector solve();
-        
+        expr_ref_vector project(model &mdl);
+
     };
 
 }