From 8d8657ac0df80d2a9c22e68489653b9bb38d99d4 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Mon, 4 Nov 2024 11:05:12 +0100 Subject: [PATCH] NonlinWork: added support for mod --- src/logics/ArithLogic.cc | 12 ++++-------- 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 +++++ .../arithmetic/miniexample8_Ok.smt2.expected.err | 0 .../arithmetic/miniexample8_Ok.smt2.expected.out | 1 + .../regression/base/arithmetic/miniexample8_Ok2.smt2 | 6 ++++++ .../arithmetic/miniexample8_Ok2.smt2.expected.err | 0 .../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 +++ test/unit/test_Rewriting.cc | 1 + 18 files changed, 49 insertions(+), 9 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..7b409b1c8 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; }; @@ -689,8 +689,6 @@ PTRef ArithLogic::mkTimes(vec && 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 && 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..4863712af --- /dev/null +++ b/test/regression/base/arithmetic/miniexample10.smt2.expected.out @@ -0,0 +1,5 @@ +sat +( + (define-fun x () Int + 1) +) 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..beab740be --- /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 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..3f65111b0 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out @@ -0,0 +1 @@ +unsat 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..6b8a2c3d2 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out @@ -0,0 +1 @@ +sat 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..57d26b569 --- /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 diff --git a/test/unit/test_Rewriting.cc b/test/unit/test_Rewriting.cc index d4e883cc7..4f15b1d54 100644 --- a/test/unit/test_Rewriting.cc +++ b/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);