move more equality functionality

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

src/math/polysat/constraint.cpp

@@ -134,4 +134,22 @@ namespace polysat {
         return false;
     }
 
+    constraint* eq_constraint::resolve(solver& s, pvar v) {
+        if (s.m_conflict.size() != 1)
+            return nullptr;
+        constraint* c = s.m_conflict[0];
+        if (c->is_eq()) {
+            pdd a = c->to_eq().p();
+            pdd b = p();
+            pdd r = a;
+            if (!a.resolve(v, b, r)) 
+                return nullptr;
+            p_dependency_ref d(s.m_dm.mk_join(c->dep(), dep()), s.m_dm);
+            // d = ;
+            unsigned lvl = std::max(c->level(), level());
+            return constraint::eq(lvl, r, d);             
+        }
+        return nullptr;
+    }
+
 }

src/math/polysat/constraint.h

@@ -42,6 +42,7 @@ namespace polysat {
         ckind_t kind() const { return m_kind; }
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual bool propagate(solver& s, pvar v) = 0;
+        virtual constraint* resolve(solver& s, pvar v) = 0;
         eq_constraint& to_eq();
         eq_constraint const& to_eq() const;
         p_dependency* dep() const { return m_dep; }
@@ -58,8 +59,8 @@ namespace polysat {
         }
         pdd const & p() const { return m_poly; }
         std::ostream& display(std::ostream& out) const override;
-
         bool propagate(solver& s, pvar v) override;
+        constraint* resolve(solver& s, pvar v) override;
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }

src/math/polysat/solver.cpp

@@ -202,29 +202,13 @@ namespace polysat {
         auto& wlist = m_watch[v];
         unsigned i = 0, j = 0, sz = wlist.size();
         for (; i < sz && !is_conflict(); ++i) 
-            if (!propagate(v, *wlist[i]))
+            if (!wlist[i]->propagate(*this, v))
                 wlist[j++] = wlist[i];
         for (; i < sz; ++i)
             wlist[j++] = wlist[i];
         wlist.shrink(j);
     }
 
-    /**
-     * Return true iff the constraint should be removed from the current watch list.
-     */
-    bool solver::propagate(pvar v, constraint& c) {
-        switch (c.kind()) {
-        case ckind_t::eq_t:
-            return c.to_eq().propagate(*this, v);
-        case ckind_t::ule_t:
-        case ckind_t::sle_t:
-            NOT_IMPLEMENTED_YET();
-            return false;
-        }
-        UNREACHABLE();
-        return false;
-    }
-
     void solver::propagate(pvar v, rational const& val, constraint& c) {
         if (is_viable(v, val)) {
             m_free_vars.del_var_eh(v);
@@ -534,24 +518,10 @@ namespace polysat {
     constraint* solver::resolve(pvar v) {
         SASSERT(!m_cjust[v].empty());
         SASSERT(m_justification[v].is_propagation());
-        if (m_conflict.size() > 1)
+        if (m_cjust[v].size() != 1)
             return nullptr;
-        if (m_cjust[v].size() > 1)
-            return nullptr;
-        constraint* c = m_conflict[0];
         constraint* d = m_cjust[v].back();
-        if (c->is_eq() && d->is_eq()) {
+        return d->resolve(*this, v);
-            pdd p = c->to_eq().p();
-            pdd q = d->to_eq().p();
-            pdd r = p;
-            if (!p.resolve(v, q, r)) 
-                return nullptr;
-            p_dependency_ref dep(m_dm);
-            dep = m_dm.mk_join(c->dep(), d->dep());
-            unsigned level = std::max(c->level(), d->level());
-            return constraint::eq(level, r, dep);             
-        }
-        return nullptr;
     }
 
     /**

src/math/polysat/solver.h

@@ -121,7 +121,6 @@ namespace polysat {
         bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }
 
         void propagate(pvar v);
-        bool propagate(pvar v, constraint& c);
         void propagate(pvar v, rational const& val, constraint& c);
         void erase_watch(pvar v, constraint& c);
         void erase_watch(constraint& c);