add note about a bug

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

src/math/dd/dd_pdd.cpp

@@ -859,7 +859,7 @@ namespace dd {
             rest = pdd(e->m_rest, this);
             return;
         }
-        unsigned const gc_generation = m_gc_generation;
+
         if (level(p.root) > level_v) {
             pdd lc1 = zero(), rest1 = zero();
             pdd vv = mk_var(p.var());

src/math/polysat/solver.cpp

@@ -84,7 +84,9 @@ namespace polysat {
     }
 
     lbool solver::unit_propagate() {
-        flet<uint64_t> _max_d(m_max_decisions, m_stats.m_num_decisions + 1);
+        return l_undef;
+        // disabled to allow debugging unsoundness for watched literals
+        flet<uint64_t> _max_d(m_max_conflicts, m_stats.m_num_conflicts + 2);
         return check_sat();
     }
 
@@ -148,8 +150,21 @@ namespace polysat {
         add_eq(b * q + r - a);
         add_noovfl(b, q);
         add_ule(r, b*q+r);
-        add_clause(eq(b), ult(r, b), false);
+        auto c1 = eq(b);
-        add_clause(diseq(b), eq(q + 1), false);
+        auto c2 = ult(r, b);
+        auto c3 = diseq(b);
+        auto c4 = eq(q + 1);
+        add_clause(c1, c2, false);
+        add_clause(c3, c4, false);
+
+        // BUG:
+        // need to watch these constraints.
+        // ... but activation discipline seems to 
+        // work only for lemmas. Literals are watched only when assigned true.
+        // The literals are de-activated
+        // after propagation
+        // Should these clauses then be added as lemmas that force a branch?
+
         return std::tuple<pdd, pdd>(q, r);
     }
 
@@ -171,6 +186,7 @@ namespace polysat {
 
 
     void solver::assign_eh(signed_constraint c, dependency dep) {
+        backjump(base_level());
         SASSERT(at_base_level());
         SASSERT(c);
         if (is_conflict())

src/sat/smt/bv_polysat.cpp

@@ -321,4 +321,13 @@ namespace bv {
         VERIFY(m_polysat.try_eval(p, val));
         values[n->get_root_id()] = bv.mk_numeral(val, get_bv_size(n));        
     }   
+
+    void solver::polysat_display(std::ostream& out) const {
+        if (!use_polysat())
+            return;
+        m_polysat.display(out);
+        for (unsigned v = 0; v < get_num_vars(); ++v) 
+            if (m_var2pdd_valid.get(v, false))
+                out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";        
+    }
 }

src/sat/smt/bv_solver.cpp

@@ -622,8 +622,7 @@ namespace bv {
         out << "bv-solver:\n";
         for (unsigned v = 0; v < num_vars; v++)
             out << pp(v);
-        if (use_polysat())
+        polysat_display(out);
-            m_polysat.display(out);
         return out;
     }
 

src/sat/smt/bv_solver.h

@@ -280,9 +280,9 @@ namespace bv {
         void polysat_neg(app* a);
         void polysat_num(app* a);
         void polysat_mkbv(app* a);
-        void solver::polysat_umul_noovfl(app* e);
+        void polysat_umul_noovfl(app* e);
-        void solver::polysat_div_rem_i(app* e, bool is_div);
+        void polysat_div_rem_i(app* e, bool is_div);
-        void solver::polysat_div_rem(app* e, bool is_div);
+        void polysat_div_rem(app* e, bool is_div);
         void polysat_bit2bool(atom* a, expr* e, unsigned idx);
         bool polysat_sort_cnstr(euf::enode* n);
         void polysat_assign(atom* a);
@@ -292,6 +292,7 @@ namespace bv {
         bool polysat_diseq_eh(euf::th_eq const& ne);
         void polysat_add_value(euf::enode* n, model& mdl, expr_ref_vector& values);
         lbool polysat_final();
+        void polysat_display(std::ostream& out) const;
         bool use_polysat() const { return get_config().m_bv_polysat; }
         vector<polysat::pdd> m_var2pdd;
         bool_vector          m_var2pdd_valid;