NonlinWork: added support for mod

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;
 };
@@ -689,8 +689,6 @@ PTRef ArithLogic::mkTimes(vec<PTRef> && args) {
     SymRef s_new;
     simp.simplify(getTimesForSort(returnSort), flatten_args, s_new, args);
     PTRef tr = mkFun(s_new, std::move(args));
-    // Either a real term or, if we constructed a multiplication of a
-    // constant and a sum, a real sum.
     return tr;
 }
 
@@ -808,11 +806,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());

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)

test/regression/base/arithmetic/miniexample10.smt2.expected.out

@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    1)
+)

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)

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)

test/regression/base/arithmetic/miniexample8.smt2.expected.out

@@ -0,0 +1,3 @@
+(error "Nonlinear operations in the formula: (mod x y)")
+
+sat

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)

test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out

@@ -0,0 +1 @@
+unsat

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)

test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out

@@ -0,0 +1 @@
+sat

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)

test/regression/base/arithmetic/miniexample9.smt2.expected.out

@@ -0,0 +1,3 @@
+(error "Nonlinear operations in the formula: (mod 5 x)")
+
+sat

test/unit/test_Rewriting.cc

@@ -84,6 +84,7 @@ TEST(Rewriting_test, test_RewriteDivMod) {
     PTRef mod = logic.mkMod(x,two);
     PTRef fla = logic.mkAnd(logic.mkEq(div, two), logic.mkEq(mod, logic.getTerm_IntZero()));
     PTRef rewritten = rewriteDivMod(logic, fla);
+//    std::cout << logic.printTerm(rewritten) << std::endl;
     SMTConfig config;
     MainSolver solver(logic, config, "test");
     solver.insertFormula(rewritten);