Skip to content

Commit

Permalink
Nested Loops: fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
BritikovKI committed Nov 28, 2024
1 parent 68062a8 commit 00adce9
Show file tree
Hide file tree
Showing 8 changed files with 9 additions and 20 deletions.
5 changes: 2 additions & 3 deletions src/api/MainSolver.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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());
Expand Down
1 change: 1 addition & 0 deletions src/logics/ArithLogic.h
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down
4 changes: 2 additions & 2 deletions src/simplifiers/LA.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
14 changes: 3 additions & 11 deletions src/tsolvers/lasolver/LASolver.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down Expand Up @@ -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();

Expand Down Expand Up @@ -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);
Expand All @@ -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);
}
Expand Down
1 change: 0 additions & 1 deletion src/tsolvers/lasolver/LASolver.h
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@
#include <unordered_set>

namespace opensmt {

class LAVarStore;
class Delta;
class PartitionManager;
Expand Down
1 change: 0 additions & 1 deletion test/regression/base/arithmetic/miniexample3.smt2
Original file line number Diff line number Diff line change
Expand Up @@ -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)
1 change: 0 additions & 1 deletion test/regression/base/arithmetic/miniexample3_Ok.smt2
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion test/unit/test_Ites.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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));

}

Expand Down

0 comments on commit 00adce9

Please sign in to comment.