Nested Loops: fixes

Author: BritikovKI

src/api/MainSolver.cc

@@ -339,8 +339,7 @@ sstat MainSolver::check() {
         rval = simplifyFormulas();
     } catch (opensmt::NonLinException const & error) {
         reasonUnknown = error.what();
-        rval = s_Undef;
-        return rval;
+        return s_Undef;
     }
 
     if (config.dump_query()) printCurrentAssertionsAsQuery();
@@ -350,7 +349,7 @@ sstat MainSolver::check() {
             rval = solve();
         } catch (std::overflow_error const & error) { rval = s_Error; } catch (opensmt::NonLinException const & error) {
             reasonUnknown = error.what();
-            rval = s_Undef;
+            return s_Undef;
         }
         if (rval == s_False) {
             assert(not smt_solver->isOK());

src/logics/ArithLogic.h

@@ -355,6 +355,7 @@ class ArithLogic : public Logic {
     bool isLinearTerm(PTRef tr) const;
     bool isLinearFactor(PTRef tr) const;
     pair<Number, vec<PTRef>> getConstantAndFactors(PTRef sum) const;
+    // Given a term `t` is splits the term into monomial and its coefficient
     pair<PTRef, PTRef> splitPolyTerm(PTRef term) const;
     PTRef normalizeMul(PTRef mul);
     // Given a sum term 't' returns a normalized inequality 'c <= s' equivalent to '0 <= t'

src/simplifiers/LA.cc

@@ -63,8 +63,8 @@ void LAExpression::initialize(PTRef e, bool do_canonize) {
             curr_term.emplace_back(var);
             curr_const.emplace_back(std::move(new_c));
         } else {
-            // Otherwise it is a variable, Ite, UF or constant
-            assert(logic.isMonomial(t) || logic.isConstant(t) || logic.isUF(t));
+            // Otherwise it is a monomial or constant
+            assert(logic.isMonomial(t) || logic.isConstant(t));
             if (logic.isConstant(t)) {
                 const Real tval = logic.getNumConst(t);
                 polynome[PTRef_Undef] += tval * c;

src/tsolvers/lasolver/LASolver.cc

@@ -92,8 +92,7 @@ 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.isTimesLinNonlin(sum) || logic.isMod(logic.getPterm(sum).symb()) ||
-           logic.isRealDiv(sum) || logic.isIntDiv(sum));
+    assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimesLinNonlin(sum) || logic.isRealDiv(sum));
     (void) cons; (void)sum;
 }
 
@@ -244,7 +243,7 @@ LVRef LASolver::getVarForLeq(PTRef ref) const {
 }
 
 LVRef LASolver::getLAVar_single(PTRef expr_in) {
-
+    if (logic.isNonlin(expr_in)) throw NonLinException(logic.pp(expr_in));
     assert(logic.isLinearTerm(expr_in));
     PTId id = logic.getPterm(expr_in).getId();
 
@@ -288,13 +287,6 @@ std::unique_ptr<Tableau::Polynomial> LASolver::expressionToLVarPoly(PTRef term)
 //
 // Returns internalized reference for the term
 LVRef LASolver::registerArithmeticTerm(PTRef expr) {
-    if (logic.isTimesNonlin(expr)) throw NonLinException(logic.pp(expr));
-    else if(logic.isTimesLin(expr)  || logic.isPlus(expr)) {
-        Pterm const & subterms = logic.getPterm(expr);
-        for(auto subterm: subterms) {
-            if (logic.isNonlin(subterm)) throw NonLinException(logic.pp(subterm));
-        }
-    }
     LVRef x = LVRef::Undef;
     if (laVarMapper.hasVar(expr)){
         x = getVarForTerm(expr);

src/tsolvers/lasolver/LASolver.h

@@ -24,7 +24,6 @@
 #include <unordered_set>
 
 namespace opensmt {
-
 class LAVarStore;
 class Delta;
 class PartitionManager;

test/regression/base/arithmetic/miniexample3.smt2

@@ -2,7 +2,6 @@
 (declare-fun x () Int)
 (declare-fun y () Int)
 (define-fun uninterp_mul ((a Int) (b Int)) Int (+ (* a b) 10))
-(assert (= x x))
 (assert (= (uninterp_mul y x) 30))
 (check-sat)
 (exit)

test/regression/base/arithmetic/miniexample3_Ok.smt2

@@ -2,7 +2,6 @@
 (declare-fun x () Int)
 (declare-fun y () Int)
 (define-fun uninterp_mul ((a Int) (b Int)) Int (+ (* a b) 10))
-(assert (= x x))
 (assert (= (uninterp_mul y 5) 30))
 (check-sat)
 (get-model)

test/unit/test_Ites.cc

@@ -136,7 +136,7 @@ TEST_F(IteManagerTest, test_IteTimesVar) {
     PTRef c2 = logic.mkConst("2");
     PTRef ite = logic.mkIte(cond, c1, c2);
 
-    EXPECT_NO_THROW(logic.mkTimes(ite,x));
+    EXPECT_NO_THROW(logic.mkTimes(ite, x));
 
 }