We only need one of is_true/is_false

src/math/polysat/constraint.h

@@ -177,9 +177,11 @@ 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;
+        bool is_always_true(bool is_positive) const { return is_always_false(!is_positive); }
+        bool is_currently_true(solver& s, bool is_positive) const { return is_currently_false(s, !is_positive); }
+        bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const { return is_currently_false(s, sub, !is_positive); }
+
         virtual void narrow(solver& s, bool is_positive, bool first) = 0;
         virtual inequality as_inequality(bool is_positive) const = 0;
 
@@ -246,8 +248,9 @@ namespace polysat {
         bool is_always_false() const { return get()->is_always_false(is_positive()); }
         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_true(solver& s) const { return get()->is_currently_false(s, is_negative()); }
         bool is_currently_false(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_positive()); }
+        bool is_currently_true(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_negative()); }
         lbool bvalue(solver& s) const;
         unsigned level(solver& s) const { return get()->level(s); }
         void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }

src/math/polysat/op_constraint.cpp

@@ -67,11 +67,7 @@ namespace polysat {
     }
 
     bool op_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
-        switch (eval(p, q, r)) {
+        return is_always_false(!is_positive, p, q, r);
-        case l_true: return is_positive;
-        case l_false: return !is_positive;
-        default: return false;
-        }
     }
 
     bool op_constraint::is_always_false(bool is_positive) const {
@@ -82,10 +78,6 @@ namespace polysat {
         return is_always_false(is_positive, s.subst(p()), s.subst(q()), s.subst(r()));        
     }
 
-    bool op_constraint::is_currently_true(solver& s, bool is_positive) const {
-        return is_always_true(is_positive, s.subst(p()), s.subst(q()), s.subst(r()));        
-    }
-
     std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
         switch (status) {
         case l_true: return display(out);

src/math/polysat/op_constraint.h

@@ -57,9 +57,7 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         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, bool first) override;
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;

src/math/polysat/smul_fl_constraint.h

@@ -37,9 +37,7 @@ namespace polysat {
         bool is_always_false(bool is_positive) const override { return false; }
         void narrow(solver& s, bool is_positive, bool first) override;
         bool is_currently_false(solver & s, bool is_positive) const override { return false; }
-        bool is_currently_true(solver& s, bool is_positive) const override { return false; }
         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/ule_constraint.cpp

@@ -224,14 +224,6 @@ namespace polysat {
         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 is_currently_false(s, sub, !is_positive);
-    }
-
-    bool ule_constraint::is_currently_true(solver& s, bool is_positive) const {
-        return is_currently_false(s, !is_positive);
-    }
-
     inequality ule_constraint::as_inequality(bool is_positive) const {
         if (is_positive)
             return inequality(lhs(), rhs(), false, this);

src/math/polysat/ule_constraint.h

@@ -38,9 +38,7 @@ namespace polysat {
         static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs);
         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, bool first) override;
         inequality as_inequality(bool is_positive) const override;
         unsigned hash() const override;

src/math/polysat/umul_ovfl_constraint.cpp

@@ -70,26 +70,17 @@ namespace polysat {
     }
 
     bool umul_ovfl_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q) const {
-        switch (eval(p, q)) {
+        return is_always_false(!is_positive, p, q);
-        case l_true: return is_positive;
-        case l_false: return !is_positive;
-        default: return false;
-        }
     }
 
     bool umul_ovfl_constraint::is_always_false(bool is_positive) const {
         return is_always_false(is_positive, m_p, m_q);
     }
 
-
     bool umul_ovfl_constraint::is_currently_false(solver& s, bool is_positive) const {
         return is_always_false(is_positive, s.subst(p()), s.subst(q()));
     }
 
-    bool umul_ovfl_constraint::is_currently_true(solver& s, bool is_positive) const {
-        return is_always_true(is_positive, s.subst(p()), s.subst(q()));
-    }
-
     void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) {    
         auto p1 = s.subst(p());
         auto q1 = s.subst(q());

src/math/polysat/umul_ovfl_constraint.h

@@ -40,9 +40,7 @@ namespace polysat {
         bool is_always_false(bool is_positive) const override;
         void narrow(solver& s, bool is_positive, bool first) 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; }
 
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;