Fix unsoundness in viable fallback

(the src constraint of forbidden intervals is not necessarily univariate)

src/math/dd/dd_pdd.cpp

@@ -1208,6 +1208,11 @@ namespace dd {
         return true;
     }
 
+    /** Return true iff p contains no variables other than v. */
+    bool pdd_manager::is_univariate_in(PDD p, unsigned v) {
+        return (is_val(p) || var(p) == v) && is_univariate(p);
+    }
+
     /**
      * Push coefficients of univariate polynomial in order of ascending degree.
      * Example:     a*x^2 + b*x + c    ==>    [ c, b, a ]

src/math/dd/dd_pdd.h

@@ -364,6 +364,7 @@ namespace dd {
         bool is_monomial(PDD p);
 
         bool is_univariate(PDD p);
+        bool is_univariate_in(PDD p, unsigned v);
         void get_univariate_coefficients(PDD p, vector<rational>& coeff);
 
         // create an spoly r if leading monomials of a and b overlap
@@ -430,6 +431,7 @@ namespace dd {
         bool is_binary() const { return m.is_binary(root); }
         bool is_monomial() const { return m.is_monomial(root); }
         bool is_univariate() const { return m.is_univariate(root); }
+        bool is_univariate_in(unsigned v) const { return m.is_univariate_in(root, v); }
         void get_univariate_coefficients(vector<rational>& coeff) const { m.get_univariate_coefficients(root, coeff); }
         vector<rational> get_univariate_coefficients() const { vector<rational> coeff; m.get_univariate_coefficients(root, coeff); return coeff; }
         bool is_never_zero() const { return m.is_never_zero(root); }

src/math/polysat/constraint.h

@@ -114,9 +114,11 @@ namespace polysat {
         bool is_pwatched() const { return m_is_pwatched; }
         void set_pwatched(bool f) { m_is_pwatched = f; }
 
-        /// Assuming the constraint is univariate under the current assignment of 's',
+        /**
-        /// adds the constraint to the univariate solver 'us'.
+         * If the constraint is univariate in variable 'v' under the current assignment of 's',
-        virtual void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const = 0;
+         * add the constraint to the univariate solver 'us'.
+         */
+        virtual void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const = 0;
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
@@ -161,7 +163,7 @@ namespace polysat {
         void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
         clause_ref produce_lemma(solver& s, assignment const& a) { return get()->produce_lemma(s, a, is_positive()); }
 
-        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep) const { get()->add_to_univariate_solver(s, us, dep, is_positive()); }
+        void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep) const { get()->add_to_univariate_solver(v, s, us, dep, is_positive()); }
 
         unsigned_vector const& vars() const { return m_constraint->vars(); }
         unsigned var(unsigned idx) const { return m_constraint->var(idx); }

src/math/polysat/op_constraint.cpp

@@ -448,19 +448,25 @@ namespace polysat {
         return l_undef;
     }
 
-    void op_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
+    void op_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
-        auto p_coeff = s.subst(p()).get_univariate_coefficients();
+        pdd pv = s.subst(p());
-        auto q_coeff = s.subst(q()).get_univariate_coefficients();
+        if (!pv.is_univariate_in(v))
-        auto r_coeff = s.subst(r()).get_univariate_coefficients();
+            return;
+        pdd qv = s.subst(q());
+        if (!qv.is_univariate_in(v))
+            return;
+        pdd rv = s.subst(r());
+        if (!rv.is_univariate_in(v))
+            return;
         switch (m_op) {
         case code::lshr_op:
-            us.add_lshr(p_coeff, q_coeff, r_coeff, !is_positive, dep);
+            us.add_lshr(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep);
             break;
         case code::shl_op:
-            us.add_shl(p_coeff, q_coeff, r_coeff, !is_positive, dep);
+            us.add_shl(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep);
             break;
         case code::and_op:
-            us.add_and(p_coeff, q_coeff, r_coeff, !is_positive, dep);
+            us.add_and(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep);
             break;
         default:
             NOT_IMPLEMENTED_YET();

src/math/polysat/op_constraint.h

@@ -69,7 +69,7 @@ namespace polysat {
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return false; }
 
-        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
+        void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
     struct op_constraint_args {

src/math/polysat/smul_fl_constraint.cpp

@@ -119,13 +119,17 @@ namespace polysat {
             && q() == other.to_smul_fl().q();
     }
 
-    void smul_fl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
+    void smul_fl_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
-        auto p_coeff = s.subst(p()).get_univariate_coefficients();
+        auto p1 = s.subst(p());
-        auto q_coeff = s.subst(q()).get_univariate_coefficients();
+        if (!p1.is_univariate_in(v))
+            return;
+        auto q1 = s.subst(q());
+        if (!q1.is_univariate_in(v))
+            return;
         if (is_overflow())
-            us.add_smul_ovfl(p_coeff, q_coeff, !is_positive, dep);
+            us.add_smul_ovfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, dep);
         else
-            us.add_smul_udfl(p_coeff, q_coeff, !is_positive, dep);
+            us.add_smul_udfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, dep);
     }
 
 }

