add back minimize vars

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

src/math/polysat/conflict.cpp

@@ -229,8 +229,10 @@ namespace polysat {
         signed_constraint c = s.lit2cnstr(lit);
         unset_mark(c);
         for (pvar v : c->vars())
-            if (s.is_assigned(v) && s.get_level(v) <= lvl)
+            if (s.is_assigned(v) && s.get_level(v) <= lvl) {
                 m_vars.insert(v);  // TODO: check this
+                inc_pref(v);
+            }
     }
 
     /** 
@@ -283,10 +285,6 @@ namespace polysat {
         if (!c.is_currently_false(s))
             return;
         
-        return;
-#if 0
-        
-        TODO - fix for new subst
         assignment_t a;
         for (auto v : m_vars)
             a.push_back(std::make_pair(v, s.get_value(v)));
@@ -295,7 +293,7 @@ namespace polysat {
             std::pair<pvar, rational> last = a.back();
             a[i] = last;
             a.pop_back();
-            if (c.is_currently_false(a)) 
+            if (c.is_currently_false(s, a)) 
                 --i;
             else {
                 a.push_back(last);
@@ -308,7 +306,6 @@ namespace polysat {
         for (auto const& [v, val] : a)
             m_vars.insert(v);
         LOG("reduced " << m_vars);
-#endif
     }
 
 

src/math/polysat/constraint.h

@@ -178,6 +178,8 @@ namespace polysat {
         virtual bool is_always_false(bool is_positive) const = 0;
         virtual bool is_currently_false(solver& s, bool is_positive) const = 0;
         virtual bool is_currently_true(solver& s, bool is_positive) const = 0;
+        virtual bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const = 0;
+        virtual bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const = 0;
         virtual void narrow(solver& s, bool is_positive) = 0;
         virtual inequality as_inequality(bool is_positive) const = 0;
 
@@ -245,6 +247,7 @@ namespace polysat {
         bool is_always_true() const { return get()->is_always_false(is_negative()); }        
         bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); }
         bool is_currently_true(solver& s) const { return get()->is_currently_true(s, is_positive()); }
+        bool is_currently_false(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_positive()); }
         lbool bvalue(solver& s) const;
         unsigned level(solver& s) const { return get()->level(s); }
         void narrow(solver& s) { get()->narrow(s, is_positive()); }

src/math/polysat/mul_ovfl_constraint.h

@@ -40,6 +40,8 @@ namespace polysat {
         void narrow(solver& s, bool is_positive) override;
         bool is_currently_false(solver & s, bool is_positive) const;
         bool is_currently_true(solver& s, bool is_positive) const;
+        bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
+        bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
 
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;

src/math/polysat/op_constraint.h

@@ -58,6 +58,8 @@ namespace polysat {
         bool is_always_false(bool is_positive) const override;
         bool is_currently_false(solver& s, bool is_positive) const override;
         bool is_currently_true(solver& s, bool is_positive) const override;
+        bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
+        bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
         void narrow(solver& s, bool is_positive) override;
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;

src/math/polysat/solver.cpp

@@ -1040,6 +1040,14 @@ namespace polysat {
         return p.subst_val(s);
     }
 
+    pdd solver::subst(assignment_t const& sub, pdd const& p) const {
+        unsigned sz = p.manager().power_of_2();
+        pdd s = p.manager().mk_val(1);
+        for (auto const [var, val] : sub) 
+            if (size(var) == sz)
+                s = p.manager().subst_add(s, var, val);
+        return p.subst_val(s);
+    }
 
     /** Check that boolean assignment and constraint evaluation are consistent */
     bool solver::assignment_invariant() {

src/math/polysat/solver.h

@@ -116,6 +116,7 @@ namespace polysat {
         search_state             m_search;
         assignment_t const& assignment() const { return m_search.assignment(); }
         pdd subst(pdd const& p) const; 
+        pdd subst(assignment_t const& sub, pdd const& p) const;
 
         unsigned                 m_qhead = 0; // next item to propagate (index into m_search)
         unsigned                 m_level = 0;

src/math/polysat/ule_constraint.cpp

@@ -196,6 +196,16 @@ namespace polysat {
         return is_always_false(is_positive, p, q);
     }
 
+    bool ule_constraint::is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const { 
+        auto p = s.subst(sub, lhs());
+        auto q = s.subst(sub, rhs());
+        return is_always_false(is_positive, p, q);
+    }
+
+    bool ule_constraint::is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const { 
+        return false; 
+    }
+
     bool ule_constraint::is_currently_true(solver& s, bool is_positive) const {
         auto p = s.subst(lhs());
         auto q = s.subst(rhs());

src/math/polysat/ule_constraint.h

@@ -38,6 +38,8 @@ namespace polysat {
         bool is_always_false(bool is_positive) const override;
         bool is_currently_false(solver& s, bool is_positive) const override;
         bool is_currently_true(solver& s, bool is_positive) const override;
+        bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override;
+        bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const override;
         void narrow(solver& s, bool is_positive) override;
         inequality as_inequality(bool is_positive) const override;
         unsigned hash() const override;