bugfixes

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

src/sat/smt/polysat/core.cpp

@@ -186,10 +186,27 @@ namespace polysat {
             propagate_assignment(m_var, m_value, d);
             return sat::check_result::CR_CONTINUE;
         }
-        case find_t::multiple:
+        case find_t::multiple: {
             TRACE("bv", tout << "check-multiple v" << m_var << " := " << m_value << "\n");
-            s.add_eq_literal(m_var, m_value);
+            do {
+                dependency d = null_dependency;
+                lbool value = s.add_eq_literal(m_var, m_value, d);
+                switch (value) {
+                case l_true:
+                    propagate_assignment(m_var, m_value, d);
+                    break;
+                case l_false:                    
+                    m_value = mod(m_value + 1, rational::power_of_two(size(m_var)));
+                    continue;
+                default:
+                    // let core assign equality.
+                    m_var_queue.unassign_var_eh(m_var);
+                    break;
+                }
+            } 
+            while (false);
             return sat::check_result::CR_CONTINUE;
+        }
         case find_t::resource_out:
             TRACE("bv", tout << "check-resource out v" << m_var << "\n");
             m_var_queue.unassign_var_eh(m_var);
@@ -206,8 +223,7 @@ namespace polysat {
             auto [sc, d, value] = m_constraint_index[idx.id];
             SASSERT(value != l_undef);
             lbool eval_value = eval(sc);
-            sc.display(verbose_stream()) << " eval: " << eval_value << "\n";
+            CTRACE("bv", eval_value == l_undef, sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n"; display(tout););
-            CTRACE("bv", eval_value == l_undef, sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n");
             SASSERT(eval_value != l_undef);
             if (eval_value == value)
                 continue;

src/sat/smt/polysat/inequality.h

@@ -36,7 +36,10 @@ namespace polysat {
         }
 
         // p := coeff*x*y where coeff_x = coeff*x, x a variable
-        bool is_coeffxY(pdd const& coeff_x, pdd const& p, pdd& y) const { throw default_exception("nyi"); }
+        bool is_coeffxY(pdd const& x, pdd const& p, pdd& y) const { 
+            pdd xy = x.manager().zero();
+            return x.is_unary() && p.try_div(x.hi().val(), xy) && xy.factor(x.var(), 1, y);
+        }
         
     public:
         static inequality from_ule(core& c, constraint_id id);

src/sat/smt/polysat/types.h

@@ -134,7 +134,7 @@ namespace polysat {
     class solver_interface {
     public:
         virtual ~solver_interface() {}
-        virtual void add_eq_literal(pvar v, rational const& val) = 0;
+        virtual lbool add_eq_literal(pvar v, rational const& val, dependency& d) = 0;
         virtual bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool redundant) = 0;
         virtual void set_conflict(dependency_vector const& core) = 0;
         virtual dependency propagate(signed_constraint sc, dependency_vector const& deps) = 0;

src/sat/smt/polysat_internalize.cpp

@@ -724,5 +724,31 @@ namespace polysat {
         SASSERT(m.is_eq(n->get_expr()));
     }
 
+    struct solver::undo_add_eq : public trail {
+        solver& s;
+        unsigned index;
+    public:
+        undo_add_eq(solver& s, unsigned i) : s(s), index(i) {}
+        void undo() override {
+            s.m_eq2constraint.remove(index);
+            s.m_eqs.pop_back();
+        }
+    };
+
+    constraint_id solver::eq_constraint(pdd p, pdd q, dependency d) {
+        pdd r = p - q;
+        constraint_id idx;
+        if (m_eq2constraint.find(r.index(), idx))
+            return idx;
+        auto sc = m_core.eq(p, q);
+        TRACE("bv", tout << "new eq " << sc << "\n");
+        idx = m_core.register_constraint(sc, d);
+
+        m_eq2constraint.insert(r.index(), idx);
+        m_eqs.push_back(r);
+        ctx.push(undo_add_eq(*this, r.index()));
+        return idx;
+    }
+
 
 }

src/sat/smt/polysat_solver.cpp

@@ -57,6 +57,7 @@ namespace polysat {
     }
 
     sat::check_result solver::check() {
+        TRACE("euf", s().display(tout));
         switch (m_core.check()) {
         case sat::check_result::CR_DONE:
             return sat::check_result::CR_DONE;
@@ -162,12 +163,21 @@ namespace polysat {
     // Create an equality literal that represents the value assignment
     // Prefer case split to true.
     // The equality gets added in a callback using asserted().
-    void solver::add_eq_literal(pvar pvar, rational const& val) {
+    lbool solver::add_eq_literal(pvar pvar, rational const& val, dependency& d) {
         auto v = m_pddvar2var[pvar];
         auto n = var2enode(v);
         auto eq = eq_internalize(n->get_expr(), bv.mk_numeral(val, get_bv_size(v)));
+        euf::enode* eqn = ctx.bool_var2enode(eq.var());
+        if (eqn->get_th_var(get_id()) == euf::null_theory_var)
+            mk_var(eqn);
+        pdd p = m_core.var(pvar);
+        pdd q = m_core.value(val, m_core.size(pvar));
+        auto sc = m_core.eq(p, q);
+        mk_atom(eq.var(), sc);
         s().set_phase(eq);
         ctx.mark_relevant(eq);
+        d = dependency(eq.var());
+        return s().value(eq);
     }
 
     void solver::new_eq_eh(euf::th_eq const& eq) {
@@ -175,15 +185,16 @@ namespace polysat {
         euf::enode* n = var2enode(v1);
         if (!bv.is_bv(n->get_expr()))
             return;
-        pdd p = var2pdd(v1);
+  
-        pdd q = var2pdd(v2);
-        auto sc = m_core.eq(p, q);        
         m_var_eqs.setx(m_var_eqs_head, {v1, v2}, {v1, v2});
         ctx.push(value_trail<unsigned>(m_var_eqs_head));    
-        auto d = dependency(v1, v2);
-        constraint_id id = m_core.register_constraint(sc, d);
-        m_core.assign_eh(id, false, s().scope_lvl()); 
         m_var_eqs_head++;
+        pdd p = var2pdd(v1);
+        pdd q = var2pdd(v2);
+        auto d = dependency(v1, v2);
+        constraint_id id = eq_constraint(p, q, d);
+        m_core.assign_eh(id, false, s().scope_lvl()); 
+
     }
 
     void solver::new_diseq_eh(euf::th_eq const& ne) {
@@ -193,10 +204,9 @@ namespace polysat {
             return;
         pdd p = var2pdd(v1);
         pdd q = var2pdd(v2);
-        auto sc = m_core.eq(p, q);
         sat::literal eq = expr2literal(ne.eq());
         auto d = dependency(eq.var());
-        auto id = m_core.register_constraint(sc, d);
+        auto id = eq_constraint(p, q, d);
         TRACE("bv", tout << eq << " := " << s().value(eq) << " @" << s().scope_lvl() << "\n");
         m_core.assign_eh(id, false, s().lvl(eq));
     }
@@ -342,9 +352,14 @@ namespace polysat {
         expr_ref result(m);
         switch (sc.op()) {
         case ckind_t::ule_t: {
-            auto l = pdd2expr(sc.to_ule().lhs());
+            auto p = sc.to_ule().lhs();
-            auto h = pdd2expr(sc.to_ule().rhs());
+            auto q = sc.to_ule().rhs();
-            result = bv.mk_ule(l, h);
+            auto l = pdd2expr(p);
+            auto h = pdd2expr(q);
+            if (q.is_zero())
+                result = m.mk_eq(l, h);
+            else
+                result = bv.mk_ule(l, h);
             if (sc.sign())
                 result = m.mk_not(result);
             return result;           

src/sat/smt/polysat_solver.h

@@ -163,9 +163,13 @@ namespace polysat {
         void internalize_set(euf::theory_var v, pdd const& p);
         void quot_rem(expr* quot, expr* rem, expr* x, expr* y);
 
+        vector<pdd> m_eqs;
+        u_map<constraint_id> m_eq2constraint;
+        struct undo_add_eq;
+        constraint_id eq_constraint(pdd p, pdd q, dependency d);
 
         // callbacks from core
-        void add_eq_literal(pvar v, rational const& val) override;
+        lbool add_eq_literal(pvar v, rational const& val, dependency& d) override;
         void set_conflict(dependency_vector const& core) override;
         bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool redundant) override;
         dependency propagate(signed_constraint sc, dependency_vector const& deps) override;
@@ -209,7 +213,7 @@ namespace polysat {
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
         void collect_statistics(statistics& st) const override;
         euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx, get_id()); }
-        extension* copy(sat::solver* s) override { throw default_exception("nyi"); }
+        extension* copy(sat::solver* s) override { throw default_exception("polysat copy nyi"); }
         void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override {}
         void gc() override {}
         void pop_reinit() override {}