From 3e99828c3c9af3479a4654252fe64feb51c8bf44 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 19 Aug 2022 17:06:28 +0200
Subject: [PATCH] start make_asserting for non-unit coeff

---
 src/math/polysat/solver.cpp                   | 49 ++++++++++++++++++-
 src/math/polysat/solver.h                     |  1 +
 .../polysat/univariate/univariate_solver.cpp  |  8 +++
 .../polysat/univariate/univariate_solver.h    | 10 ++++
 4 files changed, 66 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b1c34a21b..632242b71 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1253,12 +1253,57 @@ namespace polysat {
                 auto c_new = ule(intersection.hi() - intersection.lo(), z - intersection.lo());
                 out_lits.push_back(c_new.blit());
             }
-            return;
         } else {
             out_lits.shrink(out_lits_original_size);
-            // TODO: SAT-based approach
+            find_implied_constraint_sat(cz, z, z_val, out_lits);
         }
     }
+
+    void solver::find_implied_constraint_sat(signed_constraints const& cz, pvar z, rational z_val, sat::literal_vector& out_lits)
+    {
+        unsigned bit_width = size(z);
+        auto p_factory = mk_univariate_bitblast_factory();
+        auto p_us = (*p_factory)(bit_width);
+        auto& us = *p_us;
+
+        // Find max z1 such that z1 < z_val and all cz true under z := z1 (and current assignment)
+        rational z1 = z_val;
+
+        for (signed_constraint const& c : cz)
+            c.add_to_univariate_solver(*this, us, 0);
+        us.add_ult_const(z_val, false, 0);  // z1 < z_val
+
+        // First check if any such z1 exists
+        switch (us.check()) {
+        case l_false:
+            // No such z1 exists
+            z1 = m_pdd[z]->max_value();  // -1
+            break;
+        case l_true:
+            // z1 exists. Try to make it as small as possible by setting bits to 0
+
+            for (unsigned j = bit_width; j-- > 0; ) {
+                switch (us.check()) {
+                case l_true:
+                    // TODO
+                    break;
+                case l_false:
+                    // TODO
+                    break;
+                default:
+                    UNREACHABLE();  // TODO: see below
+                }
+            }
+
+            break;
+        default:
+            UNREACHABLE();  // TODO: should we link the child solver's resources to polysat's resource counter?
+        }
+
+        // Find min z2 such that z2 > z_val and all cz true under z := z2 (and current assignment)
+        // TODO
+    }
+
 }
 
 
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 05f939067..418f08080 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -236,6 +236,7 @@ namespace polysat {
 
         clause_ref make_asserting(clause& cl, pvar z, rational z_val);
         void find_implied_constraint(signed_constraints const& cz, pvar z, rational z_val, sat::literal_vector& out_lits);
+        void find_implied_constraint_sat(signed_constraints const& cz, pvar z, rational z_val, sat::literal_vector& out_lits);
 
     public:
 
diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index 7c0a6a36a..c5beb5ab2 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -136,6 +136,14 @@ namespace polysat {
             add(m.mk_eq(bv->mk_bv_not(mk_poly(in)), mk_poly(out)), sign, dep);
         }
 
+        void add_ule_const(rational const& val, bool sign, dep_t dep) override {
+            add(bv->mk_ule(x, mk_numeral(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);
+        }
+
         lbool check() override {
             return s->check_sat();
         }
diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h
index e88ebf60b..0a19081ed 100644
--- a/src/math/polysat/univariate/univariate_solver.h
+++ b/src/math/polysat/univariate/univariate_solver.h
@@ -56,6 +56,16 @@ namespace polysat {
         virtual void add_xor(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
         virtual void add_not(univariate const& in, univariate const& out, bool sign, dep_t dep) = 0;
 
+        /// Add x <= val or x > val, depending on sign
+        virtual void add_ule_const(rational const& val, bool sign, dep_t dep) = 0;
+        /// Add x >= val or x < val, depending on sign
+        virtual void add_uge_const(rational const& val, bool sign, dep_t dep) = 0;
+        void add_ugt_const(rational const& val, bool sign, dep_t dep) { add_ule_const(val, !sign, dep); }
+        void add_ult_const(rational const& val, bool sign, dep_t dep) { add_uge_const(val, !sign, dep); }
+
+        // TODO: assert bit; use bv->mk_bit2bool(x, idx)
+        // virtual void add_bit(unsigned idx, bool sign, dep_t dep);
+
         virtual std::ostream& display(std::ostream& out) const = 0;
     };