From 4405fa11562c33749d27ab101bbc8d9cb3ce8908 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 18 Jun 2021 14:30:56 -0700
Subject: [PATCH] add handling of misc operations

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/bv_decl_plugin.h |  1 +
 src/test/polysat.cpp     | 52 +++++++++++++++++++++++++---------------
 2 files changed, 34 insertions(+), 19 deletions(-)

diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 38456be3f..e5d0399ab 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -364,6 +364,7 @@ public:
     MATCH_UNARY(is_bv_not);
 
     MATCH_BINARY(is_bv_add);
+    MATCH_BINARY(is_bv_sub);
     MATCH_BINARY(is_bv_mul);
     MATCH_BINARY(is_bv_sle);
     MATCH_BINARY(is_bv_ule);
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 15d95c638..ea91ffebb 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -727,33 +727,44 @@ namespace polysat {
             return *r;
         bv_util bv(m);
         rational n;
-        unsigned sz;
+        unsigned sz = bv.get_bv_size(e);
         expr* a, *b;
         if (bv.is_bv_add(e, a, b)) {
             auto pa = to_pdd(m, s, expr2pdd, a);
             auto pb = to_pdd(m, s, expr2pdd, b);
             r = alloc(pdd, pa + pb);
         }
+        else if (bv.is_bv_sub(e, a, b)) {
+            auto pa = to_pdd(m, s, expr2pdd, a);
+            auto pb = to_pdd(m, s, expr2pdd, b);
+            r = alloc(pdd, pa - pb);
+        }
         else if (bv.is_bv_mul(e, a, b)) {
             auto pa = to_pdd(m, s, expr2pdd, a);
             auto pb = to_pdd(m, s, expr2pdd, b);
             r = alloc(pdd, pa * pb);
         }
         else if (bv.is_bv_udiv(e, a, b)) {
-            std::cout << "TODO udiv\n";
+            // quot = udiv(a, b)
+            // quot*b + rem == a
+            // rem < b or b == 0
+            // quot*b does not overflow
+            auto quot = s.var(s.add_var(sz));
+            auto rem = s.var(s.add_var(sz));
+            auto pa = to_pdd(m, s, expr2pdd, a);
+            auto pb = to_pdd(m, s, expr2pdd, b);            
+            s.add_eq(quot*pb + rem - pa);
+            s.add_ult(rem, pb);
+            // TODO:
+            // s.add_mul_noovfl(quot, pb);
+            r = alloc(pdd, quot);
         }
-        else if (bv.is_numeral(e, n, sz)) {
+        else if (bv.is_numeral(e, n, sz)) 
             r = alloc(pdd, s.value(n, sz));
-        }
-        else if (is_uninterp(e)) {
-            sz = bv.get_bv_size(e);
+        else if (is_uninterp(e)) 
             r = alloc(pdd, s.var(s.add_var(sz)));
-        }
-        else 
-            std::cout << "unknown " << mk_pp(e, m) << "\n";
-
-        if (!r) {
-            sz = bv.get_bv_size(e);
+        else {
+            std::cout << "UNKNOWN " << mk_pp(e, m) << "\n";
             r = alloc(pdd, s.var(s.add_var(sz)));
         }
         expr2pdd.insert(e, r);
@@ -793,15 +804,21 @@ namespace polysat {
             else if (bv.is_slt(fm, a, b) || bv.is_sgt(fm, b, a)) {
                 auto pa = to_pdd(m, s, expr2pdd, a);
                 auto pb = to_pdd(m, s, expr2pdd, b);
-                std::cout << "slt\n";
+                if (is_not)
+                    s.add_sle(pb, pa);
+                else 
+                    s.add_slt(pa, pb);
             }
             else if (bv.is_sle(fm, a, b) || bv.is_sge(fm, b, a)) {
                 auto pa = to_pdd(m, s, expr2pdd, a);
                 auto pb = to_pdd(m, s, expr2pdd, b);
-                std::cout << "sle\n";
+                if (is_not)
+                    s.add_slt(pb, pa);
+                else 
+                    s.add_sle(pa, pb);
             }
             else {
-                std::cout << "formula: " << is_not << " " << mk_pp(fm, m) << "\n";            
+                std::cout << "SKIP: " << mk_pp(fm, m) << "\n";            
             }
         }
         for (auto [k,v] : expr2pdd)
@@ -842,19 +859,15 @@ void tst_polysat() {
 #endif
 }
 
-// TBD also add test that loads from a file and runs the polysat engine.
-// sketch follows below:
 
 #include "ast/bv_decl_plugin.h"
 
 
-
 void tst_polysat_argv(char** argv, int argc, int& i) {
     // set up SMT2 parser to extract assertions
     // assume they are simple bit-vector equations (and inequations)
     // convert to solver state.
     
-    std::cout << "argc " << argc << "\n";
     if (argc < 3) {
         std::cerr << "Usage: " << argv[0] << " FILE\n";
         return;
@@ -872,5 +885,6 @@ void tst_polysat_argv(char** argv, int argc, int& i) {
     auto fmls = ctx.assertions();
     polysat::scoped_solver s("polysat");
     polysat::internalize(m, s, fmls);
+    std::cout << "checking\n";
     s.check();
 }