NonlinWork: moved and updated the Nonlin checks, tests rework, except…

…ion upd

src/itehandler/IteToSwitch.cc

@@ -233,12 +233,6 @@ ite::Dag IteToSwitch::constructIteDag(PTRef root, Logic const & logic) {
 
         } else { // not Ite
             for (PTRef child : t) {
-                if (logic.hasIntegers() || logic.hasReals()) {
-                    if (logic.isNonlin(child)) {
-                        auto termStr = logic.pp(child);
-                        throw ApiException("Nonlinear operations in the formula: " + termStr);
-                    }
-                }
                 if (logic.isIte(child) and !dag.isTopLevelIte(child)) {
                     // Term child is an ite which appears as a child of a non-ite.
                     // We store this term for an expansion into a switch.

src/logics/ArithLogic.cc

@@ -195,13 +195,25 @@ bool ArithLogic::isLinearTerm(PTRef tr) const {
 }
 
 bool ArithLogic::isNonlin(PTRef tr) const {
+    if (isPlus(tr)) {
+        Pterm const & term = getPterm(tr);
+        for (auto subterm : term) {
+            if (isNonlin(subterm)) return true;
+        }
+    }
     if (isTimes(tr)) {
         Pterm const & term = getPterm(tr);
-        return (not isConstant(term[0]) && not isConstant(term[1]));
+        if (not isConstant(term[0]) && not isConstant(term[1])) return true;
+        for (auto subterm : term) {
+            if (isNonlin(subterm)) return true;
+        }
     }
     if (isRealDiv(tr) || isIntDiv(tr) || isMod(getPterm(tr).symb())) {
         Pterm const & term = getPterm(tr);
-        return (not isConstant(term[1]));
+        if (not isConstant(term[1])) return true;
+        for (auto subterm : term) {
+            if (isNonlin(subterm)) return true;
+        }
     }
     return false;
 };
@@ -419,13 +431,12 @@ lbool ArithLogic::arithmeticElimination(vec<PTRef> const & top_level_arith, Subs
         PTRef lhs = logic.getPterm(eq)[0];
         PTRef rhs = logic.getPterm(eq)[1];
         PTRef polyTerm = lhs == logic.getZeroForSort(logic.getSortRef(lhs)) ? rhs : logic.mkMinus(rhs, lhs);
-        assert(logic.isLinearTerm(polyTerm));
         if (logic.isLinearFactor(polyTerm)) {
             auto [var, c] = logic.splitTermToVarAndConst(polyTerm);
             auto coeff = logic.getNumConst(c);
             poly.addTerm(var, std::move(coeff));
         } else {
-            assert(logic.isPlus(polyTerm));
+            assert(logic.isPlus(polyTerm) || logic.isTimes(polyTerm));
             for (PTRef factor : logic.getPterm(polyTerm)) {
                 auto [var, c] = logic.splitTermToVarAndConst(factor);
                 auto coeff = logic.getNumConst(c);

src/logics/ArithLogic.h

@@ -235,7 +235,7 @@ class ArithLogic : public Logic {
 
     // Real terms are of form c, a, or (* c a) where c is a constant and a is a variable or Ite.
     bool isNumTerm(PTRef tr) const;
-    bool isNonlin(PTRef tr) const override;
+    bool isNonlin(PTRef tr) const;
 
     PTRef getTerm_IntZero() const { return term_Int_ZERO; }
     PTRef getTerm_RealZero() const { return term_Real_ZERO; }

src/logics/Logic.h

@@ -251,7 +251,6 @@ class Logic {
     bool isDisequality(PTRef tr) const;            // { return disequalities.has(term_store[tr].symb()); }
     bool isIte(SymRef tr) const;                   // { return ites.has(tr);          }
     bool isIte(PTRef tr) const;                    // { return ites.has(term_store[tr].symb()); }
-    virtual bool isNonlin(PTRef) const { return false; }
     bool isNonBoolIte(SymRef sr) const { return isIte(sr) and getSortRef(sr) != sort_BOOL; }
     bool isNonBoolIte(PTRef tr) const { return isNonBoolIte(getPterm(tr).symb()); }
 

src/rewriters/DivModRewriter.h

@@ -36,6 +36,7 @@ class DivModConfig : public DefaultRewriterConfig {
             PTRef modVar = divMod.mod;
             PTRef rewritten = logic.isIntDiv(symRef) ? divVar : modVar;
             if (not inCache) {
+                if (logic.isNonlin(term)) { return term; }
                 // collect the definitions to add
                 assert(logic.isConstant(divisor));
                 auto divisorVal = logic.getNumConst(divisor);

src/tsolvers/lasolver/LASolver.cc

@@ -91,9 +91,8 @@ void LASolver::isProperLeq(PTRef tr)
     assert(logic.isLeq(tr));
     auto [cons, sum] = logic.leqToConstantAndTerm(tr);
     assert(logic.isConstant(cons));
-    assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimes(sum));
-    assert(!logic.isTimes(sum) || ((logic.isNumVar(logic.getPterm(sum)[0]) && logic.isOne(logic.mkNeg(logic.getPterm(sum)[1]))) ||
-                                   (logic.isNumVar(logic.getPterm(sum)[1]) && logic.isOne(logic.mkNeg(logic.getPterm(sum)[0])))));
+    assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimes(sum) || logic.isMod(logic.getPterm(sum).symb()) ||
+           logic.isRealDiv(sum) || logic.isIntDiv(sum));
     (void) cons; (void)sum;
 }
 
@@ -288,6 +287,10 @@ std::unique_ptr<Tableau::Polynomial> LASolver::expressionToLVarPoly(PTRef term)
 //
 // Returns internalized reference for the term
 LVRef LASolver::registerArithmeticTerm(PTRef expr) {
+    if (logic.isNonlin(expr)) {
+        auto termStr = logic.pp(expr);
+        throw LANonLinearException(termStr.c_str());
+    }
     LVRef x = LVRef::Undef;
     if (laVarMapper.hasVar(expr)){
         x = getVarForTerm(expr);

src/tsolvers/lasolver/LASolver.h

@@ -23,6 +23,17 @@
 #include <unordered_set>
 
 namespace opensmt {
+class LANonLinearException : public std::runtime_error {
+public:
+    LANonLinearException(char const * reason_) : runtime_error(reason_) {
+        msg = "Term " + std::string(reason_) + " is non-linear";
+    }
+    virtual char const * what() const noexcept override { return msg.c_str(); }
+
+private:
+    std::string msg;
+};
+
 class LAVarStore;
 class Delta;
 class PartitionManager;

test/regression/base/arithmetic/miniexample3.smt2.expected.err

@@ -0,0 +1,3 @@
+terminate called after throwing an instance of 'opensmt::LANonLinearException'
+  what():  Term (* -1 (* x y)) is non-linear
+Aborted

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

@@ -1,9 +0,0 @@
-(error "Nonlinear operations in the formula: (* x y)")
-
-sat
-(
-  (define-fun x () Int
-    0)
-  (define-fun y () Int
-    0)
-)

test/regression/base/arithmetic/miniexample4.smt2.expected.err

@@ -0,0 +1,3 @@
+terminate called after throwing an instance of 'opensmt::LANonLinearException'
+  what():  Term (* -1 (/ y x)) is non-linear
+Aborted

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

@@ -1,9 +0,0 @@
-(error "Nonlinear operations in the formula: (/ y x)")
-
-sat
-(
-  (define-fun x () Real
-    0)
-  (define-fun y () Real
-    0)
-)

test/regression/base/arithmetic/miniexample6.smt2.expected.err

@@ -0,0 +1,3 @@
+terminate called after throwing an instance of 'opensmt::LANonLinearException'
+  what():  Term (* -1 (* x y)) is non-linear
+Aborted

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

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

test/regression/base/arithmetic/miniexample7.smt2.expected.err

@@ -0,0 +1,3 @@
+terminate called after throwing an instance of 'opensmt::LANonLinearException'
+  what():  Term (* -1 (div x y)) is non-linear
+Aborted

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

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

test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err

@@ -0,0 +1,3 @@
+terminate called after throwing an instance of 'opensmt::LANonLinearException'
+  what():  Term (+ (div 10 y) (* -1 x)) is non-linear
+Aborted

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

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

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

@@ -0,0 +1,3 @@
+terminate called after throwing an instance of 'opensmt::LANonLinearException'
+  what():  Term (mod x y) is non-linear
+Aborted

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

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

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

@@ -0,0 +1,3 @@
+terminate called after throwing an instance of 'opensmt::LANonLinearException'
+  what():  Term (mod 5 x) is non-linear
+Aborted

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

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

test/unit/test_ArithLogicApi.cc

@@ -2,9 +2,6 @@
 // Created by Antti on 16.09.21.
 //
 
-#include "api/MainSolver.h"
-#include "options/SMTConfig.h"
-#include <common/StringConv.h>
 #include <gtest/gtest.h>
 #include <logics/ArithLogic.h>
 
@@ -23,31 +20,25 @@ class ArithLogicApiTest: public ::testing::Test {
 };
 
 TEST_F(ArithLogicApiTest, test_LRA) {
-    SMTConfig config;
-    MainSolver solver(lraLogic, config, "test");
     PTRef c1 = lraLogic.mkConst("213");
     PTRef r1 = lraLogic.mkConst("213.0");
     ASSERT_EQ(c1, r1);
     ASSERT_TRUE(lraLogic.yieldsSortReal(c1));
     ASSERT_TRUE(lraLogic.yieldsSortReal(r1));
     PTRef c2 = lraLogic.mkRealVar("a");
-    PTRef eq = lraLogic.mkEq(lraLogic.mkTimes(c2, c2), lraLogic.mkRealVar("a"));
     ASSERT_NO_THROW(lraLogic.mkPlus(c1, c2));
-    ASSERT_THROW(solver.insertFormula(eq), ApiException);
+    ASSERT_NO_THROW(lraLogic.mkTimes(c2, c2));
     ASSERT_THROW(lraLogic.mkIntVar("x"), ApiException);
     ASSERT_THROW(lraLogic.mkIntConst(2), ApiException);
 }
 
 TEST_F(ArithLogicApiTest, test_LIA) {
     PTRef c1 = liaLogic.mkConst("213");
-    SMTConfig config;
-    MainSolver solver(liaLogic, config, "test");
     ASSERT_TRUE(liaLogic.yieldsSortInt(c1));
     ASSERT_THROW(liaLogic.mkConst("213.0"), ApiException);
     PTRef c2 = liaLogic.mkIntVar("a");
-    PTRef eq = liaLogic.mkEq(liaLogic.mkTimes(c2, c2), liaLogic.mkIntVar("a"));
     ASSERT_NO_THROW(liaLogic.mkPlus(c1, c2));
-    ASSERT_THROW(solver.insertFormula(eq), ApiException);
+    ASSERT_NO_THROW(liaLogic.mkTimes(c2, c2));
     ASSERT_THROW(liaLogic.mkRealVar("a"), ApiException);
     ASSERT_THROW(liaLogic.mkRealConst(2), ApiException);
 }

test/unit/test_Ites.cc

@@ -8,8 +8,6 @@
 #include <itehandler/IteHandler.h>
 #include <common/TreeOps.h>
 
-#include "api/MainSolver.h"
-#include "options/SMTConfig.h"
 #include <algorithm>
 
 namespace opensmt {
@@ -131,25 +129,18 @@ TEST_F(IteManagerTest, test_IteTimesConst) {
 
 TEST_F(IteManagerTest, test_IteTimesVar) {
 
-    SMTConfig config;
-    MainSolver solver(logic, config, "test");
     PTRef x = logic.mkVar(lrasort, "x");
     PTRef y = logic.mkVar(lrasort, "y");
     PTRef cond = logic.mkEq(x, y);
     PTRef c1 = logic.mkConst("1");
     PTRef c2 = logic.mkConst("2");
     PTRef ite = logic.mkIte(cond, c1, c2);
-    PTRef times = logic.mkTimes(ite, x);
-    PTRef eq = logic.mkEq(times,c2);
 
-    EXPECT_THROW(solver.insertFormula(eq), ApiException);
+    EXPECT_NO_THROW(logic.mkTimes(ite,x));
 
 }
 
 TEST_F(IteManagerTest, test_IteTimesIte) {
-
-    SMTConfig config;
-    MainSolver solver(logic, config, "test");
     PTRef x = logic.mkVar(lrasort, "x");
     PTRef y = logic.mkVar(lrasort, "y");
     PTRef z = logic.mkVar(lrasort, "z");
@@ -160,10 +151,8 @@ TEST_F(IteManagerTest, test_IteTimesIte) {
 
     PTRef cond2 = logic.mkEq(x, z);
     PTRef ite2 = logic.mkIte(cond2, c2, c1);
-    PTRef times = logic.mkTimes(ite1, ite2);
-    PTRef eq = logic.mkEq(times, c2);
 
-    EXPECT_THROW(solver.insertFormula(eq), ApiException);
+    EXPECT_NO_THROW(logic.mkTimes(ite1, ite2));
 }
 
 TEST_F(IteManagerTest, test_IteChain) {

test/unit/test_LRALogicMkTerms.cc

@@ -2,8 +2,6 @@
 // Created by Martin Blicha on 02.11.18.
 //
 
-#include "api/MainSolver.h"
-#include "options/SMTConfig.h"
 #include <gtest/gtest.h>
 #include <logics/ArithLogic.h>
 
@@ -175,14 +173,9 @@ TEST_F(LRALogicMkTermsTest, test_SumToZero)
     ASSERT_EQ(sum, logic.getTerm_RealZero());
 }
 
-TEST_F(LRALogicMkTermsTest, test_NonLinearException)
+TEST_F(LRALogicMkTermsTest, test_NoNonLinearException)
 {
-    PTRef mul = logic.mkTimes(x,y);
-    SMTConfig config;
-    MainSolver solver(logic, config, "test");
-    PTRef two = logic.mkConst("2");
-    EXPECT_THROW(solver.insertFormula(logic.mkEq(mul,two)), ApiException);
-    EXPECT_NO_THROW(solver.insertFormula(logic.mkEq(logic.mkTimes(x,two), two)));
+    EXPECT_NO_THROW(logic.mkTimes(x,y));
 }
 
 TEST_F(LRALogicMkTermsTest, test_ConstantSimplification)