comments

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

src/math/polysat/constraint.cpp

@@ -112,8 +112,35 @@ namespace polysat {
     }
 
     void constraint_manager::gc() {
-        // collect used literals from lemmas and stack
+        gc_clauses();
-        // walk constraints to remove unused.
+        gc_constraints();
+    }
+
+    void constraint_manager::gc_clauses() {
+        // place to gc redundant clauses
+    }
+
+    void constraint_manager::gc_constraints() {
+        uint_set used_vars;
+        for (auto const& cls : m_clauses)
+            for (auto const& cl : cls)
+                for (auto lit : *cl)
+                    used_vars.insert(lit.var());
+#if 0
+        // anything on the search stack is justified by a clause?
+        for (auto const& a : s().m_search)
+            if (a.is_boolean())
+                used_vars.insert(a.lit().var());
+#endif
+        for (unsigned i = 0; i < m_constraints.size(); ++i) {
+            constraint* c = m_constraints[i];
+            if (c->has_bvar() && used_vars.contains(c->bvar()))
+                continue;
+            m_constraints.swap(i, m_constraints.size() - 1);
+            m_constraints.pop_back();
+            --i;
+        }
+            
     }
 
     bool constraint_manager::should_gc() {

src/math/polysat/constraint.h

@@ -58,6 +58,9 @@ namespace polysat {
 
         constraint* dedup(constraint* c);
 
+        void gc_constraints();
+        void gc_clauses();
+
     public:
         constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {}
         ~constraint_manager();
@@ -71,7 +74,7 @@ namespace polysat {
         /// Register a unit clause with an external dependency.
         void register_external(constraint* c);
 
-        /// Release constraints at the given level and above.
+        /// Release clauses at the given level and above.
         void release_level(unsigned lvl);
 
         /// Garbage-collect temporary constraints (i.e., those that do not have a boolean variable).
@@ -121,13 +124,9 @@ namespace polysat {
          *  If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
          *  Convention: the plain constraint corresponds the positive sat::literal.
          */
-        // NB code review: the convention would make sense. Unfortunately, elsewhere in z3 we use "true" for negative literals
-        // and "false" for positive literals. It is called the "sign" bit.
-        // TODO: replace parameter 'is_positive' everywhere by 'sign'? (also in signed_constraint)
         sat::bool_var       m_bvar = sat::null_bool_var;
 
-        constraint(constraint_manager& m, ckind_t k):
+        constraint(constraint_manager& m, ckind_t k): m_kind(k) {}
-            /*m_manager(&m),*/ m_kind(k) {}
 
     protected:
         std::ostream& display_extra(std::ostream& out, lbool status) const;
@@ -146,9 +145,9 @@ namespace polysat {
 
         bool propagate(solver& s, bool is_positive, pvar v);
         virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v);
-        virtual bool is_always_false(bool is_positive) = 0;
+        virtual bool is_always_false(bool is_positive) const = 0;
-        virtual bool is_currently_false(solver& s, bool is_positive) = 0;
+        virtual bool is_currently_false(solver& s, bool is_positive) const = 0;
-        virtual bool is_currently_true(solver& s, bool is_positive) = 0;
+        virtual bool is_currently_true(solver& s, bool is_positive) const = 0;
         virtual void narrow(solver& s, bool is_positive) = 0;
         virtual inequality as_inequality(bool is_positive) const = 0;
 
@@ -196,10 +195,10 @@ namespace polysat {
 
         bool propagate(solver& s, pvar v) { return get()->propagate(s, is_positive(), v); }
         void propagate_core(solver& s, pvar v, pvar other_v) { get()->propagate_core(s, is_positive(), v, other_v); }
-        bool is_always_false() { return get()->is_always_false(is_positive()); }
+        bool is_always_false() const { return get()->is_always_false(is_positive()); }
-        bool is_always_true() { return get()->is_always_false(is_negative()); }
+        bool is_always_true() const { return get()->is_always_false(is_negative()); }
-        bool is_currently_false(solver& s) { return get()->is_currently_false(s, is_positive()); }
+        bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); }
-        bool is_currently_true(solver& s) { return get()->is_currently_true(s, is_positive()); }
+        bool is_currently_true(solver& s) const { return get()->is_currently_true(s, is_positive()); }
         void narrow(solver& s) { get()->narrow(s, is_positive()); }
         inequality as_inequality() const { return get()->as_inequality(is_positive()); }
 

src/math/polysat/eq_constraint.cpp

@@ -64,14 +64,14 @@ namespace polysat {
         // TODO: what other constraints can be extracted cheaply?
     }
 
-    bool eq_constraint::is_always_false(bool is_positive) {
+    bool eq_constraint::is_always_false(bool is_positive) const {
         if (is_positive)
             return p().is_never_zero();
         else
             return p().is_zero();
     }
 
-    bool eq_constraint::is_currently_false(solver& s, bool is_positive) {
+    bool eq_constraint::is_currently_false(solver& s, bool is_positive) const {
         pdd r = p().subst_val(s.assignment());
         if (is_positive)
             return r.is_never_zero();
@@ -79,7 +79,7 @@ namespace polysat {
             return r.is_zero();
     }
 
-    bool eq_constraint::is_currently_true(solver& s, bool is_positive) {
+    bool eq_constraint::is_currently_true(solver& s, bool is_positive) const {
         pdd r = p().subst_val(s.assignment());
         if (is_positive)
             return r.is_zero();

src/math/polysat/eq_constraint.h

@@ -31,9 +31,9 @@ namespace polysat {
         ~eq_constraint() override {}
         pdd const & p() const { return m_poly; }
         std::ostream& display(std::ostream& out, lbool status) const override;
-        bool is_always_false(bool is_positive) override;
+        bool is_always_false(bool is_positive) const override;
-        bool is_currently_false(solver& s, bool is_positive) override;
+        bool is_currently_false(solver& s, bool is_positive) const override;
-        bool is_currently_true(solver& s, bool is_positive) override;
+        bool is_currently_true(solver& s, 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;

src/math/polysat/saturation.cpp

@@ -12,21 +12,16 @@ Author:
 
 
 TODO: preserve falsification
-- each rule selects a certain premise that is problematic, 
+- each rule selects a certain premises that are problematic.
-  We assume that problematic premises are false in the current assignment
+  If the problematic premise is false under the current assignment, the newly inferred
-  The derived consequence should also be false in the current assignment to be effective, but simpler so that we can resolve.
+  literal should also be false in the assignment in order to preserve conflicts.
 
-TODO:
-- remove level information from created constraints.
 
 TODO: when we check that 'x' is "unary":
 - in principle, 'x' could be any polynomial. However, we need to divide the lhs by x, and we don't have general polynomial division yet.
   so for now we just allow the form 'value*variable'.
    (extension to arbitrary monomials for 'x' should be fairly easy too)
 
-TODO: 
-- remove the "problematic" literal from the core itself such that reference counts on variable assignments are decreased.
-
 --*/
 #include "math/polysat/saturation.h"
 #include "math/polysat/solver.h"
@@ -63,11 +58,11 @@ namespace polysat {
     * The lemmas outlines in the rules are valid and therefore c is implied.
     */
     bool inf_saturate::propagate(conflict_core& core, inequality const& crit, signed_constraint& c, clause_builder& reason) {        
-        if (c.is_currently_true(s()))
+        if (crit.as_signed_constraint().is_currently_false(s()) && c.is_currently_true(s()))
             return false;
         core.insert(c);
         reason.push(c);
-        // TODO core.erase(crit.as_signed_constraint());
+        core.remove(crit.as_signed_constraint());
         s().propagate_bool(c.blit(), reason.build().get());
         return true;
     }
@@ -265,7 +260,7 @@ namespace polysat {
 
         clause_builder reason(s());   
         if (!c.is_strict)
-            reason.push(cm().eq(x - x.manager().mk_val(rational(0))));
+            reason.push(cm().eq(x));
         reason.push(~c.as_signed_constraint());
         push_omega(reason, x, y);        
         return propagate(core, c, c.is_strict, y, z, reason);

src/math/polysat/ule_constraint.cpp

@@ -86,7 +86,7 @@ namespace polysat {
         // TODO: other cheap constraints possible?
     }
 
-    bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) {
+    bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const {
         // TODO: other conditions (e.g. when forbidden interval would be full)
         if (is_positive)
             return lhs.is_val() && rhs.is_val() && lhs.val() > rhs.val();
@@ -97,17 +97,17 @@ namespace polysat {
         }
     }
 
-    bool ule_constraint::is_always_false(bool is_positive) {
+    bool ule_constraint::is_always_false(bool is_positive) const {
         return is_always_false(is_positive, lhs(), rhs());
     }
 
-    bool ule_constraint::is_currently_false(solver& s, bool is_positive) {
+    bool ule_constraint::is_currently_false(solver& s, bool is_positive) const {
         auto p = lhs().subst_val(s.assignment());
         auto q = rhs().subst_val(s.assignment());
         return is_always_false(is_positive, p, q);
     }
 
-    bool ule_constraint::is_currently_true(solver& s, bool is_positive) {
+    bool ule_constraint::is_currently_true(solver& s, bool is_positive) const {
         auto p = lhs().subst_val(s.assignment());
         auto q = rhs().subst_val(s.assignment());
         if (is_positive) {

src/math/polysat/ule_constraint.h

@@ -36,10 +36,10 @@ namespace polysat {
         pdd const& lhs() const { return m_lhs; }
         pdd const& rhs() const { return m_rhs; }
         std::ostream& display(std::ostream& out, lbool status) const override;
-        bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs);
+        bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const;
-        bool is_always_false(bool is_positive) override;
+        bool is_always_false(bool is_positive) const override;
-        bool is_currently_false(solver& s, bool is_positive) override;
+        bool is_currently_false(solver& s, bool is_positive) const override;
-        bool is_currently_true(solver& s, bool is_positive) override;
+        bool is_currently_true(solver& s, 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;