na

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

src/math/polysat/solver.cpp

@@ -521,6 +521,7 @@ namespace polysat {
         m_cjust[v].append(m_conflict);
         m_conflict.reset();
         add_non_viable(v, val);
+        narrow(v);
         decide(v);
     }
     
@@ -556,6 +557,14 @@ namespace polysat {
         return nullptr;
     }
 
+    /**
+     * placeholder for factoring/gcd common factors
+     */
+    void solver::narrow(pvar v) {
+
+    }
+
+
     bool solver::is_always_false(constraint& c) {
         if (c.is_eq()) 
             return c.p().is_never_zero();

src/math/polysat/solver.h

@@ -137,6 +137,8 @@ namespace polysat {
         void decide();
         void decide(pvar v);
 
+        void narrow(pvar v);
+
         p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); }
 
         bool is_conflict() const { return !m_conflict.empty(); }