n

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

src/math/dd/dd_pdd.cpp

@@ -960,13 +960,19 @@ namespace dd {
         pdd r = zero();
         a.factor(v, l, a1, a2);
         b.factor(v, m, b1, b2);
+        std::cout << "factor v*" << a1 << " ++ " << a2 << "\n";
+        std::cout << "factor v*" << b1 << " ++ " << b2 << "\n";
 
         quot_rem(a1, b1, q, r);
+        std::cout << "quot " << q << " rem " << r << "\n";
         if (r.is_zero()) {
             SASSERT(q * b1 == a1);
             a1 = -q * pow(mk_var(v), l - m) * b2;
             if (l > m)
                 a1 = reduce(v, a1, b);
+        }
+        else if (m_semantics == mod2N_e && r.is_val() && r.val().is_odd() && q.is_zero()) {
+            
         }
         else 
             a1 = a1 * pow(mk_var(v), l);        

src/math/polysat/explain.cpp

@@ -157,11 +157,13 @@ namespace polysat {
             auto rhs = c->to_ule().rhs();
             auto a = lhs.reduce(v, p);
             auto b = rhs.reduce(v, p);
+            LOG("try-reduce: " << c << " " << a << " " << b << " vs " << lhs << " " << rhs);
             if (a == lhs && b == rhs)
                 continue;
             auto c2 = s.ule(a, b);
             if (!c.is_positive())
                 c2 = ~c2;
+            LOG("try-reduce is false " << c2.is_currently_false(s));
             if (!c2.is_currently_false(s))
                 continue;
             SASSERT(c2.is_currently_false(s));

src/math/polysat/mul_ovfl_constraint.cpp

@@ -100,11 +100,7 @@ namespace polysat {
     }
 
     /**
-    * if p constant, q, propagate inequality
-    * 
-    * TODO optimizations:
-    * if p is constant, q variable, update viable for q
-    * 
+    * if p constant, q, propagate inequality   
     */
     bool mul_ovfl_constraint::narrow_bound(solver& s, bool is_positive, 
         pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) {
@@ -148,7 +144,7 @@ namespace polysat {
     }
 
     unsigned mul_ovfl_constraint::hash() const {
-    	return mk_mix(p().hash(), q().hash(), 325);
+    	return mk_mix(p().hash(), q().hash(), kind());
     }
 
     bool mul_ovfl_constraint::operator==(constraint const& other) const {

src/math/polysat/ule_constraint.cpp

@@ -208,7 +208,7 @@ namespace polysat {
     }
 
     unsigned ule_constraint::hash() const {
-    	return mk_mix(lhs().hash(), rhs().hash(), 23);
+    	return mk_mix(lhs().hash(), rhs().hash(), kind());
     }
     
     bool ule_constraint::operator==(constraint const& other) const {

src/test/polysat.cpp

@@ -19,8 +19,12 @@ namespace polysat {
     public:
         scoped_solver(std::string name): solver(lim), m_name(name) {
             LOG("\n\n\n" << std::string(78, '#') << "\n\nSTART: " << m_name << "\n");
+            set_max_conflicts(10);
+        }
+
+        void set_max_conflicts(unsigned c) {
             params_ref p;
-            p.set_uint("max_conflicts", 10);
+            p.set_uint("max_conflicts", c);
             updt_params(p);
         }
 
@@ -942,6 +946,7 @@ namespace polysat {
 
     static void test_quot_rem(unsigned bw = 32) {
         scoped_solver s(__func__);
+        s.set_max_conflicts(2);
         auto a = s.var(s.add_var(bw));
         auto quot = s.var(s.add_var(bw));
         auto rem = s.var(s.add_var(bw));