From 1fcf7cf0b7789e08d11f51b447584908e8ac7de6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Jun 2022 09:02:53 -0700
Subject: [PATCH] add nl div mod axioms

---
 src/sat/smt/arith_axioms.cpp | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index 7cb6a05b68a..e660c8f16b3 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -128,6 +128,22 @@ namespace arith {
         }
         else {
 
+
+            expr_ref mone(a.mk_int(-1), m);
+            expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m);
+            literal eqz = mk_literal(m.mk_eq(q, zero));
+            literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
+            literal mod_lt_q = mk_literal(a.mk_lt(a.mk_sub(mod, abs_q), mone));
+            
+            // q = 0 or p = (p mod q) + q * (p div q)
+            // q = 0 or (p mod q) >= 0
+            // q = 0 or (p mod q) < abs(q)
+
+            add_clause(eqz, eq);
+            add_clause(eqz, mod_ge_0);
+            add_clause(eqz, mod_lt_q);
+
+#if 0
             /*literal div_ge_0   = */ mk_literal(a.mk_ge(div, zero));
             /*literal div_le_0   = */ mk_literal(a.mk_le(div, zero));
             /*literal p_ge_0     = */ mk_literal(a.mk_ge(p, zero));
@@ -139,6 +155,8 @@ namespace arith {
             // q <= 0 or (p mod q) >= 0
             // q <= 0 or (p mod q) <  q
             // q >= 0 or (p mod q) < -q
+
+
             literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
             literal q_le_0 = mk_literal(a.mk_le(q, zero));
 
@@ -148,6 +166,22 @@ namespace arith {
             add_clause(q_le_0, mod_ge_0);
             add_clause(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
             add_clause(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
+#endif
+            
+            if (a.is_zero(p)) {
+                add_clause(eqz, mk_literal(m.mk_eq(mod, zero)));
+                add_clause(eqz, mk_literal(m.mk_eq(div, zero)));
+            }
+            else if (!a.is_numeral(q)) {
+                // (or (= y 0)  (<= (* y (div x y)) x))
+                // (or (<= y 0) (>= (* (+ y  1)  (div x y)) x))
+                // (or (>= y 0) (>= (* (+ y -1)  (div x y)) x))
+                expr_ref one(a.mk_int(1), m);
+                add_clause(eqz, mk_literal(a.mk_le(a.mk_mul(q, div), p)));
+                add_clause(mk_literal(a.mk_le(q, zero)), mk_literal(a.mk_ge(a.mk_mul(a.mk_add(q,  one), div), q)));
+                add_clause(mk_literal(a.mk_ge(q, zero)), mk_literal(a.mk_ge(a.mk_mul(a.mk_add(q, mone), div), q)));
+            }
+
 
         }
         if (get_config().m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {