From 00adce9b9fbf6af093cdc3ebb7f654dc983479ab Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 28 Nov 2024 17:36:32 +0100 Subject: [PATCH] Nested Loops: fixes --- src/api/MainSolver.cc | 5 ++--- src/logics/ArithLogic.h | 1 + src/simplifiers/LA.cc | 4 ++-- src/tsolvers/lasolver/LASolver.cc | 14 +++----------- src/tsolvers/lasolver/LASolver.h | 1 - test/regression/base/arithmetic/miniexample3.smt2 | 1 - .../base/arithmetic/miniexample3_Ok.smt2 | 1 - test/unit/test_Ites.cc | 2 +- 8 files changed, 9 insertions(+), 20 deletions(-) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index cda6aa342..2d5e93730 100644 --- a/src/api/MainSolver.cc +++ b/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()); diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index b1e8c2cf0..c01c0ba23 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -355,6 +355,7 @@ class ArithLogic : public Logic { bool isLinearTerm(PTRef tr) const; bool isLinearFactor(PTRef tr) const; pair> getConstantAndFactors(PTRef sum) const; + // Given a term `t` is splits the term into monomial and its coefficient pair splitPolyTerm(PTRef term) const; PTRef normalizeMul(PTRef mul); // Given a sum term 't' returns a normalized inequality 'c <= s' equivalent to '0 <= t' diff --git a/src/simplifiers/LA.cc b/src/simplifiers/LA.cc index ea964bc9a..f07ad0e0d 100644 --- a/src/simplifiers/LA.cc +++ b/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; diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 4f1345746..5ea229cf8 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/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)); (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 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); @@ -306,8 +298,8 @@ LVRef LASolver::registerArithmeticTerm(PTRef expr) { if (logic.isNumVar(expr) || logic.isTimesLin(expr)) { // Case (1), (2a), and (2b) auto [v,c] = logic.splitPolyTerm(expr); - assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v)))); x = getLAVar_single(v); + assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v)))); simplex.newNonbasicVar(x); notifyVar(x); } diff --git a/src/tsolvers/lasolver/LASolver.h b/src/tsolvers/lasolver/LASolver.h index f10e8cab8..eb09515b9 100644 --- a/src/tsolvers/lasolver/LASolver.h +++ b/src/tsolvers/lasolver/LASolver.h @@ -24,7 +24,6 @@ #include namespace opensmt { - class LAVarStore; class Delta; class PartitionManager; diff --git a/test/regression/base/arithmetic/miniexample3.smt2 b/test/regression/base/arithmetic/miniexample3.smt2 index 99f1ca183..3b95f63d7 100644 --- a/test/regression/base/arithmetic/miniexample3.smt2 +++ b/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) diff --git a/test/regression/base/arithmetic/miniexample3_Ok.smt2 b/test/regression/base/arithmetic/miniexample3_Ok.smt2 index 63242051f..ac7406bb4 100644 --- a/test/regression/base/arithmetic/miniexample3_Ok.smt2 +++ b/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) diff --git a/test/unit/test_Ites.cc b/test/unit/test_Ites.cc index 0645c9aea..2a37bc126 100644 --- a/test/unit/test_Ites.cc +++ b/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)); }