From 78b01bca1e03f94376b28bbfbc4f51b4bce659bd Mon Sep 17 00:00:00 2001
From: BritikovKI <BritikovKI@yandex.ru>
Date: Mon, 4 Nov 2024 11:05:12 +0100
Subject: [PATCH] NonlinWork: added support for mod

---
 src/logics/ArithLogic.cc                               | 10 ++++------
 test/regression/base/arithmetic/miniexample10.smt2     |  7 +++++++
 .../base/arithmetic/miniexample10.smt2.expected.err    |  0
 .../base/arithmetic/miniexample10.smt2.expected.out    |  5 +++++
 test/regression/base/arithmetic/miniexample2.smt2      |  1 -
 test/regression/base/arithmetic/miniexample8.smt2      |  7 +++++++
 .../base/arithmetic/miniexample8.smt2.expected.err     |  0
 .../base/arithmetic/miniexample8.smt2.expected.out     |  3 +++
 test/regression/base/arithmetic/miniexample8_Ok.smt2   |  5 +++++
 .../base/arithmetic/miniexample8_Ok.smt2.expected.err  |  0
 .../base/arithmetic/miniexample8_Ok.smt2.expected.out  |  1 +
 test/regression/base/arithmetic/miniexample8_Ok2.smt2  |  6 ++++++
 .../base/arithmetic/miniexample8_Ok2.smt2.expected.err |  0
 .../base/arithmetic/miniexample8_Ok2.smt2.expected.out |  1 +
 test/regression/base/arithmetic/miniexample9.smt2      |  6 ++++++
 .../base/arithmetic/miniexample9.smt2.expected.err     |  0
 .../base/arithmetic/miniexample9.smt2.expected.out     |  3 +++
 17 files changed, 48 insertions(+), 7 deletions(-)
 create mode 100644 test/regression/base/arithmetic/miniexample10.smt2
 create mode 100644 test/regression/base/arithmetic/miniexample10.smt2.expected.err
 create mode 100644 test/regression/base/arithmetic/miniexample10.smt2.expected.out
 create mode 100644 test/regression/base/arithmetic/miniexample8.smt2
 create mode 100644 test/regression/base/arithmetic/miniexample8.smt2.expected.err
 create mode 100644 test/regression/base/arithmetic/miniexample8.smt2.expected.out
 create mode 100644 test/regression/base/arithmetic/miniexample8_Ok.smt2
 create mode 100644 test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err
 create mode 100644 test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out
 create mode 100644 test/regression/base/arithmetic/miniexample8_Ok2.smt2
 create mode 100644 test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err
 create mode 100644 test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out
 create mode 100644 test/regression/base/arithmetic/miniexample9.smt2
 create mode 100644 test/regression/base/arithmetic/miniexample9.smt2.expected.err
 create mode 100644 test/regression/base/arithmetic/miniexample9.smt2.expected.out

diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc
index c2d1eff55..2cf913baf 100644
--- a/src/logics/ArithLogic.cc
+++ b/src/logics/ArithLogic.cc
@@ -197,11 +197,11 @@ bool ArithLogic::isLinearTerm(PTRef tr) const {
 bool ArithLogic::isNonlin(PTRef tr) const {
     if (isTimes(tr)) {
         Pterm const & term = getPterm(tr);
-        return (!isConstant(term[0]) && !isConstant(term[1]));
+        return (not isConstant(term[0]) && not isConstant(term[1]));
     }
-    if (isRealDiv(tr) || isIntDiv(tr)) {
+    if (isRealDiv(tr) || isIntDiv(tr) || isMod(getPterm(tr).symb())) {
         Pterm const & term = getPterm(tr);
-        return (!isConstant(term[1]));
+        return (not isConstant(term[1]));
     }
     return false;
 };
@@ -808,11 +808,9 @@ PTRef ArithLogic::mkMod(vec<PTRef> && args) {
     checkSortInt(args);
     PTRef dividend = args[0];
     PTRef divisor = args[1];
-
-    if (not isNumConst(divisor)) { throw ApiException("Divisor must be constant in linear logic"); }
     if (isZero(divisor)) { throw ArithDivisionByZeroException(); }
     if (isOne(divisor) or isMinusOne(divisor)) { return getTerm_IntZero(); }
-    if (isConstant(dividend)) {
+    if (isConstant(dividend) && isConstant(divisor)) {
         auto const & dividendValue = getNumConst(dividend);
         auto const & divisorValue = getNumConst(divisor);
         assert(dividendValue.isInteger() and divisorValue.isInteger());
diff --git a/test/regression/base/arithmetic/miniexample10.smt2 b/test/regression/base/arithmetic/miniexample10.smt2
new file mode 100644
index 000000000..53394539e
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample10.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* 2 a b))
+(assert (= (uninterp_mul 5 x) 10))
+(check-sat)
+(get-model)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.err b/test/regression/base/arithmetic/miniexample10.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.out b/test/regression/base/arithmetic/miniexample10.smt2.expected.out
new file mode 100644
index 000000000..264125822
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample10.smt2.expected.out
@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    1)
+)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample2.smt2 b/test/regression/base/arithmetic/miniexample2.smt2
index bd018eb56..effcb8af6 100644
--- a/test/regression/base/arithmetic/miniexample2.smt2
+++ b/test/regression/base/arithmetic/miniexample2.smt2
@@ -1,7 +1,6 @@
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
-(assert (= x x))
 (assert (= (uninterp_mul 2 x) (+ x x)))
 (check-sat)
 (get-model)
diff --git a/test/regression/base/arithmetic/miniexample8.smt2 b/test/regression/base/arithmetic/miniexample8.smt2
new file mode 100644
index 000000000..9a09e5260
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
+(assert (= (uninterp_mul x y) 0))
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.err b/test/regression/base/arithmetic/miniexample8.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.out b/test/regression/base/arithmetic/miniexample8.smt2.expected.out
new file mode 100644
index 000000000..aa2d0cf74
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8.smt2.expected.out
@@ -0,0 +1,3 @@
+(error "Nonlinear operations in the formula: (mod x y)")
+
+sat
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2 b/test/regression/base/arithmetic/miniexample8_Ok.smt2
new file mode 100644
index 000000000..8d277d485
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8_Ok.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_LIA)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
+(assert (= (uninterp_mul 1 2) 0))
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out
new file mode 100644
index 000000000..48cf80874
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out
@@ -0,0 +1 @@
+unsat
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2 b/test/regression/base/arithmetic/miniexample8_Ok2.smt2
new file mode 100644
index 000000000..741ce62af
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8_Ok2.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
+(assert (= (uninterp_mul x 5) 0))
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out
new file mode 100644
index 000000000..30d440c39
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out
@@ -0,0 +1 @@
+sat
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample9.smt2 b/test/regression/base/arithmetic/miniexample9.smt2
new file mode 100644
index 000000000..45c07977b
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample9.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
+(assert (= (uninterp_mul 5 x) 0))
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.err b/test/regression/base/arithmetic/miniexample9.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.out b/test/regression/base/arithmetic/miniexample9.smt2.expected.out
new file mode 100644
index 000000000..8043736ab
--- /dev/null
+++ b/test/regression/base/arithmetic/miniexample9.smt2.expected.out
@@ -0,0 +1,3 @@
+(error "Nonlinear operations in the formula: (mod 5 x)")
+
+sat
\ No newline at end of file