univariate::find_max

src/math/polysat/univariate/univariate_solver.cpp

@@ -35,6 +35,7 @@ namespace polysat {
         unsigned bit_width;
         func_decl_ref x_decl;
         expr_ref x;
+        vector<rational> model_cache;
 
     public:
         univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) :
@@ -48,15 +49,30 @@ namespace polysat {
             s = mk_solver(m, p, false, true, true, symbol::null);
             x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width));
             x = m.mk_const(x_decl);
+            model_cache.push_back(rational(-1));
         }
 
         ~univariate_bitblast_solver() override = default;
 
+        void reset_cache() {
+            model_cache.back() = -1;
+        }
+
+        void push_cache() {
+            model_cache.push_back(model_cache.back());
+        }
+
+        void pop_cache() {
+            model_cache.pop_back();
+        }
+
         void push() override {
+            push_cache();
             s->push();
         }
 
         void pop(unsigned n) override {
+            pop_cache();
             s->pop(n);
         }
 
@@ -114,6 +130,7 @@ namespace polysat {
 #endif
 
         void add(expr* e, bool sign, dep_t dep) {
+            reset_cache();
             if (sign)
                 e = m.mk_not(e);
             expr* a = m.mk_const(m.mk_const_decl(symbol(dep), m.mk_bool_sort()));
@@ -194,15 +211,19 @@ namespace polysat {
         }
 
         rational model() override {
-            model_ref model;
+            rational& cached_model = model_cache.back();
-            s->get_model(model);
+            if (cached_model.is_neg()) {
-            SASSERT(model);
+                model_ref model;
-            app* val = to_app(model->get_const_interp(x_decl));
+                s->get_model(model);
-            SASSERT(val->get_decl_kind() == OP_BV_NUM);
+                SASSERT(model);
-            SASSERT(val->get_num_parameters() == 2);
+                app* val = to_app(model->get_const_interp(x_decl));
-            auto const& p = val->get_parameter(0);
+                SASSERT(val->get_decl_kind() == OP_BV_NUM);
-            SASSERT(p.is_rational());
+                SASSERT(val->get_num_parameters() == 2);
-            return p.get_rational();
+                auto const& p = val->get_parameter(0);
+                SASSERT(p.is_rational());
+                cached_model = p.get_rational();
+            }
+            return cached_model;
         }
 
         bool find_min(rational& val) override {
@@ -214,6 +235,7 @@ namespace polysat {
                     add_bit0(k, 0);
                     continue;
                 }
+                // try decreasing k-th bit
                 push();
                 add_bit0(k, 0);
                 lbool result = check();
@@ -233,6 +255,35 @@ namespace polysat {
             return true;
         }
 
+        bool find_max(rational& val) override {
+            val = model();
+            push();
+            // try increasing val by setting bits to 1, starting at the msb.
+            for (unsigned k = bit_width; k-- > 0; ) {
+                if (val.get_bit(k)) {
+                    add_bit1(k, 0);
+                    continue;
+                }
+                // try increasing k-th bit
+                push();
+                add_bit1(k, 0);
+                lbool result = check();
+                if (result == l_true) {
+                    SASSERT(model() > val);
+                    val = model();
+                }
+                pop(1);
+                if (result == l_true)
+                    add_bit1(k, 0);
+                else if (result == l_false)
+                    add_bit0(k, 0);
+                else
+                    return false;
+            }
+            pop(1);
+            return true;
+        }
+
         std::ostream& display(std::ostream& out) const override {
             return out << *s;
         }

src/math/polysat/univariate/univariate_solver.h

@@ -42,16 +42,32 @@ namespace polysat {
 
         virtual lbool check() = 0;
 
-        // Precondition: check() returned l_false
+        /**
+         * Precondition: check() returned l_false
+         */
         virtual dep_vector unsat_core() = 0;
 
-        // Precondition: check() returned l_true
+        /**
+         * Precondition: check() returned l_true
+         */
         virtual rational model() = 0;
 
-        // Precondition: check() returned l_true
+        /**
-        // Returns false on resource out.
+         * Find minimal model.
+         *
+         * Precondition: check() returned l_true
+         * Returns: true on success, false on resource out.
+         */
         virtual bool find_min(rational& out_min) = 0;
 
+        /**
+         * Find maximal model.
+         *
+         * Precondition: check() returned l_true
+         * Returns: true on success, false on resource out.
+         */
+        virtual bool find_max(rational& out_max) = 0;
+
         virtual void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
         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;

src/test/viable.cpp

@@ -183,7 +183,7 @@ namespace polysat {
         std::cout << "core: " << solver->unsat_core() << "\n";
     }
 
-    static void test_univariate_min() {
+    static void test_univariate_minmax() {
         std::cout << "\ntest_univariate_min\n";
         unsigned const bw = 32;
         auto factory = mk_univariate_bitblast_factory();
@@ -192,6 +192,7 @@ namespace polysat {
         vector<rational> lhs;
         vector<rational> rhs;
         rational min;
+        rational max;
 
         solver->push();
 
@@ -204,10 +205,18 @@ namespace polysat {
         solver->add_ule(lhs, rhs, false, 0);
         std::cout << "status:   " << solver->check() << "\n";
         std::cout << "model:    " << solver->model() << "\n";
+
         VERIFY(solver->find_min(min));
         std::cout << "find_min: " << min << "\n";
         VERIFY(min == 57);  // 57*2 + 10 = 124;  56*2 + 10 = 122
 
+        VERIFY(solver->find_max(max));
+        std::cout << "find_max: " << max << "\n";
+        solver->push();
+        solver->add_ugt_const(max, false, 5);
+        VERIFY(solver->check() == l_false);
+        solver->pop(1);
+
         solver->push();
 
         // c1: 127 <= x
@@ -219,10 +228,16 @@ namespace polysat {
         solver->add_ule(lhs, rhs, false, 1);
         std::cout << "status:   " << solver->check() << "\n";
         std::cout << "model:    " << solver->model() << "\n";
+
         VERIFY(solver->find_min(min));
         std::cout << "find_min: " << min << "\n";
         VERIFY(min == 127);
 
+        VERIFY(solver->find_max(max));
+        std::cout << "find_max: " << max << "\n";
+        solver->add_ugt_const(max, false, 5);
+        VERIFY(solver->check() == l_false);
+
         solver->pop(1);
 
         // c2: umul_ovfl(2, x)
@@ -234,25 +249,41 @@ namespace polysat {
         solver->add_umul_ovfl(lhs, rhs, false, 2);
         std::cout << "status:   " << solver->check() << "\n";
         std::cout << "model:    " << solver->model() << "\n";
+
         VERIFY(solver->find_min(min));
         std::cout << "find_min: " << min << "\n";
-        solver->add_ule_const(min - 1, false, 3);
+        solver->push();
+        solver->add_ult_const(min, false, 5);
+        VERIFY(solver->check() == l_false);
+        solver->pop(1);
+
+        VERIFY(solver->find_max(max));
+        std::cout << "find_max: " << max << "\n";
+        solver->add_ugt_const(max, false, 5);
         VERIFY(solver->check() == l_false);
 
         solver->pop(1);
 
-        // c4: umul_ovfl(2, x)
+        // c3: umul_ovfl(2, x)
         lhs.clear();
         lhs.push_back(rational(2));
         rhs.clear();
         rhs.push_back(rational(0));
         rhs.push_back(rational(1));
-        solver->add_umul_ovfl(lhs, rhs, false, 4);
+        solver->add_umul_ovfl(lhs, rhs, false, 3);
         std::cout << "status:   " << solver->check() << "\n";
         std::cout << "model:    " << solver->model() << "\n";
+
         VERIFY(solver->find_min(min));
         std::cout << "find_min: " << min << "\n";
-        solver->add_ule_const(min - 1, false, 5);
+        solver->push();
+        solver->add_ult_const(min, false, 5);
+        VERIFY(solver->check() == l_false);
+        solver->pop(1);
+
+        VERIFY(solver->find_max(max));
+        std::cout << "find_max: " << max << "\n";
+        solver->add_ugt_const(max, false, 5);
         VERIFY(solver->check() == l_false);
     }
 
@@ -263,6 +294,6 @@ namespace polysat {
 void tst_viable() {
     polysat::test1();
     polysat::test_univariate();
-    polysat::test_univariate_min();
+    polysat::test_univariate_minmax();
     polysat::test2();  // takes long
 }