From 8a5addd891da2fbbe43e663a9a6424adbd8e8978 Mon Sep 17 00:00:00 2001
From: alexandernutz <14171425+alexandernutz@users.noreply.github.com>
Date: Thu, 20 May 2021 19:00:13 +0200
Subject: [PATCH] make the two monotonicity tests into one using push/pop; fix
 division modelling (#5220)

* make the two monotonicity tests into one using push/pop

* whitespace...

* proper division modelling for monotonicity test -- overflow checks still missing, though

* double bitwidth for overflow checking in monotonicity example
---
 src/test/polysat.cpp | 101 ++++++++++++++++++-------------------------
 1 file changed, 41 insertions(+), 60 deletions(-)

diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 30bd15474..d0d5730de 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -346,108 +346,89 @@ namespace polysat {
 
 
     /**
-     * Monotonicity example from certora (1)
-     *  expected: unsat
+     * Monotonicity example from certora
      */
-    static void test_monot1() {
+    static void test_monot() {
         scoped_solver s(__func__);
-        auto bw = 5;
+
+        auto baseBw = 5;
+        auto max_int_const = 31; // (2^5 - 1) -- change this if you change baseBw
+
+        auto bw = 2 * baseBw;
+        auto max_int = s.var(s.add_var(bw));
+        s.add_eq(max_int - max_int_const);
 
         auto tb1 = s.var(s.add_var(bw));
+        s.add_ule(tb1, max_int);
         auto tb2 = s.var(s.add_var(bw));
+        s.add_ule(tb2, max_int);
         auto a = s.var(s.add_var(bw));
+        s.add_ule(a, max_int);
         auto v = s.var(s.add_var(bw));
+        s.add_ule(v, max_int);
         auto base1 = s.var(s.add_var(bw));
+        s.add_ule(base1, max_int);
         auto base2 = s.var(s.add_var(bw));
+        s.add_ule(base2, max_int);
         auto elastic1 = s.var(s.add_var(bw));
+        s.add_ule(elastic1, max_int);
         auto elastic2 = s.var(s.add_var(bw));
+        s.add_ule(elastic2, max_int);
         auto err = s.var(s.add_var(bw));
+        s.add_ule(err, max_int);
+
+        auto zero = a - a;
 
         auto rem1 = s.var(s.add_var(bw));
         auto quot2 = s.var(s.add_var(bw));
+        s.add_ule(quot2, max_int);
         auto rem2 = s.var(s.add_var(bw));
         auto rem3 = s.var(s.add_var(bw));
         auto quot4 = s.var(s.add_var(bw));
+        s.add_ule(quot4, max_int);
         auto rem4 = s.var(s.add_var(bw));
 
         s.add_diseq(elastic1);
 
-        // tb1 = (v * base1) / elastic1;
+        // division: tb1 = (v * base1) / elastic1;
         s.add_eq((tb1 * elastic1) + rem1 - (v * base1));
+        s.add_ult(rem1, elastic1);
+        s.add_ule((tb1 * elastic1), max_int);
 
-        // quot2 = (a * base1) / elastic1
+        // division: quot2 = (a * base1) / elastic1
         s.add_eq((quot2 * elastic1) + rem2 - (a * base1));
-	
+        s.add_ult(rem2, elastic1);
+        s.add_ule((quot2 * elastic1), max_int);
+
         s.add_eq(base1 + quot2 - base2);
 
         s.add_eq(elastic1 + a - elastic2);
 
-        // tb2 = ((v * base2) / elastic2);
+        // division: tb2 = ((v * base2) / elastic2);
         s.add_eq((tb2 * elastic2) + rem3 - (v * base2));
+        s.add_ult(rem3, elastic2);
+        s.add_ule((tb2 * elastic2), max_int);
 
-        // quot4 = v / (elastic1 + a);
-        s.add_eq((quot4 * (elastic1 + a)) + rem4 - v);
+        // division: quot4 = v / elastic2;
+        s.add_eq((quot4 * elastic2) + rem4 - v);
+        s.add_ult(rem4, elastic2);
+        s.add_ule((quot4 * elastic2), max_int);
 
         s.add_eq(quot4 + 1 - err);
 
+        s.push();
         s.add_ult(tb1, tb2);
         s.check();
         s.expect_unsat();
-    }
+        s.pop();
 
-    /**
-     * Monotonicity example from certora (2)
-     *  expected: unsat
-     *
-     *  only difference to (1) is the inequality right before the check
-     */
-    static void test_monot2() {
-        scoped_solver s(__func__);
-        auto bw = 5;
-
-        auto tb1 = s.var(s.add_var(bw));
-        auto tb2 = s.var(s.add_var(bw));
-        auto a = s.var(s.add_var(bw));
-        auto v = s.var(s.add_var(bw));
-        auto base1 = s.var(s.add_var(bw));
-        auto base2 = s.var(s.add_var(bw));
-        auto elastic1 = s.var(s.add_var(bw));
-        auto elastic2 = s.var(s.add_var(bw));
-        auto err = s.var(s.add_var(bw));
-
-        auto rem1 = s.var(s.add_var(bw));
-        auto quot2 = s.var(s.add_var(bw));
-        auto rem2 = s.var(s.add_var(bw));
-        auto rem3 = s.var(s.add_var(bw));
-        auto quot4 = s.var(s.add_var(bw));
-        auto rem4 = s.var(s.add_var(bw));
-
-        s.add_diseq(elastic1);
-
-        // tb1 = (v * base1) / elastic1;
-        s.add_eq((tb1 * elastic1) + rem1 - (v * base1));
-
-        // quot2 = (a * base1) / elastic1
-        s.add_eq((quot2 * elastic1) + rem2 - (a * base1));
-
-        s.add_eq(base1 + quot2 - base2);
-
-        s.add_eq(elastic1 + a - elastic2);
-
-        // tb2 = ((v * base2) / elastic2);
-        s.add_eq((tb2 * elastic2) + rem3 - (v * base2));
-
-        // quot4 = v / (elastic1 + a);
-        s.add_eq((quot4 * (elastic1 + a)) + rem4 - v);
-
-        s.add_eq(quot4 + 1 - err);
-
-        s.add_ult(tb1 + err, tb2);
+        s.push();
+        s.add_ult(tb2 + err, tb1);
         s.check();
         s.expect_unsat();
+        s.pop();
     }
 
-
     // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
     // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
     // static void test_mixed_vars() {