NonlinWork: moved and updated the Nonlin checks, tests rework, exception upd

Author: BritikovKI

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