src/math/polysat/smul_fl_constraint.h

@@ -42,7 +42,7 @@ namespace polysat {
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return false; }
 
-        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
+        void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
 }

src/math/polysat/ule_constraint.cpp

@@ -245,9 +245,16 @@ namespace polysat {
         return other.is_ule() && lhs() == other.to_ule().lhs() && rhs() == other.to_ule().rhs();
     }
 
-    void ule_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
+    void ule_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
-        auto p_coeff = s.subst(lhs()).get_univariate_coefficients();
+        pdd p = s.subst(lhs());
-        auto q_coeff = s.subst(rhs()).get_univariate_coefficients();
+        pdd q = s.subst(rhs());
-        us.add_ule(p_coeff, q_coeff, !is_positive, dep);
+        bool p_ok = p.is_univariate_in(v);
+        bool q_ok = q.is_univariate_in(v);
+        if (!is_positive && !q_ok)  // add p > 0
+            us.add_ugt(p.get_univariate_coefficients(), rational::zero(), false, dep);
+        if (!is_positive && !p_ok)  // add -1 > q  <==>  q+1 > 0
+            us.add_ugt((q + 1).get_univariate_coefficients(), rational::zero(), false, dep);
+        if (p_ok && q_ok)
+            us.add_ule(p.get_univariate_coefficients(), q.get_univariate_coefficients(), !is_positive, dep);
     }
 }

src/math/polysat/ule_constraint.h

@@ -44,7 +44,7 @@ namespace polysat {
         unsigned hash() const override;
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return m_rhs.is_zero(); }
-        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
+        void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
     struct ule_pp {

src/math/polysat/umul_ovfl_constraint.cpp

@@ -25,8 +25,7 @@ namespace polysat {
 
     }
     void umul_ovfl_constraint::simplify() {
-        if (m_p.is_zero() || m_q.is_zero() ||
+        if (m_p.is_zero() || m_q.is_zero() || m_p.is_one() || m_q.is_one()) {
-            m_p.is_one() || m_q.is_one()) {
             m_q = 0;
             m_p = 0;
             return;
@@ -158,9 +157,13 @@ namespace polysat {
         return other.is_umul_ovfl() && p() == other.to_umul_ovfl().p() && q() == other.to_umul_ovfl().q();
     }
 
-    void umul_ovfl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
+    void umul_ovfl_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
-        auto p_coeff = s.subst(p()).get_univariate_coefficients();
+        pdd p1 = s.subst(p());
-        auto q_coeff = s.subst(q()).get_univariate_coefficients();
+        if (!p1.is_univariate_in(v))
-        us.add_umul_ovfl(p_coeff, q_coeff, !is_positive, dep);
+            return;
+        pdd q1 = s.subst(q());
+        if (!q1.is_univariate_in(v))
+            return;
+        us.add_umul_ovfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, dep);
     }
 }

src/math/polysat/umul_ovfl_constraint.h

@@ -46,7 +46,7 @@ namespace polysat {
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return false; }
 
-        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
+        void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
 }

src/math/polysat/univariate/univariate_solver.cpp

@@ -103,6 +103,10 @@ namespace polysat {
             return true;
         }
 
+        bool is_zero(rational const& p) const {
+            return p.is_zero();
+        }
+
 #if 0
         // [d,c,b,a]  -->  ((a*x + b)*x + c)*x + d
         expr* mk_poly(univariate const& p) const {
@@ -154,6 +158,10 @@ namespace polysat {
             }
             return e;
         }
+
+        expr_ref mk_poly(rational const& p) {
+            return {mk_numeral(p), m};
+        }
 #endif
 
         void add(expr* e, bool sign, dep_t dep) {
@@ -171,13 +179,18 @@ namespace polysat {
             }
         }
 
-        void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override {
+        template <typename lhs_t, typename rhs_t>
+        void add_ule_impl(lhs_t const& lhs, rhs_t const& rhs, bool sign, dep_t dep) {
             if (is_zero(rhs)) 
                 add(m.mk_eq(mk_poly(lhs), mk_poly(rhs)), sign, dep);
             else 
                 add(bv->mk_ule(mk_poly(lhs), mk_poly(rhs)), sign, dep);
         }
 
+        void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override { add_ule_impl(lhs, rhs, sign, dep); }
+        void add_ule(univariate const& lhs, rational   const& rhs, bool sign, dep_t dep) override { add_ule_impl(lhs, rhs, sign, dep); }
+        void add_ule(rational   const& lhs, univariate const& rhs, bool sign, dep_t dep) override { add_ule_impl(lhs, rhs, sign, dep); }
+
         void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override {
             add(bv->mk_bvumul_no_ovfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep);
         }
@@ -220,13 +233,13 @@ namespace polysat {
 
         void add_ule_const(rational const& val, bool sign, dep_t dep) override {
             if (val == 0)
-                add(m.mk_eq(x, mk_numeral(val)), sign, dep);
+                add(m.mk_eq(x, mk_poly(val)), sign, dep);
             else 
-                add(bv->mk_ule(x, mk_numeral(val)), sign, dep);
+                add(bv->mk_ule(x, mk_poly(val)), sign, dep);
         }
 
         void add_uge_const(rational const& val, bool sign, dep_t dep) override {
-            add(bv->mk_ule(mk_numeral(val), x), sign, dep);
+            add(bv->mk_ule(mk_poly(val), x), sign, dep);
         }
 
         void add_bit(unsigned idx, bool sign, dep_t dep) override {

src/math/polysat/univariate/univariate_solver.h

@@ -80,7 +80,23 @@ namespace polysat {
          */
         virtual bool find_two(rational& out1, rational& out2) = 0;
 
+        /** lhs <= rhs */
         virtual void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
+        virtual void add_ule(univariate const& lhs, rational   const& rhs, bool sign, dep_t dep) = 0;
+        virtual void add_ule(rational   const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
+        /** lhs >= rhs */
+        void add_uge(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); }
+        void add_uge(univariate const& lhs, rational   const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); }
+        void add_uge(rational   const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); }
+        /** lhs < rhs */
+        void add_ult(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); }
+        void add_ult(univariate const& lhs, rational   const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); }
+        void add_ult(rational   const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); }
+        /** lhs > rhs */
+        void add_ugt(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); }
+        void add_ugt(univariate const& lhs, rational   const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); }
+        void add_ugt(rational   const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); }
+
         virtual void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
         virtual void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
         virtual void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;

src/math/polysat/viable.cpp

@@ -344,9 +344,9 @@ namespace polysat {
             }
         };
         do {
-            LOG("refine-equal-lin for src: " << lit_pp(s, e->src));
             rational coeff_val = mod(e->coeff * val, mod_value);
             if (e->interval.currently_contains(coeff_val)) {
+                LOG("refine-equal-lin for src: " << lit_pp(s, e->src));
 
                 if (e->interval.lo_val().is_one() && e->interval.hi_val().is_zero() && e->coeff.is_odd()) {
                     rational lo(1);
@@ -730,6 +730,7 @@ namespace polysat {
 
         // First step: only query the looping constraints and see if they alone are already UNSAT.
         // The constraints which caused the refinement loop will be reached from m_units.
+        LOG_H3("Checking looping univariate constraints for v" << v << "...");
         entry const* first = m_units[v];
         entry const* e = first;
         do {
@@ -740,7 +741,8 @@ namespace polysat {
             sat::literal const lit = c.blit();
             if (!added.contains(lit)) {
                 added.insert(lit);
-                c.add_to_univariate_solver(s, *us, lit.to_uint());
+                LOG("Adding " << lit_pp(s, lit));
+                c.add_to_univariate_solver(v, s, *us, lit.to_uint());
             }
             e = e->next();
         }
@@ -759,13 +761,15 @@ namespace polysat {
         }
 
         // Second step: looping constraints aren't UNSAT, so add the remaining relevant constraints
+        LOG_H3("Checking all univariate constraints for v" << v << "...");
         auto const& cs = s.m_viable_fallback.m_constraints[v];
         for (unsigned i = cs.size(); i-- > 0; ) {
             sat::literal const lit = cs[i].blit();
             if (added.contains(lit))
                 continue;
+            LOG("Adding " << lit_pp(s, lit));
             added.insert(lit);
-            cs[i].add_to_univariate_solver(s, *us, lit.to_uint());
+            cs[i].add_to_univariate_solver(v, s, *us, lit.to_uint());
         }
 
         switch (us->check()) {
@@ -1060,7 +1064,7 @@ namespace polysat {
         for (unsigned i = cs.size(); i-- > 0; ) {
             signed_constraint const c = cs[i];
             LOG("Univariate constraint: " << c);
-            c.add_to_univariate_solver(s, *us, c.blit().to_uint());
+            c.add_to_univariate_solver(v, s, *us, c.blit().to_uint());
         }
 
         switch (us->check()) {