From 06306c8327d3947e8ada9045e6960b83db97a3dc Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Tue, 29 Oct 2024 14:27:22 +0100 Subject: [PATCH 01/20] NonlinWork: initial commit --- src/api/Interpret.cc | 8 +++ src/api/MainSolver.cc | 3 + src/itehandler/IteToSwitch.cc | 6 ++ src/logics/ArithLogic.cc | 104 +++++++++++++++++++++++++++------- src/logics/ArithLogic.h | 6 +- src/logics/Logic.h | 3 + 6 files changed, 108 insertions(+), 22 deletions(-) diff --git a/src/api/Interpret.cc b/src/api/Interpret.cc index cd5e32e35..8e6c87ac3 100644 --- a/src/api/Interpret.cc +++ b/src/api/Interpret.cc @@ -239,6 +239,7 @@ void Interpret::interp(ASTNode& n) { } break; } + // TODO: insertFormula case t_definefun: { if (isInitialized()) { defineFun(n); @@ -425,6 +426,13 @@ PTRef Interpret::resolveTerm(const char* s, vec&& args, SRef sortRef, Sym return logic->resolveTerm(s, std::move(args), sortRef, symbolMatcher); } +//bool Interpret::checkNonlin(const PTRef formula) { +// if(isTimes(formula)){ +// +// } +// +//} + PTRef Interpret::parseTerm(const ASTNode& term, LetRecords& letRecords) { ASTType t = term.getType(); if (t == TERM_T) { diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 44b6bb28b..575db1d77 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -147,7 +147,9 @@ sstat MainSolver::simplifyFormulas() { continue; } theory->afterPreprocessing(preprocessor.getPreprocessedFormulas()); + std::cout << "FLA Formulas: "; for (PTRef fla : frameFormulas) { + std::cout << "Before:" << logic.pp(fla) << "\n"; if (fla == logic.getTerm_true()) { continue; } assert(pmanager.getPartitionIndex(fla) != -1); // Optimize the dag for cnfization @@ -158,6 +160,7 @@ sstat MainSolver::simplifyFormulas() { } assert(pmanager.getPartitionIndex(fla) != -1); pmanager.propagatePartitionMask(fla); + std::cout << "After:" << logic.pp(fla) << "\n"; status = giveToSolver(fla, frames[i].getId()); if (status == s_False) { break; } } diff --git a/src/itehandler/IteToSwitch.cc b/src/itehandler/IteToSwitch.cc index f082fd089..69a3be13a 100644 --- a/src/itehandler/IteToSwitch.cc +++ b/src/itehandler/IteToSwitch.cc @@ -233,6 +233,12 @@ 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(tr); + 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. diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 74c8b86c7..a33fac8eb 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -184,6 +184,15 @@ bool ArithLogic::isLinearFactor(PTRef tr) const { return false; } +bool ArithLogic::isNonlinearFactor(PTRef tr) const { + if (isNumConst(tr) || isNumVarLike(tr)) { return false; } + if (isTimes(tr) || isRealDiv(tr) || isIntDiv(tr)) { + Pterm const & term = getPterm(tr); + return (!isNumConst(term[0]) && !isNumConst(term[1])); + } + return false; +} + bool ArithLogic::isLinearTerm(PTRef tr) const { if (isLinearFactor(tr)) { return true; } if (isPlus(tr)) { @@ -209,7 +218,7 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { assert(constant == PTRef_Undef); constant = arg; } else { - assert(isLinearFactor(arg)); + assert(isLinearFactor(arg) || isNonlinearFactor(arg)); varFactors.push(arg); } } @@ -220,8 +229,20 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { return {std::move(constantValue), std::move(varFactors)}; } + +pair ArithLogic::splitTerm(PTRef term) const { + assert(isTimes(term) || isRealDiv(term) || isIntDiv(term)); + assert(getPterm(term).size() == 2); + PTRef var1 = getPterm(term)[0]; + PTRef var2 = getPterm(term)[1]; + if (isNumVarLike(var2)) { std::swap(var1, var2); } + assert(isNumVarLike(var1)); + return {var1, var2}; +} + + pair ArithLogic::splitTermToVarAndConst(PTRef term) const { - assert(isTimes(term) || isNumVarLike(term) || isConstant(term)); + assert(isTimes(term) || isNumVarLike(term) || isConstant(term) || isIntDiv(term) || isRealDiv(term)); if (isTimes(term)) { assert(getPterm(term).size() == 2); PTRef fac = getPterm(term)[0]; @@ -230,7 +251,7 @@ pair ArithLogic::splitTermToVarAndConst(PTRef term) const { assert(isConstant(fac)); assert(isNumVarLike(var)); return {var, fac}; - } else if (isNumVarLike(term)) { + } else if (isNumVarLike(term) || isIntDiv(term) || isRealDiv(term)) { assert(yieldsSortInt(term) or yieldsSortReal(term)); PTRef var = term; PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); @@ -477,8 +498,13 @@ pair ArithLogic::retrieveSubstitutions(vec const uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) const { assert(l.isTimes(tr)); - auto [v, c] = l.splitTermToVarAndConst(tr); - return v.x; + auto [v1, v2] = l.splitTerm(tr); +// if (l.isNumVarLike(v1) && l.isNumVarLike(v2)) { +// auto termStr = l.pp(tr); +// throw LANonLinearException(termStr.c_str()); +// } + if (l.isNumVarLike(v1)) return v1.x; + return v2.x; } bool LessThan_deepPTRef::operator()(PTRef x_, PTRef y_) const { @@ -508,6 +534,7 @@ bool ArithLogic::isNumTerm(PTRef tr) const { return false; } + PTRef ArithLogic::mkNeg(PTRef tr) { assert(!isNeg(tr)); // MB: The invariant now is that there is no "Minus" node SymRef symref = getSymRef(tr); @@ -529,10 +556,17 @@ PTRef ArithLogic::mkNeg(PTRef tr) { PTRef tr_n = mkFun(symref, std::move(args)); return tr_n; } - if (isTimes(symref)) { // constant * var-like + if (isTimes(symref) || isRealDiv(symref) || isIntDiv(symref)) { // constant * var-like assert(getPterm(tr).size() == 2); - auto [var, constant] = splitTermToVarAndConst(tr); - return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)}); + // TODO: KB: NEG of TIMES + + auto [var1, var2] = splitTerm(tr); +// if (isConstant(var2)) + return var2 == getMinusOneForSort(getSortRef(symref)) ? var1 : mkFun(symref, {var1, mkNeg(var2)}); +// else +// return mkFun(symref, {var1, getMinusOneForSort(getSortRef(symref))}); +// auto [var, constant] = splitTermToVarAndConst(tr); +// return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)}); } if (isNumVarLike(symref)) { auto sortRef = getSortRef(symref); @@ -602,8 +636,17 @@ PTRef ArithLogic::mkPlus(vec && args) { }; std::vector simplified; simplified.reserve(args.size()); - for (PTRef arg : args) { + SRef sr = getUniqueArgSort(arg); + if(isTimes(arg) || isIntDiv(arg) || isRealDiv(arg)){ + auto [v1, v2] = splitTerm(arg); + if (!isConstant(v2)) { + simplified.push_back({.var = arg, .coeff = 1}); + continue; + } + } + + auto [v, c] = splitTermToVarAndConst(arg); assert(c != PTRef_Undef); assert(isConstant(c)); @@ -673,12 +716,12 @@ PTRef ArithLogic::mkTimes(vec && args) { PTRef tr = mkFun(s_new, std::move(args)); // Either a real term or, if we constructed a multiplication of a // constant and a sum, a real sum. - if (isNumTerm(tr) || isPlus(tr) || isUF(tr) || isIte(tr)) - return tr; - else { - auto termStr = pp(tr); - throw LANonLinearException(termStr.c_str()); - } +// if (isNumTerm(tr) || isPlus(tr) || isUF(tr) || isIte(tr)) + return tr; +// else { +// auto termStr = pp(tr); +// throw LANonLinearException(termStr.c_str()); +// } } SymRef ArithLogic::getLeqForSort(SRef sr) const { @@ -818,7 +861,7 @@ PTRef ArithLogic::mkIntDiv(vec && args) { assert(args.size() == 2); PTRef dividend = args[0]; PTRef divisor = args[1]; - if (not isConstant(divisor)) { throw LANonLinearException("Divisor must be constant in linear logic"); } +// if (not isConstant(divisor)) { throw LANonLinearException("Divisor must be constant in linear logic"); } if (isZero(divisor)) { throw ArithDivisionByZeroException(); } if (isOne(divisor)) { return dividend; } if (isMinusOne(divisor)) { return mkNeg(dividend); } @@ -839,15 +882,19 @@ PTRef ArithLogic::mkRealDiv(vec && args) { checkSortReal(args); if (args.size() != 2) { throw ApiException("Division operation requires exactly 2 arguments"); } if (isZero(args[1])) { throw ArithDivisionByZeroException(); } - if (not isConstant(args[1])) { - throw LANonLinearException("Only division by constant is permitted in linear arithmetic!"); - } +// if (not isConstant(args[1])) { +// throw LANonLinearException("Only division by constant is permitted in linear arithmetic!"); +// } SimplifyConstDiv simp(*this); vec args_new; SymRef s_new; simp.simplify(get_sym_Real_DIV(), args, s_new, args_new); - if (isRealDiv(s_new)) { - assert((isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])); +// if (isRealDiv(s_new)) { +// assert((isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])); +// args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1])); +// return mkTimes(args_new); +// } + if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])) { args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1])); return mkTimes(args_new); } @@ -1200,6 +1247,13 @@ pair ArithLogic::sumToNormalizedIntPair(PTRef sum) { std::vector coeffs; coeffs.reserve(varFactors.size()); for (PTRef factor : varFactors) { + if(isTimes(factor) || isRealDiv(factor) || isIntDiv(factor)){ + auto [t1, t2] = splitTerm(factor); + if(!isConstant(t1) && !isConstant(t2)){ + auto termStr = pp(factor); + throw LANonLinearException(termStr.c_str()); + } + } auto [var, coeff] = splitTermToVarAndConst(factor); assert(ArithLogic::isNumVarLike(var) and isNumConst(coeff)); vars.push(var); @@ -1277,6 +1331,14 @@ pair ArithLogic::sumToNormalizedRealPair(PTRef sum) { auto [constantValue, varFactors] = getConstantAndFactors(sum); PTRef leadingFactor = varFactors[0]; + + if(isTimes(leadingFactor) || isRealDiv(leadingFactor) || isIntDiv(leadingFactor)){ + auto [t1, t2] = splitTerm(leadingFactor); + if(!isConstant(t1) && !isConstant(t2)){ + auto termStr = pp(leadingFactor); + throw LANonLinearException(termStr.c_str()); + } + } // normalize the sum according to the leading factor auto [var, coeff] = splitTermToVarAndConst(leadingFactor); Number normalizationCoeff = abs(getNumConst(coeff)); diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index ecbdc9348..c0a738b32 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -223,7 +223,8 @@ class ArithLogic : public Logic { bool isNumVar(SymRef sr) const { return isVar(sr) and (yieldsSortInt(sr) or yieldsSortReal(sr)); } bool isNumVar(PTRef tr) const { return isNumVar(getPterm(tr).symb()); } bool isNumVarLike(SymRef sr) const { - return yieldsSortNum(sr) and not isPlus(sr) and not isTimes(sr) and not isNumConst(sr); + return yieldsSortNum(sr) and not isPlus(sr) and not isTimes(sr) and not isNumConst(sr) and not isRealDiv(sr) + and not isIntDiv(sr); } bool isNumVarLike(PTRef tr) const { return isNumVarLike(getPterm(tr).symb()); } @@ -245,6 +246,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 { return isNonlinearFactor(tr); }; PTRef getTerm_IntZero() const { return term_Int_ZERO; } PTRef getTerm_RealZero() const { return term_Real_ZERO; } @@ -460,6 +462,8 @@ class ArithLogic : public Logic { SymRef sym_Int_GT; SymRef sym_Int_ITE; SymRef sym_Int_DISTINCT; + pair splitTerm(PTRef term) const; + bool isNonlinearFactor(PTRef tr) const; }; // Determine for two multiplicative terms (* k1 v1) and (* k2 v2), v1 != diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 9a144ee61..03129bc39 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -251,6 +251,9 @@ 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 tr) 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()); } From 59c9152e6db16c871cca4a641770a36441255f5b Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Tue, 29 Oct 2024 15:34:05 +0100 Subject: [PATCH 02/20] NonlinWork: additional fixes concerning division and nonlin --- src/logics/ArithLogic.cc | 36 +++++++++++++++++++++++++++++------- 1 file changed, 29 insertions(+), 7 deletions(-) diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index a33fac8eb..01f04d3ee 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -181,15 +181,23 @@ bool ArithLogic::isLinearFactor(PTRef tr) const { return term.size() == 2 && ((isNumConst(term[0]) && (isNumVarLike(term[1]))) || (isNumConst(term[1]) && (isNumVarLike(term[0])))); } + if (isRealDiv(tr) || isIntDiv(tr)) { + Pterm const & term = getPterm(tr); + return (isNumConst(term[1])); + } return false; } bool ArithLogic::isNonlinearFactor(PTRef tr) const { if (isNumConst(tr) || isNumVarLike(tr)) { return false; } - if (isTimes(tr) || isRealDiv(tr) || isIntDiv(tr)) { + if (isTimes(tr)) { Pterm const & term = getPterm(tr); return (!isNumConst(term[0]) && !isNumConst(term[1])); } + if (isRealDiv(tr) || isIntDiv(tr)) { + Pterm const & term = getPterm(tr); + return (!isNumConst(term[1])); + } return false; } @@ -235,14 +243,22 @@ pair ArithLogic::splitTerm(PTRef term) const { assert(getPterm(term).size() == 2); PTRef var1 = getPterm(term)[0]; PTRef var2 = getPterm(term)[1]; - if (isNumVarLike(var2)) { std::swap(var1, var2); } - assert(isNumVarLike(var1)); +// if (isNumVarLike(var2)) { std::swap(var1, var2); } +// assert(isNumVarLike(var1)); return {var1, var2}; } pair ArithLogic::splitTermToVarAndConst(PTRef term) const { assert(isTimes(term) || isNumVarLike(term) || isConstant(term) || isIntDiv(term) || isRealDiv(term)); + if(isIntDiv(term) || isRealDiv(term)) { + assert(getPterm(term).size() == 2); + PTRef fac = getPterm(term)[1]; + PTRef var = getPterm(term)[0]; + assert(isConstant(fac)); + assert(isNumVarLike(var)); + return {var, fac}; + } if (isTimes(term)) { assert(getPterm(term).size() == 2); PTRef fac = getPterm(term)[0]; @@ -251,7 +267,7 @@ pair ArithLogic::splitTermToVarAndConst(PTRef term) const { assert(isConstant(fac)); assert(isNumVarLike(var)); return {var, fac}; - } else if (isNumVarLike(term) || isIntDiv(term) || isRealDiv(term)) { + } else if (isNumVarLike(term) ) { assert(yieldsSortInt(term) or yieldsSortReal(term)); PTRef var = term; PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); @@ -561,6 +577,9 @@ PTRef ArithLogic::mkNeg(PTRef tr) { // TODO: KB: NEG of TIMES auto [var1, var2] = splitTerm(tr); + if(isTimes(tr) && !isConstant(var2)){ + std::swap(var1, var2); + } // if (isConstant(var2)) return var2 == getMinusOneForSort(getSortRef(symref)) ? var1 : mkFun(symref, {var1, mkNeg(var2)}); // else @@ -640,7 +659,8 @@ PTRef ArithLogic::mkPlus(vec && args) { SRef sr = getUniqueArgSort(arg); if(isTimes(arg) || isIntDiv(arg) || isRealDiv(arg)){ auto [v1, v2] = splitTerm(arg); - if (!isConstant(v2)) { + if ((isTimes(arg) && !isConstant(v1) && !isConstant(v2)) || + ((isIntDiv(arg) || isRealDiv(arg)) && !isConstant(v2))) { simplified.push_back({.var = arg, .coeff = 1}); continue; } @@ -1249,7 +1269,8 @@ pair ArithLogic::sumToNormalizedIntPair(PTRef sum) { for (PTRef factor : varFactors) { if(isTimes(factor) || isRealDiv(factor) || isIntDiv(factor)){ auto [t1, t2] = splitTerm(factor); - if(!isConstant(t1) && !isConstant(t2)){ + if((isTimes(factor) && !isConstant(t1) && !isConstant(t2)) || + ((isIntDiv(factor) || isRealDiv(factor)) && !isConstant(t2))){ auto termStr = pp(factor); throw LANonLinearException(termStr.c_str()); } @@ -1334,7 +1355,8 @@ pair ArithLogic::sumToNormalizedRealPair(PTRef sum) { if(isTimes(leadingFactor) || isRealDiv(leadingFactor) || isIntDiv(leadingFactor)){ auto [t1, t2] = splitTerm(leadingFactor); - if(!isConstant(t1) && !isConstant(t2)){ + if((isTimes(leadingFactor) && !isConstant(t1) && !isConstant(t2)) || + ((isIntDiv(leadingFactor) || isRealDiv(leadingFactor)) && !isConstant(t2))){ auto termStr = pp(leadingFactor); throw LANonLinearException(termStr.c_str()); } From 9afd418f56cec108a25efee28db5504d905bd634 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Wed, 30 Oct 2024 18:04:58 +0100 Subject: [PATCH 03/20] NonlinWork: fix of tests and code rework --- src/api/MainSolver.cc | 2 +- src/api/MainSolver.h | 3 +- src/itehandler/IteToSwitch.cc | 8 +- src/logics/ArithLogic.cc | 141 ++++++++++-------------------- src/logics/ArithLogic.h | 6 +- src/logics/Logic.cc | 4 +- src/logics/Logic.h | 4 +- src/rewriters/DivModRewriter.h | 3 + test/unit/test_ArithLogicApi.cc | 14 ++- test/unit/test_Ites.cc | 14 ++- test/unit/test_LRALogicMkTerms.cc | 9 +- test/unit/test_Rewriting.cc | 1 - 12 files changed, 90 insertions(+), 119 deletions(-) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 575db1d77..1b443cb49 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -147,7 +147,7 @@ sstat MainSolver::simplifyFormulas() { continue; } theory->afterPreprocessing(preprocessor.getPreprocessedFormulas()); - std::cout << "FLA Formulas: "; + std::cout << "FLA Formulas: "; for (PTRef fla : frameFormulas) { std::cout << "Before:" << logic.pp(fla) << "\n"; if (fla == logic.getTerm_true()) { continue; } diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index 01fc6ad37..0ffe56717 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -108,8 +108,7 @@ class MainSolver { vec const & getAssertionsAtCurrentLevel() const { return getAssertionsAtLevel(getAssertionLevel()); } vec const & getAssertionsAtLevel(std::size_t) const; - [[deprecated("Use printCurrentAssertionsAsQuery")]] - void printFramesAsQuery() const { + [[deprecated("Use printCurrentAssertionsAsQuery")]] void printFramesAsQuery() const { printCurrentAssertionsAsQuery(); } void printCurrentAssertionsAsQuery() const; diff --git a/src/itehandler/IteToSwitch.cc b/src/itehandler/IteToSwitch.cc index 69a3be13a..bf878695d 100644 --- a/src/itehandler/IteToSwitch.cc +++ b/src/itehandler/IteToSwitch.cc @@ -233,10 +233,10 @@ 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(tr); - throw ApiException("Nonlinear operations in the formula: "+termStr); + 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)) { diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 01f04d3ee..0ed24a472 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -188,19 +188,6 @@ bool ArithLogic::isLinearFactor(PTRef tr) const { return false; } -bool ArithLogic::isNonlinearFactor(PTRef tr) const { - if (isNumConst(tr) || isNumVarLike(tr)) { return false; } - if (isTimes(tr)) { - Pterm const & term = getPterm(tr); - return (!isNumConst(term[0]) && !isNumConst(term[1])); - } - if (isRealDiv(tr) || isIntDiv(tr)) { - Pterm const & term = getPterm(tr); - return (!isNumConst(term[1])); - } - return false; -} - bool ArithLogic::isLinearTerm(PTRef tr) const { if (isLinearFactor(tr)) { return true; } if (isPlus(tr)) { @@ -210,6 +197,18 @@ bool ArithLogic::isLinearTerm(PTRef tr) const { return false; } +bool ArithLogic::isNonlin(PTRef tr) const { + if (isTimes(tr)) { + Pterm const & term = getPterm(tr); + return (!isConstant(term[0]) && !isConstant(term[1])); + } + if (isRealDiv(tr) || isIntDiv(tr)) { + Pterm const & term = getPterm(tr); + return (!isConstant(term[1])); + } + return false; +}; + Number const & ArithLogic::getNumConst(PTRef tr) const { SymId id = sym_store[getPterm(tr).symb()].getId(); assert(id < static_cast(numbers.size()) && numbers[id] != nullptr); @@ -226,7 +225,7 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { assert(constant == PTRef_Undef); constant = arg; } else { - assert(isLinearFactor(arg) || isNonlinearFactor(arg)); + // assert(isLinearFactor(arg) || isNonlinearFactor(arg)); varFactors.push(arg); } } @@ -237,37 +236,29 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { return {std::move(constantValue), std::move(varFactors)}; } - pair ArithLogic::splitTerm(PTRef term) const { - assert(isTimes(term) || isRealDiv(term) || isIntDiv(term)); - assert(getPterm(term).size() == 2); - PTRef var1 = getPterm(term)[0]; - PTRef var2 = getPterm(term)[1]; -// if (isNumVarLike(var2)) { std::swap(var1, var2); } -// assert(isNumVarLike(var1)); - return {var1, var2}; + PTRef fac = getPterm(term)[0]; + PTRef var = getPterm(term)[1]; + return {var, fac}; } - pair ArithLogic::splitTermToVarAndConst(PTRef term) const { - assert(isTimes(term) || isNumVarLike(term) || isConstant(term) || isIntDiv(term) || isRealDiv(term)); - if(isIntDiv(term) || isRealDiv(term)) { - assert(getPterm(term).size() == 2); - PTRef fac = getPterm(term)[1]; - PTRef var = getPterm(term)[0]; - assert(isConstant(fac)); - assert(isNumVarLike(var)); - return {var, fac}; - } + assert(isTimes(term) || isNumVarLike(term) || isConstant(term)); if (isTimes(term)) { assert(getPterm(term).size() == 2); PTRef fac = getPterm(term)[0]; PTRef var = getPterm(term)[1]; - if (not isConstant(fac)) { std::swap(fac, var); } + if (not isConstant(fac)) { + std::swap(fac, var); + if (not isConstant(fac)) { + PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); + return {term, fac}; + } + } assert(isConstant(fac)); - assert(isNumVarLike(var)); + assert(isNumVarLike(var) || isTimes(var)); return {var, fac}; - } else if (isNumVarLike(term) ) { + } else if (isNumVarLike(term)) { assert(yieldsSortInt(term) or yieldsSortReal(term)); PTRef var = term; PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); @@ -514,11 +505,7 @@ pair ArithLogic::retrieveSubstitutions(vec const uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) const { assert(l.isTimes(tr)); - auto [v1, v2] = l.splitTerm(tr); -// if (l.isNumVarLike(v1) && l.isNumVarLike(v2)) { -// auto termStr = l.pp(tr); -// throw LANonLinearException(termStr.c_str()); -// } + auto [v1, v2] = l.splitTermToVarAndConst(tr); if (l.isNumVarLike(v1)) return v1.x; return v2.x; } @@ -550,7 +537,6 @@ bool ArithLogic::isNumTerm(PTRef tr) const { return false; } - PTRef ArithLogic::mkNeg(PTRef tr) { assert(!isNeg(tr)); // MB: The invariant now is that there is no "Minus" node SymRef symref = getSymRef(tr); @@ -572,20 +558,11 @@ PTRef ArithLogic::mkNeg(PTRef tr) { PTRef tr_n = mkFun(symref, std::move(args)); return tr_n; } - if (isTimes(symref) || isRealDiv(symref) || isIntDiv(symref)) { // constant * var-like + if (isTimes(symref)) { // constant * var-like assert(getPterm(tr).size() == 2); // TODO: KB: NEG of TIMES - - auto [var1, var2] = splitTerm(tr); - if(isTimes(tr) && !isConstant(var2)){ - std::swap(var1, var2); - } -// if (isConstant(var2)) - return var2 == getMinusOneForSort(getSortRef(symref)) ? var1 : mkFun(symref, {var1, mkNeg(var2)}); -// else -// return mkFun(symref, {var1, getMinusOneForSort(getSortRef(symref))}); -// auto [var, constant] = splitTermToVarAndConst(tr); -// return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)}); + auto [var, constant] = splitTermToVarAndConst(tr); + return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)}); } if (isNumVarLike(symref)) { auto sortRef = getSortRef(symref); @@ -656,17 +633,6 @@ PTRef ArithLogic::mkPlus(vec && args) { std::vector simplified; simplified.reserve(args.size()); for (PTRef arg : args) { - SRef sr = getUniqueArgSort(arg); - if(isTimes(arg) || isIntDiv(arg) || isRealDiv(arg)){ - auto [v1, v2] = splitTerm(arg); - if ((isTimes(arg) && !isConstant(v1) && !isConstant(v2)) || - ((isIntDiv(arg) || isRealDiv(arg)) && !isConstant(v2))) { - simplified.push_back({.var = arg, .coeff = 1}); - continue; - } - } - - auto [v, c] = splitTermToVarAndConst(arg); assert(c != PTRef_Undef); assert(isConstant(c)); @@ -736,12 +702,12 @@ PTRef ArithLogic::mkTimes(vec && args) { PTRef tr = mkFun(s_new, std::move(args)); // Either a real term or, if we constructed a multiplication of a // constant and a sum, a real sum. -// if (isNumTerm(tr) || isPlus(tr) || isUF(tr) || isIte(tr)) + // if (isNumTerm(tr) || isPlus(tr) || isUF(tr) || isIte(tr)) return tr; -// else { -// auto termStr = pp(tr); -// throw LANonLinearException(termStr.c_str()); -// } + // else { + // auto termStr = pp(tr); + // throw LANonLinearException(termStr.c_str()); + // } } SymRef ArithLogic::getLeqForSort(SRef sr) const { @@ -881,7 +847,7 @@ PTRef ArithLogic::mkIntDiv(vec && args) { assert(args.size() == 2); PTRef dividend = args[0]; PTRef divisor = args[1]; -// if (not isConstant(divisor)) { throw LANonLinearException("Divisor must be constant in linear logic"); } + // if (not isConstant(divisor)) { throw LANonLinearException("Divisor must be constant in linear logic"); } if (isZero(divisor)) { throw ArithDivisionByZeroException(); } if (isOne(divisor)) { return dividend; } if (isMinusOne(divisor)) { return mkNeg(dividend); } @@ -902,18 +868,18 @@ PTRef ArithLogic::mkRealDiv(vec && args) { checkSortReal(args); if (args.size() != 2) { throw ApiException("Division operation requires exactly 2 arguments"); } if (isZero(args[1])) { throw ArithDivisionByZeroException(); } -// if (not isConstant(args[1])) { -// throw LANonLinearException("Only division by constant is permitted in linear arithmetic!"); -// } + // if (not isConstant(args[1])) { + // throw LANonLinearException("Only division by constant is permitted in linear arithmetic!"); + // } SimplifyConstDiv simp(*this); vec args_new; SymRef s_new; simp.simplify(get_sym_Real_DIV(), args, s_new, args_new); -// if (isRealDiv(s_new)) { -// assert((isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])); -// args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1])); -// return mkTimes(args_new); -// } + // if (isRealDiv(s_new)) { + // assert((isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])); + // args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1])); + // return mkTimes(args_new); + // } if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])) { args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1])); return mkTimes(args_new); @@ -1267,16 +1233,8 @@ pair ArithLogic::sumToNormalizedIntPair(PTRef sum) { std::vector coeffs; coeffs.reserve(varFactors.size()); for (PTRef factor : varFactors) { - if(isTimes(factor) || isRealDiv(factor) || isIntDiv(factor)){ - auto [t1, t2] = splitTerm(factor); - if((isTimes(factor) && !isConstant(t1) && !isConstant(t2)) || - ((isIntDiv(factor) || isRealDiv(factor)) && !isConstant(t2))){ - auto termStr = pp(factor); - throw LANonLinearException(termStr.c_str()); - } - } auto [var, coeff] = splitTermToVarAndConst(factor); - assert(ArithLogic::isNumVarLike(var) and isNumConst(coeff)); + assert((ArithLogic::isNumVarLike(var) || ArithLogic::isTimes(var)) and isNumConst(coeff)); vars.push(var); coeffs.push_back(getNumConst(coeff)); } @@ -1352,15 +1310,6 @@ pair ArithLogic::sumToNormalizedRealPair(PTRef sum) { auto [constantValue, varFactors] = getConstantAndFactors(sum); PTRef leadingFactor = varFactors[0]; - - if(isTimes(leadingFactor) || isRealDiv(leadingFactor) || isIntDiv(leadingFactor)){ - auto [t1, t2] = splitTerm(leadingFactor); - if((isTimes(leadingFactor) && !isConstant(t1) && !isConstant(t2)) || - ((isIntDiv(leadingFactor) || isRealDiv(leadingFactor)) && !isConstant(t2))){ - auto termStr = pp(leadingFactor); - throw LANonLinearException(termStr.c_str()); - } - } // normalize the sum according to the leading factor auto [var, coeff] = splitTermToVarAndConst(leadingFactor); Number normalizationCoeff = abs(getNumConst(coeff)); diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index c0a738b32..35023b6d1 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -223,8 +223,7 @@ class ArithLogic : public Logic { bool isNumVar(SymRef sr) const { return isVar(sr) and (yieldsSortInt(sr) or yieldsSortReal(sr)); } bool isNumVar(PTRef tr) const { return isNumVar(getPterm(tr).symb()); } bool isNumVarLike(SymRef sr) const { - return yieldsSortNum(sr) and not isPlus(sr) and not isTimes(sr) and not isNumConst(sr) and not isRealDiv(sr) - and not isIntDiv(sr); + return yieldsSortNum(sr) and not isPlus(sr) and not isTimes(sr) and not isNumConst(sr); } bool isNumVarLike(PTRef tr) const { return isNumVarLike(getPterm(tr).symb()); } @@ -246,7 +245,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 { return isNonlinearFactor(tr); }; + bool isNonlin(PTRef tr) const override; PTRef getTerm_IntZero() const { return term_Int_ZERO; } PTRef getTerm_RealZero() const { return term_Real_ZERO; } @@ -463,7 +462,6 @@ class ArithLogic : public Logic { SymRef sym_Int_ITE; SymRef sym_Int_DISTINCT; pair splitTerm(PTRef term) const; - bool isNonlinearFactor(PTRef tr) const; }; // Determine for two multiplicative terms (* k1 v1) and (* k2 v2), v1 != diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index 85f06522c..82e4c25cf 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -113,7 +113,9 @@ std::string Logic::disambiguateName(std::string const & protectedName, SRef sort assert(not protectedName.empty()); if (not isNullary or isInterpreted) { return protectedName; } - auto isQuoted = [](std::string const & s) { return s.size() > 2 and *s.begin() == '|' and *(s.end() - 1) == '|'; }; + auto isQuoted = [](std::string const & s) { + return s.size() > 2 and * s.begin() == '|' and * (s.end() - 1) == '|'; + }; auto name = isQuoted(protectedName) ? std::string_view(protectedName.data() + 1, protectedName.size() - 2) : std::string_view(protectedName); diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 03129bc39..809093c2f 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -251,9 +251,7 @@ 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 tr) const { - return false; - } + 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()); } diff --git a/src/rewriters/DivModRewriter.h b/src/rewriters/DivModRewriter.h index 2aa90038e..564cd88eb 100644 --- a/src/rewriters/DivModRewriter.h +++ b/src/rewriters/DivModRewriter.h @@ -37,6 +37,9 @@ class DivModConfig : public DefaultRewriterConfig { PTRef rewritten = logic.isIntDiv(symRef) ? divVar : modVar; if (not inCache) { // collect the definitions to add + if (!logic.isConstant(divisor)) { + throw ApiException("Nonlinear expression in the SMT:" + logic.pp(term)); + } assert(logic.isConstant(divisor)); auto divisorVal = logic.getNumConst(divisor); assert(divisorVal.isInteger()); diff --git a/test/unit/test_ArithLogicApi.cc b/test/unit/test_ArithLogicApi.cc index ddc7dbb8e..3ee59273f 100644 --- a/test/unit/test_ArithLogicApi.cc +++ b/test/unit/test_ArithLogicApi.cc @@ -2,9 +2,11 @@ // Created by Antti on 16.09.21. // +#include "api/MainSolver.h" +#include "options/SMTConfig.h" +#include #include #include -#include namespace opensmt { @@ -21,25 +23,31 @@ 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(lraLogic.mkTimes(c2, c2), LANonLinearException); + ASSERT_THROW(solver.insertFormula(eq), ApiException); 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(liaLogic.mkTimes(c2, c2), LANonLinearException); + ASSERT_THROW(solver.insertFormula(eq), ApiException); ASSERT_THROW(liaLogic.mkRealVar("a"), ApiException); ASSERT_THROW(liaLogic.mkRealConst(2), ApiException); } diff --git a/test/unit/test_Ites.cc b/test/unit/test_Ites.cc index ff3e5b41f..03c8bd53c 100644 --- a/test/unit/test_Ites.cc +++ b/test/unit/test_Ites.cc @@ -8,6 +8,8 @@ #include #include +#include "api/MainSolver.h" +#include "options/SMTConfig.h" #include namespace opensmt { @@ -129,19 +131,25 @@ 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(logic.mkTimes(ite, x), LANonLinearException); + EXPECT_THROW(solver.insertFormula(eq), ApiException); } 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"); @@ -152,8 +160,10 @@ 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(logic.mkTimes(ite1, ite2), LANonLinearException); + EXPECT_THROW(solver.insertFormula(eq), ApiException); } TEST_F(IteManagerTest, test_IteChain) { diff --git a/test/unit/test_LRALogicMkTerms.cc b/test/unit/test_LRALogicMkTerms.cc index 03567c88a..f447535ca 100644 --- a/test/unit/test_LRALogicMkTerms.cc +++ b/test/unit/test_LRALogicMkTerms.cc @@ -2,6 +2,8 @@ // Created by Martin Blicha on 02.11.18. // +#include "api/MainSolver.h" +#include "options/SMTConfig.h" #include #include @@ -175,9 +177,12 @@ TEST_F(LRALogicMkTermsTest, test_SumToZero) TEST_F(LRALogicMkTermsTest, test_NonLinearException) { - EXPECT_THROW(logic.mkTimes(x,y), LANonLinearException); + PTRef mul = logic.mkTimes(x,y); + SMTConfig config; + MainSolver solver(logic, config, "test"); PTRef two = logic.mkConst("2"); - EXPECT_NO_THROW(logic.mkTimes(x,two)); + EXPECT_THROW(solver.insertFormula(logic.mkEq(mul,two)), ApiException); + EXPECT_NO_THROW(solver.insertFormula(logic.mkEq(logic.mkTimes(x,two), two))); } TEST_F(LRALogicMkTermsTest, test_ConstantSimplification) diff --git a/test/unit/test_Rewriting.cc b/test/unit/test_Rewriting.cc index 4f15b1d54..d4e883cc7 100644 --- a/test/unit/test_Rewriting.cc +++ b/test/unit/test_Rewriting.cc @@ -84,7 +84,6 @@ TEST(Rewriting_test, test_RewriteDivMod) { PTRef mod = logic.mkMod(x,two); PTRef fla = logic.mkAnd(logic.mkEq(div, two), logic.mkEq(mod, logic.getTerm_IntZero())); PTRef rewritten = rewriteDivMod(logic, fla); -// std::cout << logic.printTerm(rewritten) << std::endl; SMTConfig config; MainSolver solver(logic, config, "test"); solver.insertFormula(rewritten); From 9555791ce9b627d5a0af222d222c4fa4ac9b92c2 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 31 Oct 2024 12:41:56 +0100 Subject: [PATCH 04/20] NonlinWork: PR cleanup --- src/api/Interpret.cc | 8 -------- src/api/MainSolver.cc | 3 --- src/api/MainSolver.h | 3 ++- src/logics/ArithLogic.cc | 32 +++----------------------------- src/logics/ArithLogic.h | 11 ----------- src/logics/Logic.cc | 4 +--- src/rewriters/DivModRewriter.h | 3 --- 7 files changed, 6 insertions(+), 58 deletions(-) diff --git a/src/api/Interpret.cc b/src/api/Interpret.cc index 8e6c87ac3..cd5e32e35 100644 --- a/src/api/Interpret.cc +++ b/src/api/Interpret.cc @@ -239,7 +239,6 @@ void Interpret::interp(ASTNode& n) { } break; } - // TODO: insertFormula case t_definefun: { if (isInitialized()) { defineFun(n); @@ -426,13 +425,6 @@ PTRef Interpret::resolveTerm(const char* s, vec&& args, SRef sortRef, Sym return logic->resolveTerm(s, std::move(args), sortRef, symbolMatcher); } -//bool Interpret::checkNonlin(const PTRef formula) { -// if(isTimes(formula)){ -// -// } -// -//} - PTRef Interpret::parseTerm(const ASTNode& term, LetRecords& letRecords) { ASTType t = term.getType(); if (t == TERM_T) { diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 1b443cb49..44b6bb28b 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -147,9 +147,7 @@ sstat MainSolver::simplifyFormulas() { continue; } theory->afterPreprocessing(preprocessor.getPreprocessedFormulas()); - std::cout << "FLA Formulas: "; for (PTRef fla : frameFormulas) { - std::cout << "Before:" << logic.pp(fla) << "\n"; if (fla == logic.getTerm_true()) { continue; } assert(pmanager.getPartitionIndex(fla) != -1); // Optimize the dag for cnfization @@ -160,7 +158,6 @@ sstat MainSolver::simplifyFormulas() { } assert(pmanager.getPartitionIndex(fla) != -1); pmanager.propagatePartitionMask(fla); - std::cout << "After:" << logic.pp(fla) << "\n"; status = giveToSolver(fla, frames[i].getId()); if (status == s_False) { break; } } diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index 0ffe56717..01fc6ad37 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -108,7 +108,8 @@ class MainSolver { vec const & getAssertionsAtCurrentLevel() const { return getAssertionsAtLevel(getAssertionLevel()); } vec const & getAssertionsAtLevel(std::size_t) const; - [[deprecated("Use printCurrentAssertionsAsQuery")]] void printFramesAsQuery() const { + [[deprecated("Use printCurrentAssertionsAsQuery")]] + void printFramesAsQuery() const { printCurrentAssertionsAsQuery(); } void printCurrentAssertionsAsQuery() const; diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 0ed24a472..364fd41ee 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -181,10 +181,6 @@ bool ArithLogic::isLinearFactor(PTRef tr) const { return term.size() == 2 && ((isNumConst(term[0]) && (isNumVarLike(term[1]))) || (isNumConst(term[1]) && (isNumVarLike(term[0])))); } - if (isRealDiv(tr) || isIntDiv(tr)) { - Pterm const & term = getPterm(tr); - return (isNumConst(term[1])); - } return false; } @@ -225,7 +221,6 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { assert(constant == PTRef_Undef); constant = arg; } else { - // assert(isLinearFactor(arg) || isNonlinearFactor(arg)); varFactors.push(arg); } } @@ -236,12 +231,6 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { return {std::move(constantValue), std::move(varFactors)}; } -pair ArithLogic::splitTerm(PTRef term) const { - PTRef fac = getPterm(term)[0]; - PTRef var = getPterm(term)[1]; - return {var, fac}; -} - pair ArithLogic::splitTermToVarAndConst(PTRef term) const { assert(isTimes(term) || isNumVarLike(term) || isConstant(term)); if (isTimes(term)) { @@ -505,9 +494,8 @@ pair ArithLogic::retrieveSubstitutions(vec const uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) const { assert(l.isTimes(tr)); - auto [v1, v2] = l.splitTermToVarAndConst(tr); - if (l.isNumVarLike(v1)) return v1.x; - return v2.x; + auto [v, c] = l.splitTermToVarAndConst(tr); + return v.x; } bool LessThan_deepPTRef::operator()(PTRef x_, PTRef y_) const { @@ -560,7 +548,6 @@ PTRef ArithLogic::mkNeg(PTRef tr) { } if (isTimes(symref)) { // constant * var-like assert(getPterm(tr).size() == 2); - // TODO: KB: NEG of TIMES auto [var, constant] = splitTermToVarAndConst(tr); return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)}); } @@ -632,6 +619,7 @@ PTRef ArithLogic::mkPlus(vec && args) { }; std::vector simplified; simplified.reserve(args.size()); + for (PTRef arg : args) { auto [v, c] = splitTermToVarAndConst(arg); assert(c != PTRef_Undef); @@ -702,12 +690,7 @@ PTRef ArithLogic::mkTimes(vec && args) { PTRef tr = mkFun(s_new, std::move(args)); // Either a real term or, if we constructed a multiplication of a // constant and a sum, a real sum. - // if (isNumTerm(tr) || isPlus(tr) || isUF(tr) || isIte(tr)) return tr; - // else { - // auto termStr = pp(tr); - // throw LANonLinearException(termStr.c_str()); - // } } SymRef ArithLogic::getLeqForSort(SRef sr) const { @@ -847,7 +830,6 @@ PTRef ArithLogic::mkIntDiv(vec && args) { assert(args.size() == 2); PTRef dividend = args[0]; PTRef divisor = args[1]; - // if (not isConstant(divisor)) { throw LANonLinearException("Divisor must be constant in linear logic"); } if (isZero(divisor)) { throw ArithDivisionByZeroException(); } if (isOne(divisor)) { return dividend; } if (isMinusOne(divisor)) { return mkNeg(dividend); } @@ -868,18 +850,10 @@ PTRef ArithLogic::mkRealDiv(vec && args) { checkSortReal(args); if (args.size() != 2) { throw ApiException("Division operation requires exactly 2 arguments"); } if (isZero(args[1])) { throw ArithDivisionByZeroException(); } - // if (not isConstant(args[1])) { - // throw LANonLinearException("Only division by constant is permitted in linear arithmetic!"); - // } SimplifyConstDiv simp(*this); vec args_new; SymRef s_new; simp.simplify(get_sym_Real_DIV(), args, s_new, args_new); - // if (isRealDiv(s_new)) { - // assert((isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])); - // args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1])); - // return mkTimes(args_new); - // } if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])) { args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1])); return mkTimes(args_new); diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index 35023b6d1..ac9179320 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -8,16 +8,6 @@ #include 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 ArithDivisionByZeroException : public std::runtime_error { public: @@ -461,7 +451,6 @@ class ArithLogic : public Logic { SymRef sym_Int_GT; SymRef sym_Int_ITE; SymRef sym_Int_DISTINCT; - pair splitTerm(PTRef term) const; }; // Determine for two multiplicative terms (* k1 v1) and (* k2 v2), v1 != diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index 82e4c25cf..85f06522c 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -113,9 +113,7 @@ std::string Logic::disambiguateName(std::string const & protectedName, SRef sort assert(not protectedName.empty()); if (not isNullary or isInterpreted) { return protectedName; } - auto isQuoted = [](std::string const & s) { - return s.size() > 2 and * s.begin() == '|' and * (s.end() - 1) == '|'; - }; + auto isQuoted = [](std::string const & s) { return s.size() > 2 and *s.begin() == '|' and *(s.end() - 1) == '|'; }; auto name = isQuoted(protectedName) ? std::string_view(protectedName.data() + 1, protectedName.size() - 2) : std::string_view(protectedName); diff --git a/src/rewriters/DivModRewriter.h b/src/rewriters/DivModRewriter.h index 564cd88eb..2aa90038e 100644 --- a/src/rewriters/DivModRewriter.h +++ b/src/rewriters/DivModRewriter.h @@ -37,9 +37,6 @@ class DivModConfig : public DefaultRewriterConfig { PTRef rewritten = logic.isIntDiv(symRef) ? divVar : modVar; if (not inCache) { // collect the definitions to add - if (!logic.isConstant(divisor)) { - throw ApiException("Nonlinear expression in the SMT:" + logic.pp(term)); - } assert(logic.isConstant(divisor)); auto divisorVal = logic.getNumConst(divisor); assert(divisorVal.isInteger()); From b64f03b2b66d2bec97f316fff621ea36928c9f65 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Sun, 3 Nov 2024 10:30:17 +0100 Subject: [PATCH 05/20] NonlinWork: added PR-connected regression tests --- test/regression/base/arithmetic/miniexample.smt2 | 5 +++++ .../base/arithmetic/miniexample.smt2.expected.err | 0 .../base/arithmetic/miniexample.smt2.expected.out | 1 + test/regression/base/arithmetic/miniexample1.smt2 | 5 +++++ .../base/arithmetic/miniexample1.smt2.expected.err | 0 .../base/arithmetic/miniexample1.smt2.expected.out | 1 + test/regression/base/arithmetic/miniexample2.smt2 | 8 ++++++++ .../base/arithmetic/miniexample2.smt2.expected.err | 0 .../base/arithmetic/miniexample2.smt2.expected.out | 5 +++++ test/regression/base/arithmetic/miniexample3.smt2 | 9 +++++++++ .../base/arithmetic/miniexample3.smt2.expected.err | 0 .../base/arithmetic/miniexample3.smt2.expected.out | 9 +++++++++ test/regression/base/arithmetic/miniexample3_Ok.smt2 | 9 +++++++++ .../base/arithmetic/miniexample3_Ok.smt2.expected.err | 0 .../base/arithmetic/miniexample3_Ok.smt2.expected.out | 7 +++++++ test/regression/base/arithmetic/miniexample4.smt2 | 8 ++++++++ .../base/arithmetic/miniexample4.smt2.expected.err | 0 .../base/arithmetic/miniexample4.smt2.expected.out | 9 +++++++++ test/regression/base/arithmetic/miniexample4_Ok.smt2 | 8 ++++++++ .../base/arithmetic/miniexample4_Ok.smt2.expected.err | 0 .../base/arithmetic/miniexample4_Ok.smt2.expected.out | 7 +++++++ test/regression/base/arithmetic/miniexample5.smt2 | 7 +++++++ .../base/arithmetic/miniexample5.smt2.expected.err | 0 .../base/arithmetic/miniexample5.smt2.expected.out | 5 +++++ test/regression/base/arithmetic/miniexample6.smt2 | 7 +++++++ .../base/arithmetic/miniexample6.smt2.expected.err | 0 .../base/arithmetic/miniexample6.smt2.expected.out | 3 +++ test/regression/base/arithmetic/miniexample6_Ok.smt2 | 8 ++++++++ .../base/arithmetic/miniexample6_Ok.smt2.expected.err | 0 .../base/arithmetic/miniexample6_Ok.smt2.expected.out | 7 +++++++ test/regression/base/arithmetic/miniexample7.smt2 | 7 +++++++ .../base/arithmetic/miniexample7.smt2.expected.err | 0 .../base/arithmetic/miniexample7.smt2.expected.out | 3 +++ test/regression/base/arithmetic/miniexample7_Ok.smt2 | 7 +++++++ .../base/arithmetic/miniexample7_Ok.smt2.expected.err | 0 .../base/arithmetic/miniexample7_Ok.smt2.expected.out | 3 +++ test/regression/base/arithmetic/miniexample7_Ok1.smt2 | 8 ++++++++ .../base/arithmetic/miniexample7_Ok1.smt2.expected.err | 0 .../base/arithmetic/miniexample7_Ok1.smt2.expected.out | 7 +++++++ 39 files changed, 163 insertions(+) create mode 100644 test/regression/base/arithmetic/miniexample.smt2 create mode 100644 test/regression/base/arithmetic/miniexample.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample1.smt2 create mode 100644 test/regression/base/arithmetic/miniexample1.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample1.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample2.smt2 create mode 100644 test/regression/base/arithmetic/miniexample2.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample2.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample3.smt2 create mode 100644 test/regression/base/arithmetic/miniexample3.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample3.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample3_Ok.smt2 create mode 100644 test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample4.smt2 create mode 100644 test/regression/base/arithmetic/miniexample4.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample4.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample4_Ok.smt2 create mode 100644 test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample5.smt2 create mode 100644 test/regression/base/arithmetic/miniexample5.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample5.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample6.smt2 create mode 100644 test/regression/base/arithmetic/miniexample6.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample6.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample6_Ok.smt2 create mode 100644 test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample7.smt2 create mode 100644 test/regression/base/arithmetic/miniexample7.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample7.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample7_Ok.smt2 create mode 100644 test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample7_Ok1.smt2 create mode 100644 test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.out diff --git a/test/regression/base/arithmetic/miniexample.smt2 b/test/regression/base/arithmetic/miniexample.smt2 new file mode 100644 index 000000000..a5c6afc70 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_LIA) +(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b)) +(assert (= (uninterp_mul 1 2) 2)) +(check-sat) +(exit) diff --git a/test/regression/base/arithmetic/miniexample.smt2.expected.err b/test/regression/base/arithmetic/miniexample.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample.smt2.expected.out b/test/regression/base/arithmetic/miniexample.smt2.expected.out new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample.smt2.expected.out @@ -0,0 +1 @@ +sat diff --git a/test/regression/base/arithmetic/miniexample1.smt2 b/test/regression/base/arithmetic/miniexample1.smt2 new file mode 100644 index 000000000..15bd69389 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample1.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_LRA) +(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b)) +(assert (= (uninterp_div 1 2) 0.5)) +(check-sat) +(exit) diff --git a/test/regression/base/arithmetic/miniexample1.smt2.expected.err b/test/regression/base/arithmetic/miniexample1.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample1.smt2.expected.out b/test/regression/base/arithmetic/miniexample1.smt2.expected.out new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample1.smt2.expected.out @@ -0,0 +1 @@ +sat diff --git a/test/regression/base/arithmetic/miniexample2.smt2 b/test/regression/base/arithmetic/miniexample2.smt2 new file mode 100644 index 000000000..bd018eb56 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample2.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b)) +(assert (= x x)) +(assert (= (uninterp_mul 2 x) (+ x x))) +(check-sat) +(get-model) +(exit) \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample2.smt2.expected.err b/test/regression/base/arithmetic/miniexample2.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample2.smt2.expected.out b/test/regression/base/arithmetic/miniexample2.smt2.expected.out new file mode 100644 index 000000000..7db85b27c --- /dev/null +++ b/test/regression/base/arithmetic/miniexample2.smt2.expected.out @@ -0,0 +1,5 @@ +sat +( + (define-fun x () Int + 0) +) diff --git a/test/regression/base/arithmetic/miniexample3.smt2 b/test/regression/base/arithmetic/miniexample3.smt2 new file mode 100644 index 000000000..3a97106d0 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample3.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_LIA) +(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) +(get-model) +(exit) diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.err b/test/regression/base/arithmetic/miniexample3.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.out b/test/regression/base/arithmetic/miniexample3.smt2.expected.out new file mode 100644 index 000000000..be90b3315 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample3.smt2.expected.out @@ -0,0 +1,9 @@ +(error "Nonlinear operations in the formula: (* x y)") + +sat +( + (define-fun x () Int + 0) + (define-fun y () Int + 0) +) diff --git a/test/regression/base/arithmetic/miniexample3_Ok.smt2 b/test/regression/base/arithmetic/miniexample3_Ok.smt2 new file mode 100644 index 000000000..63242051f --- /dev/null +++ b/test/regression/base/arithmetic/miniexample3_Ok.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_LIA) +(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) +(exit) diff --git a/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.out new file mode 100644 index 000000000..af8095222 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample3_Ok.smt2.expected.out @@ -0,0 +1,7 @@ +sat +( + (define-fun x () Int + 0) + (define-fun y () Int + 4) +) diff --git a/test/regression/base/arithmetic/miniexample4.smt2 b/test/regression/base/arithmetic/miniexample4.smt2 new file mode 100644 index 000000000..3c485d0d2 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample4.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_LRA) +(declare-fun x () Real) +(declare-fun y () Real) +(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b)) +(assert (= (uninterp_div y x) 20)) +(check-sat) +(get-model) +(exit) diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.err b/test/regression/base/arithmetic/miniexample4.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.out b/test/regression/base/arithmetic/miniexample4.smt2.expected.out new file mode 100644 index 000000000..31cd2c1c6 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample4.smt2.expected.out @@ -0,0 +1,9 @@ +(error "Nonlinear operations in the formula: (/ y x)") + +sat +( + (define-fun x () Real + 0) + (define-fun y () Real + 0) +) diff --git a/test/regression/base/arithmetic/miniexample4_Ok.smt2 b/test/regression/base/arithmetic/miniexample4_Ok.smt2 new file mode 100644 index 000000000..83b26639b --- /dev/null +++ b/test/regression/base/arithmetic/miniexample4_Ok.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_LRA) +(declare-fun x () Real) +(declare-fun y () Real) +(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b)) +(assert (= (uninterp_div y 5) (+ 3 x))) +(check-sat) +(get-model) +(exit) diff --git a/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out new file mode 100644 index 000000000..e009558ce --- /dev/null +++ b/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out @@ -0,0 +1,7 @@ +sat +( + (define-fun x () Real + 0) + (define-fun y () Real + 15) +) diff --git a/test/regression/base/arithmetic/miniexample5.smt2 b/test/regression/base/arithmetic/miniexample5.smt2 new file mode 100644 index 000000000..f1fb44dc4 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample5.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (* a (+ b 5))) +(assert (= (uninterp_mul 2 x) (+ x 15))) +(check-sat) +(get-model) +(exit) \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample5.smt2.expected.err b/test/regression/base/arithmetic/miniexample5.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample5.smt2.expected.out b/test/regression/base/arithmetic/miniexample5.smt2.expected.out new file mode 100644 index 000000000..cccd2f94f --- /dev/null +++ b/test/regression/base/arithmetic/miniexample5.smt2.expected.out @@ -0,0 +1,5 @@ +sat +( + (define-fun x () Int + 5) +) diff --git a/test/regression/base/arithmetic/miniexample6.smt2 b/test/regression/base/arithmetic/miniexample6.smt2 new file mode 100644 index 000000000..57ec4e470 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample6.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b)) +(assert (= (uninterp_mul x y) 10)) +(check-sat) +(exit) diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.err b/test/regression/base/arithmetic/miniexample6.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.out b/test/regression/base/arithmetic/miniexample6.smt2.expected.out new file mode 100644 index 000000000..ed4d45660 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample6.smt2.expected.out @@ -0,0 +1,3 @@ +(error "Nonlinear operations in the formula: (* x y)") + +sat diff --git a/test/regression/base/arithmetic/miniexample6_Ok.smt2 b/test/regression/base/arithmetic/miniexample6_Ok.smt2 new file mode 100644 index 000000000..61cc3b630 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample6_Ok.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b)) +(assert (= (uninterp_mul x 10) y)) +(check-sat) +(get-model) +(exit) diff --git a/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.out new file mode 100644 index 000000000..ebf63a539 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample6_Ok.smt2.expected.out @@ -0,0 +1,7 @@ +sat +( + (define-fun x () Int + 0) + (define-fun y () Int + 0) +) diff --git a/test/regression/base/arithmetic/miniexample7.smt2 b/test/regression/base/arithmetic/miniexample7.smt2 new file mode 100644 index 000000000..989cc24de --- /dev/null +++ b/test/regression/base/arithmetic/miniexample7.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (div a b)) +(assert (= (uninterp_mul x y) 10)) +(check-sat) +(exit) diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.err b/test/regression/base/arithmetic/miniexample7.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.out b/test/regression/base/arithmetic/miniexample7.smt2.expected.out new file mode 100644 index 000000000..70209d4ff --- /dev/null +++ b/test/regression/base/arithmetic/miniexample7.smt2.expected.out @@ -0,0 +1,3 @@ +(error "Nonlinear operations in the formula: (div x y)") + +sat diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2 b/test/regression/base/arithmetic/miniexample7_Ok.smt2 new file mode 100644 index 000000000..68ffd95aa --- /dev/null +++ b/test/regression/base/arithmetic/miniexample7_Ok.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (div a b)) +(assert (= (uninterp_mul 10 y) x)) +(check-sat) +(exit) diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out new file mode 100644 index 000000000..22f155026 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out @@ -0,0 +1,3 @@ +(error "Nonlinear operations in the formula: (div 10 y)") + +sat diff --git a/test/regression/base/arithmetic/miniexample7_Ok1.smt2 b/test/regression/base/arithmetic/miniexample7_Ok1.smt2 new file mode 100644 index 000000000..36c908178 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample7_Ok1.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (div a b)) +(assert (= (uninterp_mul y 10) x)) +(check-sat) +(get-model) +(exit) diff --git a/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.err b/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.out b/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.out new file mode 100644 index 000000000..ebf63a539 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample7_Ok1.smt2.expected.out @@ -0,0 +1,7 @@ +sat +( + (define-fun x () Int + 0) + (define-fun y () Int + 0) +) From b617b20321c21b64062edd120420bdf07a276310 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Mon, 4 Nov 2024 11:05:12 +0100 Subject: [PATCH 06/20] NonlinWork: added support for mod --- src/logics/ArithLogic.cc | 12 ++++-------- test/regression/base/arithmetic/miniexample10.smt2 | 7 +++++++ .../base/arithmetic/miniexample10.smt2.expected.err | 0 .../base/arithmetic/miniexample10.smt2.expected.out | 5 +++++ test/regression/base/arithmetic/miniexample2.smt2 | 1 - test/regression/base/arithmetic/miniexample8.smt2 | 7 +++++++ .../base/arithmetic/miniexample8.smt2.expected.err | 0 .../base/arithmetic/miniexample8.smt2.expected.out | 3 +++ test/regression/base/arithmetic/miniexample8_Ok.smt2 | 5 +++++ .../arithmetic/miniexample8_Ok.smt2.expected.err | 0 .../arithmetic/miniexample8_Ok.smt2.expected.out | 1 + .../regression/base/arithmetic/miniexample8_Ok2.smt2 | 6 ++++++ .../arithmetic/miniexample8_Ok2.smt2.expected.err | 0 .../arithmetic/miniexample8_Ok2.smt2.expected.out | 1 + test/regression/base/arithmetic/miniexample9.smt2 | 6 ++++++ .../base/arithmetic/miniexample9.smt2.expected.err | 0 .../base/arithmetic/miniexample9.smt2.expected.out | 3 +++ test/unit/test_Rewriting.cc | 1 + 18 files changed, 49 insertions(+), 9 deletions(-) create mode 100644 test/regression/base/arithmetic/miniexample10.smt2 create mode 100644 test/regression/base/arithmetic/miniexample10.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample10.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample8.smt2 create mode 100644 test/regression/base/arithmetic/miniexample8.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample8.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample8_Ok.smt2 create mode 100644 test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample8_Ok2.smt2 create mode 100644 test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out create mode 100644 test/regression/base/arithmetic/miniexample9.smt2 create mode 100644 test/regression/base/arithmetic/miniexample9.smt2.expected.err create mode 100644 test/regression/base/arithmetic/miniexample9.smt2.expected.out diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 364fd41ee..76e98c728 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -196,11 +196,11 @@ bool ArithLogic::isLinearTerm(PTRef tr) const { bool ArithLogic::isNonlin(PTRef tr) const { if (isTimes(tr)) { Pterm const & term = getPterm(tr); - return (!isConstant(term[0]) && !isConstant(term[1])); + return (not isConstant(term[0]) && not isConstant(term[1])); } - if (isRealDiv(tr) || isIntDiv(tr)) { + if (isRealDiv(tr) || isIntDiv(tr) || isMod(getPterm(tr).symb())) { Pterm const & term = getPterm(tr); - return (!isConstant(term[1])); + return (not isConstant(term[1])); } return false; }; @@ -688,8 +688,6 @@ PTRef ArithLogic::mkTimes(vec && args) { SymRef s_new; simp.simplify(getTimesForSort(returnSort), flatten_args, s_new, args); PTRef tr = mkFun(s_new, std::move(args)); - // Either a real term or, if we constructed a multiplication of a - // constant and a sum, a real sum. return tr; } @@ -807,11 +805,9 @@ PTRef ArithLogic::mkMod(vec && args) { checkSortInt(args); PTRef dividend = args[0]; PTRef divisor = args[1]; - - if (not isNumConst(divisor)) { throw ApiException("Divisor must be constant in linear logic"); } if (isZero(divisor)) { throw ArithDivisionByZeroException(); } if (isOne(divisor) or isMinusOne(divisor)) { return getTerm_IntZero(); } - if (isConstant(dividend)) { + if (isConstant(dividend) && isConstant(divisor)) { auto const & dividendValue = getNumConst(dividend); auto const & divisorValue = getNumConst(divisor); assert(dividendValue.isInteger() and divisorValue.isInteger()); diff --git a/test/regression/base/arithmetic/miniexample10.smt2 b/test/regression/base/arithmetic/miniexample10.smt2 new file mode 100644 index 000000000..53394539e --- /dev/null +++ b/test/regression/base/arithmetic/miniexample10.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (* 2 a b)) +(assert (= (uninterp_mul 5 x) 10)) +(check-sat) +(get-model) +(exit) \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.err b/test/regression/base/arithmetic/miniexample10.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample10.smt2.expected.out b/test/regression/base/arithmetic/miniexample10.smt2.expected.out new file mode 100644 index 000000000..4863712af --- /dev/null +++ b/test/regression/base/arithmetic/miniexample10.smt2.expected.out @@ -0,0 +1,5 @@ +sat +( + (define-fun x () Int + 1) +) diff --git a/test/regression/base/arithmetic/miniexample2.smt2 b/test/regression/base/arithmetic/miniexample2.smt2 index bd018eb56..effcb8af6 100644 --- a/test/regression/base/arithmetic/miniexample2.smt2 +++ b/test/regression/base/arithmetic/miniexample2.smt2 @@ -1,7 +1,6 @@ (set-logic QF_LIA) (declare-fun x () Int) (define-fun uninterp_mul ((a Int) (b Int)) Int (* a b)) -(assert (= x x)) (assert (= (uninterp_mul 2 x) (+ x x))) (check-sat) (get-model) diff --git a/test/regression/base/arithmetic/miniexample8.smt2 b/test/regression/base/arithmetic/miniexample8.smt2 new file mode 100644 index 000000000..9a09e5260 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(declare-fun y () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b)) +(assert (= (uninterp_mul x y) 0)) +(check-sat) +(exit) \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.err b/test/regression/base/arithmetic/miniexample8.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.out b/test/regression/base/arithmetic/miniexample8.smt2.expected.out new file mode 100644 index 000000000..beab740be --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8.smt2.expected.out @@ -0,0 +1,3 @@ +(error "Nonlinear operations in the formula: (mod x y)") + +sat diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2 b/test/regression/base/arithmetic/miniexample8_Ok.smt2 new file mode 100644 index 000000000..8d277d485 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8_Ok.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_LIA) +(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b)) +(assert (= (uninterp_mul 1 2) 0)) +(check-sat) +(exit) \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8_Ok.smt2.expected.out @@ -0,0 +1 @@ +unsat diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2 b/test/regression/base/arithmetic/miniexample8_Ok2.smt2 new file mode 100644 index 000000000..741ce62af --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8_Ok2.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b)) +(assert (= (uninterp_mul x 5) 0)) +(check-sat) +(exit) \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample8_Ok2.smt2.expected.out @@ -0,0 +1 @@ +sat diff --git a/test/regression/base/arithmetic/miniexample9.smt2 b/test/regression/base/arithmetic/miniexample9.smt2 new file mode 100644 index 000000000..45c07977b --- /dev/null +++ b/test/regression/base/arithmetic/miniexample9.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_LIA) +(declare-fun x () Int) +(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b)) +(assert (= (uninterp_mul 5 x) 0)) +(check-sat) +(exit) \ No newline at end of file diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.err b/test/regression/base/arithmetic/miniexample9.smt2.expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.out b/test/regression/base/arithmetic/miniexample9.smt2.expected.out new file mode 100644 index 000000000..57d26b569 --- /dev/null +++ b/test/regression/base/arithmetic/miniexample9.smt2.expected.out @@ -0,0 +1,3 @@ +(error "Nonlinear operations in the formula: (mod 5 x)") + +sat diff --git a/test/unit/test_Rewriting.cc b/test/unit/test_Rewriting.cc index d4e883cc7..4f15b1d54 100644 --- a/test/unit/test_Rewriting.cc +++ b/test/unit/test_Rewriting.cc @@ -84,6 +84,7 @@ TEST(Rewriting_test, test_RewriteDivMod) { PTRef mod = logic.mkMod(x,two); PTRef fla = logic.mkAnd(logic.mkEq(div, two), logic.mkEq(mod, logic.getTerm_IntZero())); PTRef rewritten = rewriteDivMod(logic, fla); +// std::cout << logic.printTerm(rewritten) << std::endl; SMTConfig config; MainSolver solver(logic, config, "test"); solver.insertFormula(rewritten); From 2f49d4056c0bfe121dff91ec81288c1a0fab6073 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Tue, 5 Nov 2024 12:53:09 +0100 Subject: [PATCH 07/20] NonlinWork: moved and updated the Nonlin checks, tests rework, exception upd --- src/itehandler/IteToSwitch.cc | 6 ------ src/logics/ArithLogic.cc | 19 +++++++++++++++---- src/logics/ArithLogic.h | 2 +- src/logics/Logic.h | 1 - src/rewriters/DivModRewriter.h | 1 + src/tsolvers/lasolver/LASolver.cc | 9 ++++++--- src/tsolvers/lasolver/LASolver.h | 11 +++++++++++ .../arithmetic/miniexample3.smt2.expected.err | 3 +++ .../arithmetic/miniexample3.smt2.expected.out | 9 --------- .../arithmetic/miniexample4.smt2.expected.err | 3 +++ .../arithmetic/miniexample4.smt2.expected.out | 9 --------- .../arithmetic/miniexample6.smt2.expected.err | 3 +++ .../arithmetic/miniexample6.smt2.expected.out | 3 --- .../arithmetic/miniexample7.smt2.expected.err | 3 +++ .../arithmetic/miniexample7.smt2.expected.out | 3 --- .../miniexample7_Ok.smt2.expected.err | 3 +++ .../miniexample7_Ok.smt2.expected.out | 3 --- .../arithmetic/miniexample8.smt2.expected.err | 3 +++ .../arithmetic/miniexample8.smt2.expected.out | 3 --- .../arithmetic/miniexample9.smt2.expected.err | 3 +++ .../arithmetic/miniexample9.smt2.expected.out | 3 --- test/unit/test_ArithLogicApi.cc | 13 ++----------- test/unit/test_Ites.cc | 15 ++------------- test/unit/test_LRALogicMkTerms.cc | 11 ++--------- 24 files changed, 61 insertions(+), 81 deletions(-) diff --git a/src/itehandler/IteToSwitch.cc b/src/itehandler/IteToSwitch.cc index bf878695d..f082fd089 100644 --- a/src/itehandler/IteToSwitch.cc +++ b/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. diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 76e98c728..080b18632 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -194,13 +194,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; }; @@ -418,13 +430,12 @@ lbool ArithLogic::arithmeticElimination(vec 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); diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index ac9179320..7cc77de40 100644 --- a/src/logics/ArithLogic.h +++ b/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; } diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 809093c2f..9a144ee61 100644 --- a/src/logics/Logic.h +++ b/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()); } diff --git a/src/rewriters/DivModRewriter.h b/src/rewriters/DivModRewriter.h index 2aa90038e..e7c5f2495 100644 --- a/src/rewriters/DivModRewriter.h +++ b/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); diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 1d11eaea0..410766ed5 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/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 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); diff --git a/src/tsolvers/lasolver/LASolver.h b/src/tsolvers/lasolver/LASolver.h index eb09515b9..bad5a03fc 100644 --- a/src/tsolvers/lasolver/LASolver.h +++ b/src/tsolvers/lasolver/LASolver.h @@ -24,6 +24,17 @@ #include 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; diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.err b/test/regression/base/arithmetic/miniexample3.smt2.expected.err index e69de29bb..1d62dc3ea 100644 --- a/test/regression/base/arithmetic/miniexample3.smt2.expected.err +++ b/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 diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.out b/test/regression/base/arithmetic/miniexample3.smt2.expected.out index be90b3315..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample3.smt2.expected.out +++ b/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) -) diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.err b/test/regression/base/arithmetic/miniexample4.smt2.expected.err index e69de29bb..0d9258fce 100644 --- a/test/regression/base/arithmetic/miniexample4.smt2.expected.err +++ b/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 diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.out b/test/regression/base/arithmetic/miniexample4.smt2.expected.out index 31cd2c1c6..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample4.smt2.expected.out +++ b/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) -) diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.err b/test/regression/base/arithmetic/miniexample6.smt2.expected.err index e69de29bb..1d62dc3ea 100644 --- a/test/regression/base/arithmetic/miniexample6.smt2.expected.err +++ b/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 diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.out b/test/regression/base/arithmetic/miniexample6.smt2.expected.out index ed4d45660..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample6.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample6.smt2.expected.out @@ -1,3 +0,0 @@ -(error "Nonlinear operations in the formula: (* x y)") - -sat diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.err b/test/regression/base/arithmetic/miniexample7.smt2.expected.err index e69de29bb..e6fc63f27 100644 --- a/test/regression/base/arithmetic/miniexample7.smt2.expected.err +++ b/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 diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.out b/test/regression/base/arithmetic/miniexample7.smt2.expected.out index 70209d4ff..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample7.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample7.smt2.expected.out @@ -1,3 +0,0 @@ -(error "Nonlinear operations in the formula: (div x y)") - -sat diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err index e69de29bb..46aaf8321 100644 --- a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err +++ b/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 diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out index 22f155026..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out @@ -1,3 +0,0 @@ -(error "Nonlinear operations in the formula: (div 10 y)") - -sat diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.err b/test/regression/base/arithmetic/miniexample8.smt2.expected.err index e69de29bb..e43224680 100644 --- a/test/regression/base/arithmetic/miniexample8.smt2.expected.err +++ b/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 diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.out b/test/regression/base/arithmetic/miniexample8.smt2.expected.out index beab740be..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample8.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample8.smt2.expected.out @@ -1,3 +0,0 @@ -(error "Nonlinear operations in the formula: (mod x y)") - -sat diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.err b/test/regression/base/arithmetic/miniexample9.smt2.expected.err index e69de29bb..2caf3091e 100644 --- a/test/regression/base/arithmetic/miniexample9.smt2.expected.err +++ b/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 diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.out b/test/regression/base/arithmetic/miniexample9.smt2.expected.out index 57d26b569..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample9.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample9.smt2.expected.out @@ -1,3 +0,0 @@ -(error "Nonlinear operations in the formula: (mod 5 x)") - -sat diff --git a/test/unit/test_ArithLogicApi.cc b/test/unit/test_ArithLogicApi.cc index 3ee59273f..0ec854b7d 100644 --- a/test/unit/test_ArithLogicApi.cc +++ b/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 #include #include @@ -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); } diff --git a/test/unit/test_Ites.cc b/test/unit/test_Ites.cc index 03c8bd53c..0645c9aea 100644 --- a/test/unit/test_Ites.cc +++ b/test/unit/test_Ites.cc @@ -8,8 +8,6 @@ #include #include -#include "api/MainSolver.h" -#include "options/SMTConfig.h" #include 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) { diff --git a/test/unit/test_LRALogicMkTerms.cc b/test/unit/test_LRALogicMkTerms.cc index f447535ca..7a8bb6914 100644 --- a/test/unit/test_LRALogicMkTerms.cc +++ b/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 #include @@ -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) From 9bc9c8aee75c05501775edb7ca6e344e2dd78bf3 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Wed, 6 Nov 2024 14:53:40 +0100 Subject: [PATCH 08/20] NonlinWork: catching exceptions, few fixes --- src/api/MainSolver.cc | 7 ++++++- src/logics/ArithLogic.cc | 4 +++- test/regression/base/arithmetic/miniexample3.smt2 | 1 - .../base/arithmetic/miniexample3.smt2.expected.err | 3 --- .../base/arithmetic/miniexample3.smt2.expected.out | 2 ++ test/regression/base/arithmetic/miniexample4.smt2 | 1 - .../base/arithmetic/miniexample4.smt2.expected.err | 3 --- .../base/arithmetic/miniexample4.smt2.expected.out | 2 ++ .../base/arithmetic/miniexample6.smt2.expected.err | 3 --- .../base/arithmetic/miniexample6.smt2.expected.out | 2 ++ .../base/arithmetic/miniexample7.smt2.expected.err | 3 --- .../base/arithmetic/miniexample7.smt2.expected.out | 2 ++ .../base/arithmetic/miniexample7_Ok.smt2.expected.err | 3 --- .../base/arithmetic/miniexample7_Ok.smt2.expected.out | 2 ++ .../base/arithmetic/miniexample8.smt2.expected.err | 3 --- .../base/arithmetic/miniexample8.smt2.expected.out | 2 ++ .../base/arithmetic/miniexample9.smt2.expected.err | 3 --- .../base/arithmetic/miniexample9.smt2.expected.out | 2 ++ test/unit/test_LRALogicMkTerms.cc | 2 ++ 19 files changed, 25 insertions(+), 25 deletions(-) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 44b6bb28b..444125111 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -340,7 +340,12 @@ sstat MainSolver::check() { if (rval == s_Undef) { try { rval = solve(); - } catch (std::overflow_error const & error) { rval = s_Error; } + } catch (std::overflow_error const & error) { + rval = s_Error; + } catch (opensmt::LANonLinearException const & error) { + printf("%s\n", error.what()); + rval = s_Undef; + } if (rval == s_False) { assert(not smt_solver->isOK()); rememberUnsatFrame(smt_solver->getConflictFrame()); diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 080b18632..8ad1576ef 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -202,9 +202,11 @@ bool ArithLogic::isNonlin(PTRef tr) const { } if (isTimes(tr)) { Pterm const & term = getPterm(tr); + int vars = 0; if (not isConstant(term[0]) && not isConstant(term[1])) return true; for (auto subterm : term) { - if (isNonlin(subterm)) return true; + if (not isConstant(subterm)) vars++; + if (isNonlin(subterm) || vars > 1) return true; } } if (isRealDiv(tr) || isIntDiv(tr) || isMod(getPterm(tr).symb())) { diff --git a/test/regression/base/arithmetic/miniexample3.smt2 b/test/regression/base/arithmetic/miniexample3.smt2 index 3a97106d0..99f1ca183 100644 --- a/test/regression/base/arithmetic/miniexample3.smt2 +++ b/test/regression/base/arithmetic/miniexample3.smt2 @@ -5,5 +5,4 @@ (assert (= x x)) (assert (= (uninterp_mul y x) 30)) (check-sat) -(get-model) (exit) diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.err b/test/regression/base/arithmetic/miniexample3.smt2.expected.err index 1d62dc3ea..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample3.smt2.expected.err +++ b/test/regression/base/arithmetic/miniexample3.smt2.expected.err @@ -1,3 +0,0 @@ -terminate called after throwing an instance of 'opensmt::LANonLinearException' - what(): Term (* -1 (* x y)) is non-linear -Aborted diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.out b/test/regression/base/arithmetic/miniexample3.smt2.expected.out index e69de29bb..10f6c448b 100644 --- a/test/regression/base/arithmetic/miniexample3.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample3.smt2.expected.out @@ -0,0 +1,2 @@ +Term (* -1 (* x y)) is non-linear +unknown diff --git a/test/regression/base/arithmetic/miniexample4.smt2 b/test/regression/base/arithmetic/miniexample4.smt2 index 3c485d0d2..4f6320543 100644 --- a/test/regression/base/arithmetic/miniexample4.smt2 +++ b/test/regression/base/arithmetic/miniexample4.smt2 @@ -4,5 +4,4 @@ (define-fun uninterp_div ((a Real) (b Real)) Real (/ a b)) (assert (= (uninterp_div y x) 20)) (check-sat) -(get-model) (exit) diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.err b/test/regression/base/arithmetic/miniexample4.smt2.expected.err index 0d9258fce..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample4.smt2.expected.err +++ b/test/regression/base/arithmetic/miniexample4.smt2.expected.err @@ -1,3 +0,0 @@ -terminate called after throwing an instance of 'opensmt::LANonLinearException' - what(): Term (* -1 (/ y x)) is non-linear -Aborted diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.out b/test/regression/base/arithmetic/miniexample4.smt2.expected.out index e69de29bb..d5b30a85a 100644 --- a/test/regression/base/arithmetic/miniexample4.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample4.smt2.expected.out @@ -0,0 +1,2 @@ +Term (* -1 (/ y x)) is non-linear +unknown diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.err b/test/regression/base/arithmetic/miniexample6.smt2.expected.err index 1d62dc3ea..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample6.smt2.expected.err +++ b/test/regression/base/arithmetic/miniexample6.smt2.expected.err @@ -1,3 +0,0 @@ -terminate called after throwing an instance of 'opensmt::LANonLinearException' - what(): Term (* -1 (* x y)) is non-linear -Aborted diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.out b/test/regression/base/arithmetic/miniexample6.smt2.expected.out index e69de29bb..10f6c448b 100644 --- a/test/regression/base/arithmetic/miniexample6.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample6.smt2.expected.out @@ -0,0 +1,2 @@ +Term (* -1 (* x y)) is non-linear +unknown diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.err b/test/regression/base/arithmetic/miniexample7.smt2.expected.err index e6fc63f27..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample7.smt2.expected.err +++ b/test/regression/base/arithmetic/miniexample7.smt2.expected.err @@ -1,3 +0,0 @@ -terminate called after throwing an instance of 'opensmt::LANonLinearException' - what(): Term (* -1 (div x y)) is non-linear -Aborted diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.out b/test/regression/base/arithmetic/miniexample7.smt2.expected.out index e69de29bb..b3bf09830 100644 --- a/test/regression/base/arithmetic/miniexample7.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample7.smt2.expected.out @@ -0,0 +1,2 @@ +Term (* -1 (div x y)) is non-linear +unknown diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err index 46aaf8321..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err +++ b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.err @@ -1,3 +0,0 @@ -terminate called after throwing an instance of 'opensmt::LANonLinearException' - what(): Term (+ (div 10 y) (* -1 x)) is non-linear -Aborted diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out index e69de29bb..b887dc52f 100644 --- a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out @@ -0,0 +1,2 @@ +Term (+ (div 10 y) (* -1 x)) is non-linear +unknown diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.err b/test/regression/base/arithmetic/miniexample8.smt2.expected.err index e43224680..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample8.smt2.expected.err +++ b/test/regression/base/arithmetic/miniexample8.smt2.expected.err @@ -1,3 +0,0 @@ -terminate called after throwing an instance of 'opensmt::LANonLinearException' - what(): Term (mod x y) is non-linear -Aborted diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.out b/test/regression/base/arithmetic/miniexample8.smt2.expected.out index e69de29bb..6220dea8e 100644 --- a/test/regression/base/arithmetic/miniexample8.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample8.smt2.expected.out @@ -0,0 +1,2 @@ +Term (mod x y) is non-linear +unknown diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.err b/test/regression/base/arithmetic/miniexample9.smt2.expected.err index 2caf3091e..e69de29bb 100644 --- a/test/regression/base/arithmetic/miniexample9.smt2.expected.err +++ b/test/regression/base/arithmetic/miniexample9.smt2.expected.err @@ -1,3 +0,0 @@ -terminate called after throwing an instance of 'opensmt::LANonLinearException' - what(): Term (mod 5 x) is non-linear -Aborted diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.out b/test/regression/base/arithmetic/miniexample9.smt2.expected.out index e69de29bb..395f3d669 100644 --- a/test/regression/base/arithmetic/miniexample9.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample9.smt2.expected.out @@ -0,0 +1,2 @@ +Term (mod 5 x) is non-linear +unknown diff --git a/test/unit/test_LRALogicMkTerms.cc b/test/unit/test_LRALogicMkTerms.cc index 7a8bb6914..4d1d6d068 100644 --- a/test/unit/test_LRALogicMkTerms.cc +++ b/test/unit/test_LRALogicMkTerms.cc @@ -176,6 +176,8 @@ TEST_F(LRALogicMkTermsTest, test_SumToZero) TEST_F(LRALogicMkTermsTest, test_NoNonLinearException) { EXPECT_NO_THROW(logic.mkTimes(x,y)); + PTRef two = logic.mkConst("2"); + EXPECT_NO_THROW(logic.mkTimes(x,two)); } TEST_F(LRALogicMkTermsTest, test_ConstantSimplification) From 046a7b960b7ba31b60c39860b347997080c482e8 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 7 Nov 2024 15:17:32 +0100 Subject: [PATCH 09/20] NonlinWork: update to atomic Nonlin checks, propper checks in the LASolver, updated multiplication asserts --- src/logics/ArithLogic.cc | 23 ++++--------------- src/tsolvers/lasolver/LASolver.cc | 8 +++++++ .../arithmetic/miniexample3.smt2.expected.out | 2 +- .../arithmetic/miniexample4.smt2.expected.out | 2 +- .../arithmetic/miniexample6.smt2.expected.out | 2 +- .../arithmetic/miniexample7.smt2.expected.out | 2 +- .../miniexample7_Ok.smt2.expected.out | 2 +- 7 files changed, 17 insertions(+), 24 deletions(-) diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 8ad1576ef..18271a5a7 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -194,27 +194,13 @@ 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); - int vars = 0; - if (not isConstant(term[0]) && not isConstant(term[1])) return true; - for (auto subterm : term) { - if (not isConstant(subterm)) vars++; - if (isNonlin(subterm) || vars > 1) return true; - } + if (term.size() > 2 || (not isConstant(term[0]) && not isConstant(term[1]))) return true; } if (isRealDiv(tr) || isIntDiv(tr) || isMod(getPterm(tr).symb())) { Pterm const & term = getPterm(tr); if (not isConstant(term[1])) return true; - for (auto subterm : term) { - if (isNonlin(subterm)) return true; - } } return false; }; @@ -247,10 +233,10 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { pair ArithLogic::splitTermToVarAndConst(PTRef term) const { assert(isTimes(term) || isNumVarLike(term) || isConstant(term)); - if (isTimes(term)) { - assert(getPterm(term).size() == 2); + if (isTimes(term) && getPterm(term).size() == 2) { PTRef fac = getPterm(term)[0]; PTRef var = getPterm(term)[1]; + if (not isConstant(fac)) { std::swap(fac, var); } if (not isConstant(fac)) { std::swap(fac, var); if (not isConstant(fac)) { @@ -261,7 +247,7 @@ pair ArithLogic::splitTermToVarAndConst(PTRef term) const { assert(isConstant(fac)); assert(isNumVarLike(var) || isTimes(var)); return {var, fac}; - } else if (isNumVarLike(term)) { + } else if (isNumVarLike(term) || isTimes(term)) { assert(yieldsSortInt(term) or yieldsSortReal(term)); PTRef var = term; PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); @@ -560,7 +546,6 @@ PTRef ArithLogic::mkNeg(PTRef tr) { return tr_n; } if (isTimes(symref)) { // constant * var-like - assert(getPterm(tr).size() == 2); auto [var, constant] = splitTermToVarAndConst(tr); return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)}); } diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 410766ed5..89443dee3 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -290,6 +290,14 @@ LVRef LASolver::registerArithmeticTerm(PTRef expr) { if (logic.isNonlin(expr)) { auto termStr = logic.pp(expr); throw LANonLinearException(termStr.c_str()); + } else if(logic.isTimes(expr) || logic.isPlus(expr)) { + Pterm const & subterms = logic.getPterm(expr); + for(auto subterm: subterms) { + if (logic.isNonlin(subterm)) { + auto termStr = logic.pp(subterm); + throw LANonLinearException(termStr.c_str()); + } + } } LVRef x = LVRef::Undef; if (laVarMapper.hasVar(expr)){ diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.out b/test/regression/base/arithmetic/miniexample3.smt2.expected.out index 10f6c448b..c3d0674ed 100644 --- a/test/regression/base/arithmetic/miniexample3.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample3.smt2.expected.out @@ -1,2 +1,2 @@ -Term (* -1 (* x y)) is non-linear +Term (* x y) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.out b/test/regression/base/arithmetic/miniexample4.smt2.expected.out index d5b30a85a..04865578d 100644 --- a/test/regression/base/arithmetic/miniexample4.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample4.smt2.expected.out @@ -1,2 +1,2 @@ -Term (* -1 (/ y x)) is non-linear +Term (/ y x) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.out b/test/regression/base/arithmetic/miniexample6.smt2.expected.out index 10f6c448b..c3d0674ed 100644 --- a/test/regression/base/arithmetic/miniexample6.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample6.smt2.expected.out @@ -1,2 +1,2 @@ -Term (* -1 (* x y)) is non-linear +Term (* x y) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.out b/test/regression/base/arithmetic/miniexample7.smt2.expected.out index b3bf09830..b59c967d4 100644 --- a/test/regression/base/arithmetic/miniexample7.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample7.smt2.expected.out @@ -1,2 +1,2 @@ -Term (* -1 (div x y)) is non-linear +Term (div x y) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out index b887dc52f..85210c4b0 100644 --- a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out @@ -1,2 +1,2 @@ -Term (+ (div 10 y) (* -1 x)) is non-linear +Term (div 10 y) is non-linear unknown From fab2f0893212166f17770108dcd811d69ae8a9af Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Fri, 8 Nov 2024 09:54:59 +0100 Subject: [PATCH 10/20] NonlinWork: fix of the print in MainSolver --- src/api/MainSolver.cc | 2 +- src/api/MainSolver.h | 1 + test/regression/base/arithmetic/miniexample3.smt2.expected.out | 1 - test/regression/base/arithmetic/miniexample4.smt2.expected.out | 1 - test/regression/base/arithmetic/miniexample6.smt2.expected.out | 1 - test/regression/base/arithmetic/miniexample7.smt2.expected.out | 1 - .../base/arithmetic/miniexample7_Ok.smt2.expected.out | 1 - test/regression/base/arithmetic/miniexample8.smt2.expected.out | 1 - test/regression/base/arithmetic/miniexample9.smt2.expected.out | 1 - 9 files changed, 2 insertions(+), 8 deletions(-) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 444125111..6d1043df8 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -343,7 +343,7 @@ sstat MainSolver::check() { } catch (std::overflow_error const & error) { rval = s_Error; } catch (opensmt::LANonLinearException const & error) { - printf("%s\n", error.what()); + reasonUnknown = error.what(); rval = s_Undef; } if (rval == s_False) { diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index 01fc6ad37..088e21c09 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -310,6 +310,7 @@ class MainSolver { vec frameTerms; std::size_t firstNotSimplifiedFrame = 0; unsigned int insertedFormulasCount = 0; + std::string reasonUnknown; }; bool MainSolver::trackPartitions() const { diff --git a/test/regression/base/arithmetic/miniexample3.smt2.expected.out b/test/regression/base/arithmetic/miniexample3.smt2.expected.out index c3d0674ed..354664565 100644 --- a/test/regression/base/arithmetic/miniexample3.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample3.smt2.expected.out @@ -1,2 +1 @@ -Term (* x y) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.out b/test/regression/base/arithmetic/miniexample4.smt2.expected.out index 04865578d..354664565 100644 --- a/test/regression/base/arithmetic/miniexample4.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample4.smt2.expected.out @@ -1,2 +1 @@ -Term (/ y x) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample6.smt2.expected.out b/test/regression/base/arithmetic/miniexample6.smt2.expected.out index c3d0674ed..354664565 100644 --- a/test/regression/base/arithmetic/miniexample6.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample6.smt2.expected.out @@ -1,2 +1 @@ -Term (* x y) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample7.smt2.expected.out b/test/regression/base/arithmetic/miniexample7.smt2.expected.out index b59c967d4..354664565 100644 --- a/test/regression/base/arithmetic/miniexample7.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample7.smt2.expected.out @@ -1,2 +1 @@ -Term (div x y) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out index 85210c4b0..354664565 100644 --- a/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample7_Ok.smt2.expected.out @@ -1,2 +1 @@ -Term (div 10 y) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample8.smt2.expected.out b/test/regression/base/arithmetic/miniexample8.smt2.expected.out index 6220dea8e..354664565 100644 --- a/test/regression/base/arithmetic/miniexample8.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample8.smt2.expected.out @@ -1,2 +1 @@ -Term (mod x y) is non-linear unknown diff --git a/test/regression/base/arithmetic/miniexample9.smt2.expected.out b/test/regression/base/arithmetic/miniexample9.smt2.expected.out index 395f3d669..354664565 100644 --- a/test/regression/base/arithmetic/miniexample9.smt2.expected.out +++ b/test/regression/base/arithmetic/miniexample9.smt2.expected.out @@ -1,2 +1 @@ -Term (mod 5 x) is non-linear unknown From a236b36498d516ae51347da1aeae206990492d84 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Wed, 13 Nov 2024 16:05:00 +0100 Subject: [PATCH 11/20] NonlinWork: changed splitTerm --- src/logics/ArithLogic.cc | 62 ++++++++++++++++------------ src/logics/ArithLogic.h | 16 +++---- src/logics/Logic.cc | 2 +- src/logics/Logic.h | 2 +- src/simplifiers/LA.cc | 2 +- src/tsolvers/lasolver/LASolver.cc | 8 ++-- src/tsolvers/lasolver/LAVarMapper.cc | 2 +- 7 files changed, 51 insertions(+), 43 deletions(-) diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 18271a5a7..20a3923a5 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -211,7 +211,7 @@ Number const & ArithLogic::getNumConst(PTRef tr) const { return *numbers[id]; } -pair> ArithLogic::getConstantAndFactors(PTRef sum) const { +pair> ArithLogic::getConstantAndFactors(PTRef sum) { assert(isPlus(sum)); vec varFactors; PTRef constant = PTRef_Undef; @@ -231,23 +231,31 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { return {std::move(constantValue), std::move(varFactors)}; } -pair ArithLogic::splitTermToVarAndConst(PTRef term) const { +pair ArithLogic::splitPolyTerm(PTRef term) { assert(isTimes(term) || isNumVarLike(term) || isConstant(term)); - if (isTimes(term) && getPterm(term).size() == 2) { - PTRef fac = getPterm(term)[0]; - PTRef var = getPterm(term)[1]; - if (not isConstant(fac)) { std::swap(fac, var); } - if (not isConstant(fac)) { - std::swap(fac, var); - if (not isConstant(fac)) { - PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); - return {term, fac}; + if (isTimes(term)) { + PTRef fac = PTRef_Undef; + std::vector vars; + for (auto subterm : getPterm(term)) { + if (isConstant(subterm)) { + assert(fac == PTRef_Undef); + fac = subterm; + continue; } + vars.push_back(subterm); + } + assert(vars.size() > 0); + + if (fac == PTRef_Undef) { + PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); + return {term, fac}; } + auto returnSort = getSortRef(term); + PTRef var = vars.size() == 1 ? vars[0] : mkFun(getTimesForSort(returnSort), std::move(vars)); assert(isConstant(fac)); assert(isNumVarLike(var) || isTimes(var)); return {var, fac}; - } else if (isNumVarLike(term) || isTimes(term)) { + } else if (isNumVarLike(term)) { assert(yieldsSortInt(term) or yieldsSortReal(term)); PTRef var = term; PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); @@ -261,7 +269,7 @@ pair ArithLogic::splitTermToVarAndConst(PTRef term) const { // Normalize a product of the form (* a v) to either v or (* -1 v) PTRef ArithLogic::normalizeMul(PTRef mul) { assert(isTimes(mul)); - auto [v, c] = splitTermToVarAndConst(mul); + auto [v, c] = splitPolyTerm(mul); if (getNumConst(c) < 0) { return mkNeg(v); } else { @@ -419,13 +427,13 @@ lbool ArithLogic::arithmeticElimination(vec const & top_level_arith, Subs PTRef rhs = logic.getPterm(eq)[1]; PTRef polyTerm = lhs == logic.getZeroForSort(logic.getSortRef(lhs)) ? rhs : logic.mkMinus(rhs, lhs); if (logic.isLinearFactor(polyTerm)) { - auto [var, c] = logic.splitTermToVarAndConst(polyTerm); + auto [var, c] = logic.splitPolyTerm(polyTerm); auto coeff = logic.getNumConst(c); poly.addTerm(var, std::move(coeff)); } else { assert(logic.isPlus(polyTerm) || logic.isTimes(polyTerm)); for (PTRef factor : logic.getPterm(polyTerm)) { - auto [var, c] = logic.splitTermToVarAndConst(factor); + auto [var, c] = logic.splitPolyTerm(factor); auto coeff = logic.getNumConst(c); poly.addTerm(var, std::move(coeff)); } @@ -491,19 +499,19 @@ pair ArithLogic::retrieveSubstitutions(vec const return {res, std::move(resAndSubsts.second)}; } -uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) const { +uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) { assert(l.isTimes(tr)); - auto [v, c] = l.splitTermToVarAndConst(tr); + auto [v, c] = l.splitPolyTerm(tr); return v.x; } -bool LessThan_deepPTRef::operator()(PTRef x_, PTRef y_) const { +bool LessThan_deepPTRef::operator()(PTRef x_, PTRef y_) { uint32_t id_x = l.isTimes(x_) ? getVarIdFromProduct(x_) : x_.x; uint32_t id_y = l.isTimes(y_) ? getVarIdFromProduct(y_) : y_.x; return id_x < id_y; } -void ArithLogic::termSort(vec & v) const { +void ArithLogic::termSort(vec & v) { sort(v, LessThan_deepPTRef(*this)); } @@ -546,7 +554,7 @@ PTRef ArithLogic::mkNeg(PTRef tr) { return tr_n; } if (isTimes(symref)) { // constant * var-like - auto [var, constant] = splitTermToVarAndConst(tr); + auto [var, constant] = splitPolyTerm(tr); return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)}); } if (isNumVarLike(symref)) { @@ -619,7 +627,7 @@ PTRef ArithLogic::mkPlus(vec && args) { simplified.reserve(args.size()); for (PTRef arg : args) { - auto [v, c] = splitTermToVarAndConst(arg); + auto [v, c] = splitPolyTerm(arg); assert(c != PTRef_Undef); assert(isConstant(c)); if (not varIndices.has(v)) { @@ -787,7 +795,7 @@ PTRef ArithLogic::mkBinaryEq(PTRef lhs, PTRef rhs) { Number const & v = this->getNumConst(diff); return v.isZero() ? getTerm_true() : getTerm_false(); } else if (isNumVarLike(diff) || isTimes(diff)) { - auto [var, constant] = splitTermToVarAndConst(diff); + auto [var, constant] = splitPolyTerm(diff); return Logic::mkBinaryEq(getZeroForSort(eqSort), var); // Avoid anything that calls Logic::mkEq as this would create a loop } else if (isPlus(diff)) { @@ -1201,7 +1209,7 @@ pair ArithLogic::sumToNormalizedIntPair(PTRef sum) { std::vector coeffs; coeffs.reserve(varFactors.size()); for (PTRef factor : varFactors) { - auto [var, coeff] = splitTermToVarAndConst(factor); + auto [var, coeff] = splitPolyTerm(factor); assert((ArithLogic::isNumVarLike(var) || ArithLogic::isTimes(var)) and isNumConst(coeff)); vars.push(var); coeffs.push_back(getNumConst(coeff)); @@ -1279,7 +1287,7 @@ pair ArithLogic::sumToNormalizedRealPair(PTRef sum) { PTRef leadingFactor = varFactors[0]; // normalize the sum according to the leading factor - auto [var, coeff] = splitTermToVarAndConst(leadingFactor); + auto [var, coeff] = splitPolyTerm(leadingFactor); Number normalizationCoeff = abs(getNumConst(coeff)); // varFactors come from a normalized sum, no need to call normalization code again PTRef normalizedSum = varFactors.size() == 1 ? varFactors[0] : mkFun(get_sym_Real_PLUS(), std::move(varFactors)); @@ -1340,15 +1348,15 @@ std::pair ArithLogic::leqToConstantAndTerm(PTRef leq) { return std::make_pair(term[0], term[1]); } -bool ArithLogic::hasNegativeLeadingVariable(PTRef poly) const { +bool ArithLogic::hasNegativeLeadingVariable(PTRef poly) { if (isNumConst(poly) or isNumVarLike(poly)) { return false; } if (isTimes(poly)) { - auto [var, constant] = splitTermToVarAndConst(poly); + auto [var, constant] = splitPolyTerm(poly); return isNegative(getNumConst(constant)); } assert(isPlus(poly)); PTRef leadingTerm = getPterm(poly)[0]; - auto [var, constant] = splitTermToVarAndConst(leadingTerm); + auto [var, constant] = splitPolyTerm(leadingTerm); return isNegative(getNumConst(constant)); } } // namespace opensmt diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index 7cc77de40..8891e9b14 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -336,8 +336,8 @@ class ArithLogic : public Logic { bool isLinearTerm(PTRef tr) const; bool isLinearFactor(PTRef tr) const; - pair> getConstantAndFactors(PTRef sum) const; - pair splitTermToVarAndConst(PTRef term) const; + pair> getConstantAndFactors(PTRef sum); + pair splitPolyTerm(PTRef term); PTRef normalizeMul(PTRef mul); // Given a sum term 't' returns a normalized inequality 'c <= s' equivalent to '0 <= t' PTRef sumToNormalizedInequality(PTRef sum); @@ -345,7 +345,7 @@ class ArithLogic : public Logic { lbool arithmeticElimination(vec const & top_level_arith, SubstMap & substitutions); pair retrieveSubstitutions(vec const & facts) override; - void termSort(vec & v) const override; + void termSort(vec & v) override; PTRef removeAuxVars(PTRef) override; @@ -376,7 +376,7 @@ class ArithLogic : public Logic { pair sumToNormalizedIntPair(PTRef sum); pair sumToNormalizedRealPair(PTRef sum); - bool hasNegativeLeadingVariable(PTRef poly) const; + bool hasNegativeLeadingVariable(PTRef poly); std::vector numbers; @@ -464,13 +464,13 @@ class ArithLogic : public Logic { // (* ite1 ite2) => consider min(ite1.ptref, ite2.ptref) class LessThan_deepPTRef { public: - LessThan_deepPTRef(ArithLogic const & l) : l(l) {} + LessThan_deepPTRef(ArithLogic & l) : l(l) {} - bool operator()(PTRef x_, PTRef y_) const; + bool operator()(PTRef x_, PTRef y_); private: - ArithLogic const & l; - uint32_t getVarIdFromProduct(PTRef term) const; + ArithLogic & l; + uint32_t getVarIdFromProduct(PTRef term); }; } // namespace opensmt diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index 85f06522c..fd6fee2b5 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -1545,7 +1545,7 @@ SRef Logic::getArraySort(SRef domain, SRef codomain) { return getSort(sym_ArraySort, {domain, codomain}); } -void Logic::termSort(vec & v) const { +void Logic::termSort(vec & v) { sort(v, std::less{}); } diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 9a144ee61..d0091f50c 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -352,7 +352,7 @@ class Logic { std::string pp(PTRef tr) const; // A pretty printer std::string printSym(SymRef sr) const; - virtual void termSort(vec & v) const; // { sort(v, LessThan_PTRef()); } + virtual void termSort(vec & v); // { sort(v, LessThan_PTRef()); } void purify(PTRef r, PTRef & p, lbool & sgn) const; //{p = r; sgn = l_True; while (isNot(p)) { sgn = sgn^1; p = getPterm(p)[0]; }} diff --git a/src/simplifiers/LA.cc b/src/simplifiers/LA.cc index 682c64d61..ec1a51fa8 100644 --- a/src/simplifiers/LA.cc +++ b/src/simplifiers/LA.cc @@ -57,7 +57,7 @@ void LAExpression::initialize(PTRef e, bool do_canonize) { } else if (logic.isTimes(t)) { // If it is times, then one side must be constant, other // is enqueued with a new constant - auto [var, constant] = logic.splitTermToVarAndConst(t); + auto [var, constant] = logic.splitPolyTerm(t); Real new_c = logic.getNumConst(constant); new_c *= c; curr_term.emplace_back(var); diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 89443dee3..659987484 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -261,7 +261,7 @@ std::unique_ptr LASolver::expressionToLVarPoly(PTRef term) auto poly = std::make_unique(); bool negated = laVarMapper.isNegated(term); for (int i = 0; i < logic.getPterm(term).size(); i++) { - auto [v,c] = logic.splitTermToVarAndConst(logic.getPterm(term)[i]); + auto [v,c] = logic.splitPolyTerm(logic.getPterm(term)[i]); LVRef var = getLAVar_single(v); Real coeff = getNum(c); if (negated) { @@ -309,7 +309,7 @@ LVRef LASolver::registerArithmeticTerm(PTRef expr) { if (logic.isNumVar(expr) || logic.isTimes(expr)) { // Case (1), (2a), and (2b) - auto [v,c] = logic.splitTermToVarAndConst(expr); + auto [v,c] = logic.splitPolyTerm(expr); assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v)))); x = getLAVar_single(v); simplex.newNonbasicVar(x); @@ -858,7 +858,7 @@ std::pair> linearSystemFromConstraints(std PTRef poly = defConstraint.lhs; fillTerms(poly, terms); for (PTRef arg : terms) { - auto [var, constant] = logic.splitTermToVarAndConst(arg); + auto [var, constant] = logic.splitPolyTerm(arg); assert(var != PTRef_Undef); if (varIndices.find(var) == varIndices.end()) { varIndices.insert({var, columns++}); @@ -877,7 +877,7 @@ std::pair> linearSystemFromConstraints(std PTRef poly = constraints[row].lhs; fillTerms(poly, terms); for (PTRef arg : terms) { - auto [var, constant] = logic.splitTermToVarAndConst(arg); + auto [var, constant] = logic.splitPolyTerm(arg); auto col = varIndices[var]; columnPolynomials[col].addTerm(IndexType{row}, logic.getNumConst(constant)); } diff --git a/src/tsolvers/lasolver/LAVarMapper.cc b/src/tsolvers/lasolver/LAVarMapper.cc index bcf3d95c5..e2f5fcde1 100644 --- a/src/tsolvers/lasolver/LAVarMapper.cc +++ b/src/tsolvers/lasolver/LAVarMapper.cc @@ -58,7 +58,7 @@ bool LAVarMapper::isNegated(PTRef tr) const { return false; // Case (1a) if (logic.isTimes(tr)) { // Cases (2) - auto [v,c] = logic.splitTermToVarAndConst(tr); + auto [v,c] = logic.splitPolyTerm(tr); return isNegated(c); } if (logic.isIte(tr)) { From 2eedd001f24b90f64ef7ca1f3977542241261eba Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 14 Nov 2024 16:15:53 +0100 Subject: [PATCH 12/20] NonlinWork: changes in multiplication handling --- src/logics/ArithLogic.cc | 84 ++++++++++++++++++++++++++-------------- src/logics/ArithLogic.h | 33 +++++++++++----- src/logics/Logic.cc | 2 +- src/logics/Logic.h | 2 +- 4 files changed, 82 insertions(+), 39 deletions(-) diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 20a3923a5..e090e9a3f 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -75,6 +75,7 @@ std::string const ArithLogic::tk_int_neg = "-"; std::string const ArithLogic::tk_int_minus = "-"; std::string const ArithLogic::tk_int_plus = "+"; std::string const ArithLogic::tk_int_times = "*"; +std::string const ArithLogic::tk_int_times_nonlin = "mul"; std::string const ArithLogic::tk_int_div = "div"; std::string const ArithLogic::tk_int_mod = "mod"; std::string const ArithLogic::tk_int_lt = "<"; @@ -90,6 +91,7 @@ std::string const ArithLogic::tk_real_neg = "-"; std::string const ArithLogic::tk_real_minus = "-"; std::string const ArithLogic::tk_real_plus = "+"; std::string const ArithLogic::tk_real_times = "*"; +std::string const ArithLogic::tk_real_times_nonlin = "mul"; std::string const ArithLogic::tk_real_div = "/"; std::string const ArithLogic::tk_real_lt = "<"; std::string const ArithLogic::tk_real_leq = "<="; @@ -114,6 +116,8 @@ ArithLogic::ArithLogic(Logic_t type) sym_Real_MINUS(declareFun_NoScoping_LeftAssoc(tk_real_minus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_plus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), + sym_Real_TIMES_NONLIN( + declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times_nonlin, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_DIV(declareFun_NoScoping_LeftAssoc(tk_real_div, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_EQ(sortToEquality[sort_REAL]), sym_Real_LEQ(declareFun_NoScoping_Chainable(tk_real_leq, sort_BOOL, {sort_REAL, sort_REAL})), @@ -134,6 +138,8 @@ ArithLogic::ArithLogic(Logic_t type) sym_Int_MINUS(declareFun_NoScoping_LeftAssoc(tk_int_minus, sort_INT, {sort_INT, sort_INT})), sym_Int_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_plus, sort_INT, {sort_INT, sort_INT})), sym_Int_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})), + sym_Int_TIMES_NONLIN( + declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times_nonlin, sort_INT, {sort_INT, sort_INT})), sym_Int_DIV(declareFun_NoScoping_LeftAssoc(tk_int_div, sort_INT, {sort_INT, sort_INT})), sym_Int_MOD(declareFun_NoScoping(tk_int_mod, sort_INT, {sort_INT, sort_INT})), sym_Int_EQ(sortToEquality[sort_INT]), @@ -154,6 +160,11 @@ SymRef ArithLogic::getTimesForSort(SRef sort) const { return sort == getSort_int() ? get_sym_Int_TIMES() : get_sym_Real_TIMES(); } +SymRef ArithLogic::getTimesNonlinForSort(SRef sort) const { + assert(sort == getSort_int() or sort == getSort_real()); + return sort == getSort_int() ? get_sym_Int_TIMES_NONLIN() : get_sym_Real_TIMES_NONLIN(); +} + SymRef ArithLogic::getMinusForSort(SRef sort) const { assert(sort == getSort_int() or sort == getSort_real()); return sort == getSort_int() ? get_sym_Int_MINUS() : get_sym_Real_MINUS(); @@ -211,7 +222,7 @@ Number const & ArithLogic::getNumConst(PTRef tr) const { return *numbers[id]; } -pair> ArithLogic::getConstantAndFactors(PTRef sum) { +pair> ArithLogic::getConstantAndFactors(PTRef sum) const { assert(isPlus(sum)); vec varFactors; PTRef constant = PTRef_Undef; @@ -231,30 +242,19 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) { return {std::move(constantValue), std::move(varFactors)}; } -pair ArithLogic::splitPolyTerm(PTRef term) { +pair ArithLogic::splitPolyTerm(PTRef term) const { assert(isTimes(term) || isNumVarLike(term) || isConstant(term)); - if (isTimes(term)) { - PTRef fac = PTRef_Undef; - std::vector vars; - for (auto subterm : getPterm(term)) { - if (isConstant(subterm)) { - assert(fac == PTRef_Undef); - fac = subterm; - continue; - } - vars.push_back(subterm); - } - assert(vars.size() > 0); - - if (fac == PTRef_Undef) { - PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); - return {term, fac}; - } - auto returnSort = getSortRef(term); - PTRef var = vars.size() == 1 ? vars[0] : mkFun(getTimesForSort(returnSort), std::move(vars)); + if (isTimesLin(term)) { + assert(getPterm(term).size() == 2); + PTRef fac = getPterm(term)[0]; + PTRef var = getPterm(term)[1]; + if (not isConstant(fac)) { std::swap(fac, var); } assert(isConstant(fac)); - assert(isNumVarLike(var) || isTimes(var)); + assert(isNumVarLike(var) || isTimesNonlin(var)); return {var, fac}; + } else if (isTimesNonlin(term)) { + PTRef one = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); + return {term, one}; } else if (isNumVarLike(term)) { assert(yieldsSortInt(term) or yieldsSortReal(term)); PTRef var = term; @@ -499,19 +499,19 @@ pair ArithLogic::retrieveSubstitutions(vec const return {res, std::move(resAndSubsts.second)}; } -uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) { +uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) const { assert(l.isTimes(tr)); auto [v, c] = l.splitPolyTerm(tr); return v.x; } -bool LessThan_deepPTRef::operator()(PTRef x_, PTRef y_) { +bool LessThan_deepPTRef::operator()(PTRef x_, PTRef y_) const { uint32_t id_x = l.isTimes(x_) ? getVarIdFromProduct(x_) : x_.x; uint32_t id_y = l.isTimes(y_) ? getVarIdFromProduct(y_) : y_.x; return id_x < id_y; } -void ArithLogic::termSort(vec & v) { +void ArithLogic::termSort(vec & v) const { sort(v, LessThan_deepPTRef(*this)); } @@ -553,10 +553,15 @@ PTRef ArithLogic::mkNeg(PTRef tr) { PTRef tr_n = mkFun(symref, std::move(args)); return tr_n; } - if (isTimes(symref)) { // constant * var-like + if (isTimesLin(symref)) { // constant * (var-like \/ times-nonlin) + assert(getPterm(tr).size() == 2); auto [var, constant] = splitPolyTerm(tr); return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)}); } + if (isTimesNonlin(symref)) { + SRef returnSort = getSortRef(tr); + return mkFun(getTimesForSort(returnSort), {tr, getMinusOneForSort(returnSort)}); + } if (isNumVarLike(symref)) { auto sortRef = getSortRef(symref); return mkFun(getTimesForSort(sortRef), {tr, getMinusOneForSort(sortRef)}); @@ -693,7 +698,30 @@ PTRef ArithLogic::mkTimes(vec && args) { args.clear(); SymRef s_new; simp.simplify(getTimesForSort(returnSort), flatten_args, s_new, args); - PTRef tr = mkFun(s_new, std::move(args)); + if (!isTimes(s_new)) return mkFun(s_new, std::move(args)); + PTRef coef = PTRef_Undef; + std::vector vars; + // return mkFun(s_new, std::move(args)); + // Splitting Multiplication into constant and variable subterms + for (int i = 0; i < args.size(); i++) { + if (isConstant(args[i])) { + assert(coef == PTRef_Undef); + coef = args[i]; + continue; + } + vars.push_back(args[i]); + } + assert(!vars.empty()); + PTRef tr; + if (vars.size() > 1) { + if (coef == PTRef_Undef) { + tr = mkFun(getTimesNonlinForSort(returnSort), vars); + } else { + tr = mkFun(s_new, {coef, mkFun(getTimesNonlinForSort(returnSort), vars)}); + } + } else { + tr = mkFun(s_new, {coef, vars[0]}); + } return tr; } @@ -1348,7 +1376,7 @@ std::pair ArithLogic::leqToConstantAndTerm(PTRef leq) { return std::make_pair(term[0], term[1]); } -bool ArithLogic::hasNegativeLeadingVariable(PTRef poly) { +bool ArithLogic::hasNegativeLeadingVariable(PTRef poly) const { if (isNumConst(poly) or isNumVarLike(poly)) { return false; } if (isTimes(poly)) { auto [var, constant] = splitPolyTerm(poly); diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index 8891e9b14..e9e0e260d 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -95,6 +95,8 @@ class ArithLogic : public Logic { SymRef get_sym_Int_TIMES() const { return sym_Int_TIMES; } SymRef get_sym_Real_TIMES() const { return sym_Real_TIMES; } + SymRef get_sym_Int_TIMES_NONLIN() const { return sym_Int_TIMES_NONLIN; } + SymRef get_sym_Real_TIMES_NONLIN() const { return sym_Real_TIMES_NONLIN; } SymRef get_sym_Int_DIV() const { return sym_Int_DIV; } SymRef get_sym_Int_MOD() const { return sym_Int_MOD; } SymRef get_sym_Real_DIV() const { return sym_Real_DIV; } @@ -160,12 +162,20 @@ class ArithLogic : public Logic { bool isIntNeg(SymRef sr) const { return sr == sym_Int_NEG; } bool isRealNeg(SymRef sr) const { return sr == sym_Real_NEG; } - bool isTimes(SymRef sr) const { return isIntTimes(sr) or isRealTimes(sr); } + bool isTimes(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr); }; + bool isTimesLin(SymRef sr) const { return isIntTimes(sr) or isRealTimes(sr); } + bool isTimesNonlin(SymRef sr) const { return isIntTimesNonlin(sr) or isRealTimesNonlin(sr); } bool isTimes(PTRef tr) const { return isTimes(getPterm(tr).symb()); } + bool isTimesLin(PTRef tr) const { return isTimesLin(getPterm(tr).symb()); } + bool isTimesNonlin(PTRef tr) const { return isTimesNonlin(getPterm(tr).symb()); } bool isIntTimes(PTRef tr) const { return isIntTimes(getPterm(tr).symb()); } + bool isIntTimesNonlin(PTRef tr) const { return isIntTimesNonlin(getPterm(tr).symb()); } bool isRealTimes(PTRef tr) const { return isRealTimes(getPterm(tr).symb()); } + bool isRealTimesNonlin(PTRef tr) const { return isRealTimesNonlin(getPterm(tr).symb()); } bool isIntTimes(SymRef sr) const { return sr == sym_Int_TIMES; } + bool isIntTimesNonlin(SymRef sr) const { return sr == sym_Int_TIMES_NONLIN; } bool isRealTimes(SymRef sr) const { return sr == sym_Real_TIMES; } + bool isRealTimesNonlin(SymRef sr) const { return sr == sym_Real_TIMES_NONLIN; } bool isRealDiv(PTRef tr) const { return isRealDiv(getPterm(tr).symb()); } bool isRealDiv(SymRef sr) const { return sr == sym_Real_DIV; } @@ -259,6 +269,7 @@ class ArithLogic : public Logic { SymRef getPlusForSort(SRef sort) const; SymRef getTimesForSort(SRef sort) const; + SymRef getTimesNonlinForSort(SRef sort) const; SymRef getMinusForSort(SRef sort) const; PTRef getZeroForSort(SRef sort) const; @@ -336,8 +347,8 @@ class ArithLogic : public Logic { bool isLinearTerm(PTRef tr) const; bool isLinearFactor(PTRef tr) const; - pair> getConstantAndFactors(PTRef sum); - pair splitPolyTerm(PTRef term); + pair> getConstantAndFactors(PTRef sum) const; + pair splitPolyTerm(PTRef term) const; PTRef normalizeMul(PTRef mul); // Given a sum term 't' returns a normalized inequality 'c <= s' equivalent to '0 <= t' PTRef sumToNormalizedInequality(PTRef sum); @@ -345,7 +356,7 @@ class ArithLogic : public Logic { lbool arithmeticElimination(vec const & top_level_arith, SubstMap & substitutions); pair retrieveSubstitutions(vec const & facts) override; - void termSort(vec & v) override; + void termSort(vec & v) const override; PTRef removeAuxVars(PTRef) override; @@ -376,7 +387,7 @@ class ArithLogic : public Logic { pair sumToNormalizedIntPair(PTRef sum); pair sumToNormalizedRealPair(PTRef sum); - bool hasNegativeLeadingVariable(PTRef poly); + bool hasNegativeLeadingVariable(PTRef poly) const; std::vector numbers; @@ -396,6 +407,8 @@ class ArithLogic : public Logic { static std::string const tk_int_plus; static std::string const tk_real_times; static std::string const tk_int_times; + static std::string const tk_real_times_nonlin; + static std::string const tk_int_times_nonlin; static std::string const tk_real_div; static std::string const tk_int_div; static std::string const tk_int_mod; @@ -422,6 +435,7 @@ class ArithLogic : public Logic { SymRef sym_Real_MINUS; SymRef sym_Real_PLUS; SymRef sym_Real_TIMES; + SymRef sym_Real_TIMES_NONLIN; SymRef sym_Real_DIV; SymRef sym_Real_EQ; SymRef sym_Real_LEQ; @@ -442,6 +456,7 @@ class ArithLogic : public Logic { SymRef sym_Int_MINUS; SymRef sym_Int_PLUS; SymRef sym_Int_TIMES; + SymRef sym_Int_TIMES_NONLIN; SymRef sym_Int_DIV; SymRef sym_Int_MOD; SymRef sym_Int_EQ; @@ -464,13 +479,13 @@ class ArithLogic : public Logic { // (* ite1 ite2) => consider min(ite1.ptref, ite2.ptref) class LessThan_deepPTRef { public: - LessThan_deepPTRef(ArithLogic & l) : l(l) {} + LessThan_deepPTRef(ArithLogic const & l) : l(l) {} - bool operator()(PTRef x_, PTRef y_); + bool operator()(PTRef x_, PTRef y_) const; private: - ArithLogic & l; - uint32_t getVarIdFromProduct(PTRef term); + ArithLogic const & l; + uint32_t getVarIdFromProduct(PTRef term) const; }; } // namespace opensmt diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index fd6fee2b5..85f06522c 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -1545,7 +1545,7 @@ SRef Logic::getArraySort(SRef domain, SRef codomain) { return getSort(sym_ArraySort, {domain, codomain}); } -void Logic::termSort(vec & v) { +void Logic::termSort(vec & v) const { sort(v, std::less{}); } diff --git a/src/logics/Logic.h b/src/logics/Logic.h index d0091f50c..9a144ee61 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -352,7 +352,7 @@ class Logic { std::string pp(PTRef tr) const; // A pretty printer std::string printSym(SymRef sr) const; - virtual void termSort(vec & v); // { sort(v, LessThan_PTRef()); } + virtual void termSort(vec & v) const; // { sort(v, LessThan_PTRef()); } void purify(PTRef r, PTRef & p, lbool & sgn) const; //{p = r; sgn = l_True; while (isNot(p)) { sgn = sgn^1; p = getPterm(p)[0]; }} From 8ff3d598fb8170303e67ae63e1bc151620779530 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Mon, 18 Nov 2024 11:38:08 +0100 Subject: [PATCH 13/20] NonlinWork: single symbol for multiplication --- src/logics/ArithLogic.cc | 7 ++----- src/logics/ArithLogic.h | 2 -- src/pterms/PtStore.cc | 6 ++++-- src/symbols/SymStore.cc | 4 +++- 4 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index e090e9a3f..43a19c201 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -75,7 +75,6 @@ std::string const ArithLogic::tk_int_neg = "-"; std::string const ArithLogic::tk_int_minus = "-"; std::string const ArithLogic::tk_int_plus = "+"; std::string const ArithLogic::tk_int_times = "*"; -std::string const ArithLogic::tk_int_times_nonlin = "mul"; std::string const ArithLogic::tk_int_div = "div"; std::string const ArithLogic::tk_int_mod = "mod"; std::string const ArithLogic::tk_int_lt = "<"; @@ -91,7 +90,6 @@ std::string const ArithLogic::tk_real_neg = "-"; std::string const ArithLogic::tk_real_minus = "-"; std::string const ArithLogic::tk_real_plus = "+"; std::string const ArithLogic::tk_real_times = "*"; -std::string const ArithLogic::tk_real_times_nonlin = "mul"; std::string const ArithLogic::tk_real_div = "/"; std::string const ArithLogic::tk_real_lt = "<"; std::string const ArithLogic::tk_real_leq = "<="; @@ -117,7 +115,7 @@ ArithLogic::ArithLogic(Logic_t type) sym_Real_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_plus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_TIMES_NONLIN( - declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times_nonlin, sort_REAL, {sort_REAL, sort_REAL})), + declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_DIV(declareFun_NoScoping_LeftAssoc(tk_real_div, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_EQ(sortToEquality[sort_REAL]), sym_Real_LEQ(declareFun_NoScoping_Chainable(tk_real_leq, sort_BOOL, {sort_REAL, sort_REAL})), @@ -138,8 +136,7 @@ ArithLogic::ArithLogic(Logic_t type) sym_Int_MINUS(declareFun_NoScoping_LeftAssoc(tk_int_minus, sort_INT, {sort_INT, sort_INT})), sym_Int_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_plus, sort_INT, {sort_INT, sort_INT})), sym_Int_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})), - sym_Int_TIMES_NONLIN( - declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times_nonlin, sort_INT, {sort_INT, sort_INT})), + sym_Int_TIMES_NONLIN(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})), sym_Int_DIV(declareFun_NoScoping_LeftAssoc(tk_int_div, sort_INT, {sort_INT, sort_INT})), sym_Int_MOD(declareFun_NoScoping(tk_int_mod, sort_INT, {sort_INT, sort_INT})), sym_Int_EQ(sortToEquality[sort_INT]), diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index e9e0e260d..9e2382fe3 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -407,8 +407,6 @@ class ArithLogic : public Logic { static std::string const tk_int_plus; static std::string const tk_real_times; static std::string const tk_int_times; - static std::string const tk_real_times_nonlin; - static std::string const tk_int_times_nonlin; static std::string const tk_real_div; static std::string const tk_int_div; static std::string const tk_int_mod; diff --git a/src/pterms/PtStore.cc b/src/pterms/PtStore.cc index 6c28226ae..f2700787c 100644 --- a/src/pterms/PtStore.cc +++ b/src/pterms/PtStore.cc @@ -29,7 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include #include -#include +#include namespace opensmt { int const PtStore::ptstore_vec_idx = 1; @@ -153,8 +153,10 @@ SymRef PtStore::lookupSymbol(char const * s, vec const & args, SymbolMatc } else { return candidates[0]; } + } else if (strcmp(s, "*") == 0) { + assert(candidates.size() == 2); + return candidates[0]; } - assert(candidates.size() > 1); if (sort == SRef_Undef) { throw ApiException("Ambiguous symbol: `" + std::string(s) + "'"); } diff --git a/src/symbols/SymStore.cc b/src/symbols/SymStore.cc index 66cfa6051..49c5cd965 100644 --- a/src/symbols/SymStore.cc +++ b/src/symbols/SymStore.cc @@ -50,7 +50,9 @@ SymRef SymStore::newSymb(char const * fname, SRef rsort, vec const & args, if (symbol.rsort() == rsort and symbol.nargs() == args.size_() and symbol.commutes() == symConfig.commutes and symbol.noScoping() == symConfig.noScoping and symbol.isInterpreted() == symConfig.isInterpreted) { - if (std::equal(symbol.begin(), symbol.end(), args.begin())) { return symref; } + if (std::equal(symbol.begin(), symbol.end(), args.begin()) && (strcmp(fname, "*") != 0)) { + return symref; + } } } } From d8ecbb6ec6944e117e1fef369131b98fc7c36cc3 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Tue, 19 Nov 2024 10:52:48 +0100 Subject: [PATCH 14/20] NonlinWork: duplicate symbol creation --- src/logics/ArithLogic.cc | 5 +++-- src/logics/Logic.cc | 4 ++-- src/logics/Logic.h | 8 +++++--- src/symbols/SymStore.cc | 9 ++++----- src/symbols/SymStore.h | 3 ++- 5 files changed, 16 insertions(+), 13 deletions(-) diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 43a19c201..0452dd550 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -115,7 +115,7 @@ ArithLogic::ArithLogic(Logic_t type) sym_Real_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_plus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_TIMES_NONLIN( - declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), + declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL}, true)), sym_Real_DIV(declareFun_NoScoping_LeftAssoc(tk_real_div, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_EQ(sortToEquality[sort_REAL]), sym_Real_LEQ(declareFun_NoScoping_Chainable(tk_real_leq, sort_BOOL, {sort_REAL, sort_REAL})), @@ -136,7 +136,8 @@ ArithLogic::ArithLogic(Logic_t type) sym_Int_MINUS(declareFun_NoScoping_LeftAssoc(tk_int_minus, sort_INT, {sort_INT, sort_INT})), sym_Int_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_plus, sort_INT, {sort_INT, sort_INT})), sym_Int_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})), - sym_Int_TIMES_NONLIN(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})), + sym_Int_TIMES_NONLIN( + declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT}, true)), sym_Int_DIV(declareFun_NoScoping_LeftAssoc(tk_int_div, sort_INT, {sort_INT, sort_INT})), sym_Int_MOD(declareFun_NoScoping(tk_int_mod, sort_INT, {sort_INT, sort_INT})), sym_Int_EQ(sortToEquality[sort_INT]), diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index 85f06522c..487735e11 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -728,11 +728,11 @@ PTRef Logic::mkSelect(vec && args) { } SymRef Logic::declareFun(std::string const & fname, SRef rsort, vec const & args, - SymbolConfig const & symbolConfig) { + SymbolConfig const & symbolConfig, bool duplicate) { assert(rsort != SRef_Undef); assert(std::find(args.begin(), args.end(), SRef_Undef) == args.end()); - SymRef sr = sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig); + SymRef sr = sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig, duplicate); return sr; } diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 9a144ee61..a98bb69b1 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -164,7 +164,8 @@ class Logic { virtual PTRef mkConst(char const *); virtual PTRef mkConst(SRef, char const *); - SymRef declareFun(std::string const & fname, SRef rsort, vec const & args, SymbolConfig const & symbolConfig); + SymRef declareFun(std::string const & fname, SRef rsort, vec const & args, SymbolConfig const & symbolConfig, + bool duplicate = false); SymRef declareFun(std::string const & fname, SRef rsort, vec const & args) { return declareFun(fname, rsort, args, SymConf::Default); } @@ -183,8 +184,9 @@ class Logic { SymRef declareFun_NoScoping_Pairwise(std::string const & s, SRef rsort, vec const & args) { return declareFun(s, rsort, args, SymConf::NoScopingPairwise); } - SymRef declareFun_Commutative_NoScoping_LeftAssoc(std::string const & s, SRef rsort, vec const & args) { - return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc); + SymRef declareFun_Commutative_NoScoping_LeftAssoc(std::string const & s, SRef rsort, vec const & args, + bool duplicate = false) { + return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc, duplicate); } SymRef declareFun_Commutative_NoScoping_Chainable(std::string const & s, SRef rsort, vec const & args) { return declareFun(s, rsort, args, SymConf::CommutativeNoScopingChainable); diff --git a/src/symbols/SymStore.cc b/src/symbols/SymStore.cc index 49c5cd965..2d274bf0a 100644 --- a/src/symbols/SymStore.cc +++ b/src/symbols/SymStore.cc @@ -39,20 +39,19 @@ SymStore::~SymStore() { free(idToName[i]); } -SymRef SymStore::newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig) { +SymRef SymStore::newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig, + bool duplicate) { // Check if there already is a term called fname with same number of arguments of the same sort auto * symrefs = getRefOrNull(fname); - if (symrefs) { + if (symrefs && !duplicate) { vec const & trs = *symrefs; for (SymRef symref : trs) { auto const & symbol = ta[symref]; if (symbol.rsort() == rsort and symbol.nargs() == args.size_() and symbol.commutes() == symConfig.commutes and symbol.noScoping() == symConfig.noScoping and symbol.isInterpreted() == symConfig.isInterpreted) { - if (std::equal(symbol.begin(), symbol.end(), args.begin()) && (strcmp(fname, "*") != 0)) { - return symref; - } + if (std::equal(symbol.begin(), symbol.end(), args.begin())) { return symref; } } } } diff --git a/src/symbols/SymStore.h b/src/symbols/SymStore.h index 375c8b527..8bcc12540 100644 --- a/src/symbols/SymStore.h +++ b/src/symbols/SymStore.h @@ -40,7 +40,8 @@ class SymStore { SymStore(SymStore &&) = default; SymStore & operator=(SymStore &&) = default; // Constructs a new symbol. - SymRef newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig); + SymRef newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig, + bool ignoreDuplicates = false); SymRef newSymb(char const * fname, SRef rsort, vec const & args) { return newSymb(fname, rsort, args, SymConf::Default); } From d8953ace4dbf50d615758e7d832bda4e9d939edb Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Tue, 19 Nov 2024 11:54:03 +0100 Subject: [PATCH 15/20] NonlinWork: SubSymbol notion --- src/logics/Logic.cc | 4 ++-- src/logics/Logic.h | 4 ++-- src/pterms/PtStore.cc | 6 ++---- src/symbols/SymStore.cc | 6 +++--- src/symbols/SymStore.h | 2 +- 5 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index 487735e11..7aecc74ad 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -728,11 +728,11 @@ PTRef Logic::mkSelect(vec && args) { } SymRef Logic::declareFun(std::string const & fname, SRef rsort, vec const & args, - SymbolConfig const & symbolConfig, bool duplicate) { + SymbolConfig const & symbolConfig, bool subSymb) { assert(rsort != SRef_Undef); assert(std::find(args.begin(), args.end(), SRef_Undef) == args.end()); - SymRef sr = sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig, duplicate); + SymRef sr = sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig, subSymb); return sr; } diff --git a/src/logics/Logic.h b/src/logics/Logic.h index a98bb69b1..1fb68d411 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -185,8 +185,8 @@ class Logic { return declareFun(s, rsort, args, SymConf::NoScopingPairwise); } SymRef declareFun_Commutative_NoScoping_LeftAssoc(std::string const & s, SRef rsort, vec const & args, - bool duplicate = false) { - return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc, duplicate); + bool subSymb = false) { + return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc, subSymb); } SymRef declareFun_Commutative_NoScoping_Chainable(std::string const & s, SRef rsort, vec const & args) { return declareFun(s, rsort, args, SymConf::CommutativeNoScopingChainable); diff --git a/src/pterms/PtStore.cc b/src/pterms/PtStore.cc index f2700787c..6c28226ae 100644 --- a/src/pterms/PtStore.cc +++ b/src/pterms/PtStore.cc @@ -29,7 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include #include -#include +#include namespace opensmt { int const PtStore::ptstore_vec_idx = 1; @@ -153,10 +153,8 @@ SymRef PtStore::lookupSymbol(char const * s, vec const & args, SymbolMatc } else { return candidates[0]; } - } else if (strcmp(s, "*") == 0) { - assert(candidates.size() == 2); - return candidates[0]; } + assert(candidates.size() > 1); if (sort == SRef_Undef) { throw ApiException("Ambiguous symbol: `" + std::string(s) + "'"); } diff --git a/src/symbols/SymStore.cc b/src/symbols/SymStore.cc index 2d274bf0a..306a3ed3c 100644 --- a/src/symbols/SymStore.cc +++ b/src/symbols/SymStore.cc @@ -40,11 +40,11 @@ SymStore::~SymStore() { } SymRef SymStore::newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig, - bool duplicate) { + bool subSymb) { // Check if there already is a term called fname with same number of arguments of the same sort auto * symrefs = getRefOrNull(fname); - if (symrefs && !duplicate) { + if (symrefs && !subSymb) { vec const & trs = *symrefs; for (SymRef symref : trs) { auto const & symbol = ta[symref]; @@ -68,7 +68,7 @@ SymRef SymStore::newSymb(char const * fname, SRef rsort, vec const & args, vec trs; trs.push(tr); symbolTable.insert(tmp_name, trs); - } else { + } else if (!subSymb) { symbolTable[tmp_name].push(tr); // Map the name to term reference (why not id?), used in parsing } return tr; diff --git a/src/symbols/SymStore.h b/src/symbols/SymStore.h index 8bcc12540..baa95ad28 100644 --- a/src/symbols/SymStore.h +++ b/src/symbols/SymStore.h @@ -41,7 +41,7 @@ class SymStore { SymStore & operator=(SymStore &&) = default; // Constructs a new symbol. SymRef newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig, - bool ignoreDuplicates = false); + bool subSymb = false); SymRef newSymb(char const * fname, SRef rsort, vec const & args) { return newSymb(fname, rsort, args, SymConf::Default); } From 3829c5caa9f09e6d0b2268824e4159972c517b77 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Wed, 20 Nov 2024 18:51:07 +0100 Subject: [PATCH 16/20] NonlinWork: added sym_Int_TIMES_LIN --- src/logics/ArithLogic.cc | 46 +++++++++++++++---------------- src/logics/ArithLogic.h | 23 +++++++++++----- src/tsolvers/lasolver/LASolver.cc | 6 ++-- test/unit/test_LIALogicMkTerms.cc | 6 ++-- 4 files changed, 45 insertions(+), 36 deletions(-) diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 0452dd550..7dd6ec884 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -114,6 +114,8 @@ ArithLogic::ArithLogic(Logic_t type) sym_Real_MINUS(declareFun_NoScoping_LeftAssoc(tk_real_minus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_plus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), + sym_Real_TIMES_LIN( + declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL}, true)), sym_Real_TIMES_NONLIN( declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL}, true)), sym_Real_DIV(declareFun_NoScoping_LeftAssoc(tk_real_div, sort_REAL, {sort_REAL, sort_REAL})), @@ -136,6 +138,7 @@ ArithLogic::ArithLogic(Logic_t type) sym_Int_MINUS(declareFun_NoScoping_LeftAssoc(tk_int_minus, sort_INT, {sort_INT, sort_INT})), sym_Int_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_plus, sort_INT, {sort_INT, sort_INT})), sym_Int_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})), + sym_Int_TIMES_LIN(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT}, true)), sym_Int_TIMES_NONLIN( declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT}, true)), sym_Int_DIV(declareFun_NoScoping_LeftAssoc(tk_int_div, sort_INT, {sort_INT, sort_INT})), @@ -153,9 +156,9 @@ SymRef ArithLogic::getPlusForSort(SRef sort) const { return sort == getSort_int() ? get_sym_Int_PLUS() : get_sym_Real_PLUS(); } -SymRef ArithLogic::getTimesForSort(SRef sort) const { +SymRef ArithLogic::getTimesLinForSort(SRef sort) const { assert(sort == getSort_int() or sort == getSort_real()); - return sort == getSort_int() ? get_sym_Int_TIMES() : get_sym_Real_TIMES(); + return sort == getSort_int() ? get_sym_Int_TIMES_LIN() : get_sym_Real_TIMES_LIN(); } SymRef ArithLogic::getTimesNonlinForSort(SRef sort) const { @@ -185,7 +188,7 @@ PTRef ArithLogic::getMinusOneForSort(SRef sort) const { bool ArithLogic::isLinearFactor(PTRef tr) const { if (isNumConst(tr) || isNumVarLike(tr)) { return true; } - if (isTimes(tr)) { + if (isTimesLin(tr)) { Pterm const & term = getPterm(tr); return term.size() == 2 && ((isNumConst(term[0]) && (isNumVarLike(term[1]))) || (isNumConst(term[1]) && (isNumVarLike(term[0])))); @@ -203,10 +206,7 @@ bool ArithLogic::isLinearTerm(PTRef tr) const { } bool ArithLogic::isNonlin(PTRef tr) const { - if (isTimes(tr)) { - Pterm const & term = getPterm(tr); - if (term.size() > 2 || (not isConstant(term[0]) && not isConstant(term[1]))) return true; - } + if (isTimesNonlin(tr)) { return true; } if (isRealDiv(tr) || isIntDiv(tr) || isMod(getPterm(tr).symb())) { Pterm const & term = getPterm(tr); if (not isConstant(term[1])) return true; @@ -266,7 +266,7 @@ pair ArithLogic::splitPolyTerm(PTRef term) const { // Normalize a product of the form (* a v) to either v or (* -1 v) PTRef ArithLogic::normalizeMul(PTRef mul) { - assert(isTimes(mul)); + assert(isTimesDefined(mul)); auto [v, c] = splitPolyTerm(mul); if (getNumConst(c) < 0) { return mkNeg(v); @@ -429,7 +429,7 @@ lbool ArithLogic::arithmeticElimination(vec const & top_level_arith, Subs auto coeff = logic.getNumConst(c); poly.addTerm(var, std::move(coeff)); } else { - assert(logic.isPlus(polyTerm) || logic.isTimes(polyTerm)); + assert(logic.isPlus(polyTerm) || logic.isTimesDefined(polyTerm)); for (PTRef factor : logic.getPterm(polyTerm)) { auto [var, c] = logic.splitPolyTerm(factor); auto coeff = logic.getNumConst(c); @@ -498,14 +498,14 @@ pair ArithLogic::retrieveSubstitutions(vec const } uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) const { - assert(l.isTimes(tr)); + assert(l.isTimesDefined(tr)); auto [v, c] = l.splitPolyTerm(tr); return v.x; } bool LessThan_deepPTRef::operator()(PTRef x_, PTRef y_) const { - uint32_t id_x = l.isTimes(x_) ? getVarIdFromProduct(x_) : x_.x; - uint32_t id_y = l.isTimes(y_) ? getVarIdFromProduct(y_) : y_.x; + uint32_t id_x = l.isTimesDefined(x_) ? getVarIdFromProduct(x_) : x_.x; + uint32_t id_y = l.isTimesDefined(y_) ? getVarIdFromProduct(y_) : y_.x; return id_x < id_y; } @@ -522,7 +522,7 @@ bool ArithLogic::isBuiltinFunction(SymRef const sr) const { bool ArithLogic::isNumTerm(PTRef tr) const { if (isNumVarLike(tr)) return true; Pterm const & t = getPterm(tr); - if (t.size() == 2 && isTimes(tr)) + if (t.size() == 2 && isTimesLin(tr)) return (isNumVarLike(t[0]) && isConstant(t[1])) || (isNumVarLike(t[1]) && isConstant(t[0])); else if (t.size() == 0) return isNumVar(tr) || isConstant(tr); @@ -558,11 +558,11 @@ PTRef ArithLogic::mkNeg(PTRef tr) { } if (isTimesNonlin(symref)) { SRef returnSort = getSortRef(tr); - return mkFun(getTimesForSort(returnSort), {tr, getMinusOneForSort(returnSort)}); + return mkFun(getTimesLinForSort(returnSort), {tr, getMinusOneForSort(returnSort)}); } if (isNumVarLike(symref)) { auto sortRef = getSortRef(symref); - return mkFun(getTimesForSort(sortRef), {tr, getMinusOneForSort(sortRef)}); + return mkFun(getTimesLinForSort(sortRef), {tr, getMinusOneForSort(sortRef)}); } // MB: All cases should be covered throw InternalException("Failed attempt to negate a term"); @@ -661,7 +661,7 @@ PTRef ArithLogic::mkPlus(vec && args) { continue; } // default case, variable and constant (cannot be simplified) - PTRef term = mkFun(getTimesForSort(returnSort), {coeffTerm, var}); + PTRef term = mkFun(getTimesLinForSort(returnSort), {coeffTerm, var}); flattened_args.push(term); } if (flattened_args.size() == 0) return getZeroForSort(returnSort); @@ -695,7 +695,7 @@ PTRef ArithLogic::mkTimes(vec && args) { SimplifyConstTimes simp(*this); args.clear(); SymRef s_new; - simp.simplify(getTimesForSort(returnSort), flatten_args, s_new, args); + simp.simplify(getTimesLinForSort(returnSort), flatten_args, s_new, args); if (!isTimes(s_new)) return mkFun(s_new, std::move(args)); PTRef coef = PTRef_Undef; std::vector vars; @@ -748,8 +748,8 @@ PTRef ArithLogic::mkBinaryLeq(PTRef lhs, PTRef rhs) { return v.sign() < 0 ? getTerm_false() : getTerm_true(); } if (isNumVarLike(sum_tmp) || - isTimes(sum_tmp)) { // "sum_tmp = c * v", just scale to "v" or "-v" without changing the sign - sum_tmp = isTimes(sum_tmp) ? normalizeMul(sum_tmp) : sum_tmp; + isTimesDefined(sum_tmp)) { // "sum_tmp = c * v", just scale to "v" or "-v" without changing the sign + sum_tmp = isTimesDefined(sum_tmp) ? normalizeMul(sum_tmp) : sum_tmp; return mkFun(getLeqForSort(argSort), {getZeroForSort(argSort), sum_tmp}); } else if (isPlus(sum_tmp)) { // Normalize the sum @@ -820,7 +820,7 @@ PTRef ArithLogic::mkBinaryEq(PTRef lhs, PTRef rhs) { if (isConstant(diff)) { Number const & v = this->getNumConst(diff); return v.isZero() ? getTerm_true() : getTerm_false(); - } else if (isNumVarLike(diff) || isTimes(diff)) { + } else if (isNumVarLike(diff) || isTimesDefined(diff)) { auto [var, constant] = splitPolyTerm(diff); return Logic::mkBinaryEq(getZeroForSort(eqSort), var); // Avoid anything that calls Logic::mkEq as this would create a loop @@ -1017,7 +1017,7 @@ void SimplifyConst::simplify(SymRef s, vec const & args, SymRef & s_new, } // // A single argument for the operator, and the operator is identity // // in that case - if (args_new.size() == 1 && (l.isPlus(s_new) || l.isTimes(s_new))) { + if (args_new.size() == 1 && (l.isPlus(s_new) || l.isTimesDefined(s_new))) { PTRef ch_tr = args_new[0]; args_new.clear(); s_new = l.getPterm(ch_tr).symb(); @@ -1236,7 +1236,7 @@ pair ArithLogic::sumToNormalizedIntPair(PTRef sum) { coeffs.reserve(varFactors.size()); for (PTRef factor : varFactors) { auto [var, coeff] = splitPolyTerm(factor); - assert((ArithLogic::isNumVarLike(var) || ArithLogic::isTimes(var)) and isNumConst(coeff)); + assert((ArithLogic::isNumVarLike(var) || ArithLogic::isTimesDefined(var)) and isNumConst(coeff)); vars.push(var); coeffs.push_back(getNumConst(coeff)); } @@ -1376,7 +1376,7 @@ std::pair ArithLogic::leqToConstantAndTerm(PTRef leq) { bool ArithLogic::hasNegativeLeadingVariable(PTRef poly) const { if (isNumConst(poly) or isNumVarLike(poly)) { return false; } - if (isTimes(poly)) { + if (isTimesDefined(poly)) { auto [var, constant] = splitPolyTerm(poly); return isNegative(getNumConst(constant)); } diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index 9e2382fe3..10d9a387d 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -95,6 +95,8 @@ class ArithLogic : public Logic { SymRef get_sym_Int_TIMES() const { return sym_Int_TIMES; } SymRef get_sym_Real_TIMES() const { return sym_Real_TIMES; } + SymRef get_sym_Int_TIMES_LIN() const { return sym_Int_TIMES_LIN; } + SymRef get_sym_Real_TIMES_LIN() const { return sym_Real_TIMES_LIN; } SymRef get_sym_Int_TIMES_NONLIN() const { return sym_Int_TIMES_NONLIN; } SymRef get_sym_Real_TIMES_NONLIN() const { return sym_Real_TIMES_NONLIN; } SymRef get_sym_Int_DIV() const { return sym_Int_DIV; } @@ -162,20 +164,25 @@ class ArithLogic : public Logic { bool isIntNeg(SymRef sr) const { return sr == sym_Int_NEG; } bool isRealNeg(SymRef sr) const { return sr == sym_Real_NEG; } - bool isTimes(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr); }; - bool isTimesLin(SymRef sr) const { return isIntTimes(sr) or isRealTimes(sr); } + bool isTimes(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr) or isTimesUnknown(sr); }; + bool isTimesDefined(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr); }; + bool isTimesLin(SymRef sr) const { return isIntTimesLin(sr) or isRealTimesLin(sr); } + bool isTimesUnknown(SymRef sr) const { return isIntTimes(sr) or isRealTimes(sr); } bool isTimesNonlin(SymRef sr) const { return isIntTimesNonlin(sr) or isRealTimesNonlin(sr); } bool isTimes(PTRef tr) const { return isTimes(getPterm(tr).symb()); } + bool isTimesDefined(PTRef tr) const { return isTimesDefined(getPterm(tr).symb()); }; bool isTimesLin(PTRef tr) const { return isTimesLin(getPterm(tr).symb()); } bool isTimesNonlin(PTRef tr) const { return isTimesNonlin(getPterm(tr).symb()); } - bool isIntTimes(PTRef tr) const { return isIntTimes(getPterm(tr).symb()); } + bool isIntTimesLin(PTRef tr) const { return isIntTimesLin(getPterm(tr).symb()); } bool isIntTimesNonlin(PTRef tr) const { return isIntTimesNonlin(getPterm(tr).symb()); } - bool isRealTimes(PTRef tr) const { return isRealTimes(getPterm(tr).symb()); } + bool isRealTimesLin(PTRef tr) const { return isRealTimesLin(getPterm(tr).symb()); } bool isRealTimesNonlin(PTRef tr) const { return isRealTimesNonlin(getPterm(tr).symb()); } - bool isIntTimes(SymRef sr) const { return sr == sym_Int_TIMES; } + bool isIntTimesLin(SymRef sr) const { return sr == sym_Int_TIMES_LIN; } bool isIntTimesNonlin(SymRef sr) const { return sr == sym_Int_TIMES_NONLIN; } - bool isRealTimes(SymRef sr) const { return sr == sym_Real_TIMES; } + bool isRealTimesLin(SymRef sr) const { return sr == sym_Real_TIMES_LIN; } bool isRealTimesNonlin(SymRef sr) const { return sr == sym_Real_TIMES_NONLIN; } + bool isIntTimes(SymRef sr) const { return sr == sym_Int_TIMES; } + bool isRealTimes(SymRef sr) const { return sr == sym_Real_TIMES; } bool isRealDiv(PTRef tr) const { return isRealDiv(getPterm(tr).symb()); } bool isRealDiv(SymRef sr) const { return sr == sym_Real_DIV; } @@ -268,7 +275,7 @@ class ArithLogic : public Logic { } SymRef getPlusForSort(SRef sort) const; - SymRef getTimesForSort(SRef sort) const; + SymRef getTimesLinForSort(SRef sort) const; SymRef getTimesNonlinForSort(SRef sort) const; SymRef getMinusForSort(SRef sort) const; @@ -433,6 +440,7 @@ class ArithLogic : public Logic { SymRef sym_Real_MINUS; SymRef sym_Real_PLUS; SymRef sym_Real_TIMES; + SymRef sym_Real_TIMES_LIN; SymRef sym_Real_TIMES_NONLIN; SymRef sym_Real_DIV; SymRef sym_Real_EQ; @@ -454,6 +462,7 @@ class ArithLogic : public Logic { SymRef sym_Int_MINUS; SymRef sym_Int_PLUS; SymRef sym_Int_TIMES; + SymRef sym_Int_TIMES_LIN; SymRef sym_Int_TIMES_NONLIN; SymRef sym_Int_DIV; SymRef sym_Int_MOD; diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index 659987484..b4cd98124 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -91,7 +91,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.isTimes(sum) || logic.isMod(logic.getPterm(sum).symb()) || + assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimesDefined(sum) || logic.isMod(logic.getPterm(sum).symb()) || logic.isRealDiv(sum) || logic.isIntDiv(sum)); (void) cons; (void)sum; } @@ -290,7 +290,7 @@ LVRef LASolver::registerArithmeticTerm(PTRef expr) { if (logic.isNonlin(expr)) { auto termStr = logic.pp(expr); throw LANonLinearException(termStr.c_str()); - } else if(logic.isTimes(expr) || logic.isPlus(expr)) { + } else if(logic.isTimesLin(expr) || logic.isPlus(expr)) { Pterm const & subterms = logic.getPterm(expr); for(auto subterm: subterms) { if (logic.isNonlin(subterm)) { @@ -307,7 +307,7 @@ LVRef LASolver::registerArithmeticTerm(PTRef expr) { } } - if (logic.isNumVar(expr) || logic.isTimes(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)))); diff --git a/test/unit/test_LIALogicMkTerms.cc b/test/unit/test_LIALogicMkTerms.cc index 8d6ed42e1..f41d12ce2 100644 --- a/test/unit/test_LIALogicMkTerms.cc +++ b/test/unit/test_LIALogicMkTerms.cc @@ -74,7 +74,7 @@ TEST_F(LIALogicMkTermsTest, testMod_Times) { PTRef three = logic.mkIntConst(3); PTRef mod = logic.mkMod(x,two); PTRef times = logic.mkTimes(mod, three); - EXPECT_EQ(logic.getSymRef(times), logic.get_sym_Int_TIMES()); + EXPECT_EQ(logic.getSymRef(times), logic.get_sym_Int_TIMES_LIN()); } TEST_F(LIALogicMkTermsTest, testMod_Leq) { @@ -191,8 +191,8 @@ TEST_F(LIALogicMkTermsTest, test_EqualityNormalization_EqualityToConstant) { PTRef eq = logic.mkEq(x, two); PTRef lhs = logic.getPterm(eq)[0]; PTRef rhs = logic.getPterm(eq)[1]; - EXPECT_NE(logic.getSymRef(lhs), logic.get_sym_Int_TIMES()); - EXPECT_NE(logic.getSymRef(rhs), logic.get_sym_Int_TIMES()); + EXPECT_NE(logic.getSymRef(lhs), logic.get_sym_Int_TIMES_LIN()); + EXPECT_NE(logic.getSymRef(rhs), logic.get_sym_Int_TIMES_LIN()); } TEST_F(LIALogicMkTermsTest, test_ReverseAuxRewrite) { From 68ac42d10d6c14cff5c2513eac2b0fb87086f1a1 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Mon, 25 Nov 2024 12:09:51 +0100 Subject: [PATCH 17/20] NonlinWork: added new functions, rework of the accessible parts --- src/logics/ArithLogic.cc | 11 ++++------- src/logics/Logic.cc | 4 ++-- src/logics/Logic.h | 12 +++++++----- src/symbols/SymStore.h | 4 ++++ 4 files changed, 17 insertions(+), 14 deletions(-) diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 7dd6ec884..02b602fab 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -114,10 +114,8 @@ ArithLogic::ArithLogic(Logic_t type) sym_Real_MINUS(declareFun_NoScoping_LeftAssoc(tk_real_minus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_plus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), - sym_Real_TIMES_LIN( - declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL}, true)), - sym_Real_TIMES_NONLIN( - declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL}, true)), + sym_Real_TIMES_LIN(declareFun_Multiplication_Duplicate(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), + sym_Real_TIMES_NONLIN(declareFun_Multiplication_Duplicate(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_DIV(declareFun_NoScoping_LeftAssoc(tk_real_div, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_EQ(sortToEquality[sort_REAL]), sym_Real_LEQ(declareFun_NoScoping_Chainable(tk_real_leq, sort_BOOL, {sort_REAL, sort_REAL})), @@ -138,9 +136,8 @@ ArithLogic::ArithLogic(Logic_t type) sym_Int_MINUS(declareFun_NoScoping_LeftAssoc(tk_int_minus, sort_INT, {sort_INT, sort_INT})), sym_Int_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_plus, sort_INT, {sort_INT, sort_INT})), sym_Int_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})), - sym_Int_TIMES_LIN(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT}, true)), - sym_Int_TIMES_NONLIN( - declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT}, true)), + sym_Int_TIMES_LIN(declareFun_Multiplication_Duplicate(tk_int_times, sort_INT, {sort_INT, sort_INT})), + sym_Int_TIMES_NONLIN(declareFun_Multiplication_Duplicate(tk_int_times, sort_INT, {sort_INT, sort_INT})), sym_Int_DIV(declareFun_NoScoping_LeftAssoc(tk_int_div, sort_INT, {sort_INT, sort_INT})), sym_Int_MOD(declareFun_NoScoping(tk_int_mod, sort_INT, {sort_INT, sort_INT})), sym_Int_EQ(sortToEquality[sort_INT]), diff --git a/src/logics/Logic.cc b/src/logics/Logic.cc index 7aecc74ad..85f06522c 100644 --- a/src/logics/Logic.cc +++ b/src/logics/Logic.cc @@ -728,11 +728,11 @@ PTRef Logic::mkSelect(vec && args) { } SymRef Logic::declareFun(std::string const & fname, SRef rsort, vec const & args, - SymbolConfig const & symbolConfig, bool subSymb) { + SymbolConfig const & symbolConfig) { assert(rsort != SRef_Undef); assert(std::find(args.begin(), args.end(), SRef_Undef) == args.end()); - SymRef sr = sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig, subSymb); + SymRef sr = sym_store.newSymb(fname.c_str(), rsort, args, symbolConfig); return sr; } diff --git a/src/logics/Logic.h b/src/logics/Logic.h index 1fb68d411..b5d0cbc10 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -164,8 +164,7 @@ class Logic { virtual PTRef mkConst(char const *); virtual PTRef mkConst(SRef, char const *); - SymRef declareFun(std::string const & fname, SRef rsort, vec const & args, SymbolConfig const & symbolConfig, - bool duplicate = false); + SymRef declareFun(std::string const & fname, SRef rsort, vec const & args, SymbolConfig const & symbolConfig); SymRef declareFun(std::string const & fname, SRef rsort, vec const & args) { return declareFun(fname, rsort, args, SymConf::Default); } @@ -184,9 +183,12 @@ class Logic { SymRef declareFun_NoScoping_Pairwise(std::string const & s, SRef rsort, vec const & args) { return declareFun(s, rsort, args, SymConf::NoScopingPairwise); } - SymRef declareFun_Commutative_NoScoping_LeftAssoc(std::string const & s, SRef rsort, vec const & args, - bool subSymb = false) { - return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc, subSymb); + SymRef declareFun_Commutative_NoScoping_LeftAssoc(std::string const & s, SRef rsort, vec const & args) { + return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc); + } + SymRef declareFun_Multiplication_Duplicate(std::string const & s, SRef rsort, vec const & args) { + SymRef sr = sym_store.newUnparsableSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc); + return sr; } SymRef declareFun_Commutative_NoScoping_Chainable(std::string const & s, SRef rsort, vec const & args) { return declareFun(s, rsort, args, SymConf::CommutativeNoScopingChainable); diff --git a/src/symbols/SymStore.h b/src/symbols/SymStore.h index baa95ad28..b32600f00 100644 --- a/src/symbols/SymStore.h +++ b/src/symbols/SymStore.h @@ -40,11 +40,15 @@ class SymStore { SymStore(SymStore &&) = default; SymStore & operator=(SymStore &&) = default; // Constructs a new symbol. + SymRef newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig, bool subSymb = false); SymRef newSymb(char const * fname, SRef rsort, vec const & args) { return newSymb(fname, rsort, args, SymConf::Default); } + SymRef newUnparsableSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig) { + return newSymb(fname, rsort, args, symConfig, true); + } bool contains(char const * fname) const { return symbolTable.has(fname); } vec const & nameToRef(char const * s) const { return symbolTable[s]; } vec & nameToRef(char const * s) { return symbolTable[s]; } From 1668eff5d7a8c1692b97d41501be11c1f80fa181 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 28 Nov 2024 11:12:36 +0100 Subject: [PATCH 18/20] NonlinWork: Fixes according to comments --- src/api/MainSolver.cc | 15 ++-- src/common/CMakeLists.txt | 2 +- src/common/NonLinException.h | 23 ++++++ src/logics/ArithLogic.cc | 72 ++++++++----------- src/logics/ArithLogic.h | 19 ++--- src/logics/Logic.h | 4 -- src/rewriters/DivModRewriter.h | 3 +- src/simplifiers/LA.cc | 4 +- src/symbols/SymStore.h | 12 ++-- src/tsolvers/lasolver/LASolver.cc | 20 ++---- src/tsolvers/lasolver/LASolver.h | 11 --- .../base/arithmetic/miniexample3.smt2 | 1 - .../base/arithmetic/miniexample3_Ok.smt2 | 1 - test/unit/test_Ites.cc | 2 +- 14 files changed, 90 insertions(+), 99 deletions(-) create mode 100644 src/common/NonLinException.h diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 6d1043df8..2d5e93730 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -9,6 +9,7 @@ #include "MainSolver.h" #include +#include #include #include #include @@ -333,18 +334,22 @@ sstat MainSolver::check() { StopWatch sw(query_timer); } if (isLastFrameUnsat()) { return s_False; } - sstat rval = simplifyFormulas(); + sstat rval; + try { + rval = simplifyFormulas(); + } catch (opensmt::NonLinException const & error) { + reasonUnknown = error.what(); + return s_Undef; + } if (config.dump_query()) printCurrentAssertionsAsQuery(); if (rval == s_Undef) { try { rval = solve(); - } catch (std::overflow_error const & error) { - rval = s_Error; - } catch (opensmt::LANonLinearException const & error) { + } 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/common/CMakeLists.txt b/src/common/CMakeLists.txt index ed6e244aa..fcb542f1a 100644 --- a/src/common/CMakeLists.txt +++ b/src/common/CMakeLists.txt @@ -24,5 +24,5 @@ include(numbers/CMakeLists.txt) install(FILES StringMap.h Timer.h inttypes.h IColor.h TreeOps.h FlaPartitionMap.h PartitionInfo.h Partitions.h ApiException.h TypeUtils.h - NatSet.h ScopedVector.h TermNames.h + NatSet.h ScopedVector.h TermNames.h NonLinException.h DESTINATION ${INSTALL_HEADERS_DIR}/common) diff --git a/src/common/NonLinException.h b/src/common/NonLinException.h new file mode 100644 index 000000000..0d476c525 --- /dev/null +++ b/src/common/NonLinException.h @@ -0,0 +1,23 @@ +/* +* Copyright (c) 2024, Konstantin Britikov +* +* SPDX-License-Identifier: MIT +*/ + +#ifndef OPENSMT_NONLINEXCEPTION_H +#define OPENSMT_NONLINEXCEPTION_H + +namespace opensmt { +class NonLinException : public std::runtime_error { +public: + NonLinException(std::string_view const reason_) : runtime_error(std::string(reason_)) { + msg = "Term " + std::string(reason_) + " is non-linear"; + } + virtual char const * what() const noexcept override { return msg.c_str(); } + +private: + std::string msg; +}; +} + +#endif // OPENSMT_NONLINEXCEPTION_H diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 02b602fab..5f2079d2b 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -114,8 +114,8 @@ ArithLogic::ArithLogic(Logic_t type) sym_Real_MINUS(declareFun_NoScoping_LeftAssoc(tk_real_minus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_plus, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), - sym_Real_TIMES_LIN(declareFun_Multiplication_Duplicate(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), - sym_Real_TIMES_NONLIN(declareFun_Multiplication_Duplicate(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), + sym_Real_TIMES_LIN(declareFun_Multiplication_LinNonlin(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), + sym_Real_TIMES_NONLIN(declareFun_Multiplication_LinNonlin(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_DIV(declareFun_NoScoping_LeftAssoc(tk_real_div, sort_REAL, {sort_REAL, sort_REAL})), sym_Real_EQ(sortToEquality[sort_REAL]), sym_Real_LEQ(declareFun_NoScoping_Chainable(tk_real_leq, sort_BOOL, {sort_REAL, sort_REAL})), @@ -136,8 +136,8 @@ ArithLogic::ArithLogic(Logic_t type) sym_Int_MINUS(declareFun_NoScoping_LeftAssoc(tk_int_minus, sort_INT, {sort_INT, sort_INT})), sym_Int_PLUS(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_plus, sort_INT, {sort_INT, sort_INT})), sym_Int_TIMES(declareFun_Commutative_NoScoping_LeftAssoc(tk_int_times, sort_INT, {sort_INT, sort_INT})), - sym_Int_TIMES_LIN(declareFun_Multiplication_Duplicate(tk_int_times, sort_INT, {sort_INT, sort_INT})), - sym_Int_TIMES_NONLIN(declareFun_Multiplication_Duplicate(tk_int_times, sort_INT, {sort_INT, sort_INT})), + sym_Int_TIMES_LIN(declareFun_Multiplication_LinNonlin(tk_int_times, sort_INT, {sort_INT, sort_INT})), + sym_Int_TIMES_NONLIN(declareFun_Multiplication_LinNonlin(tk_int_times, sort_INT, {sort_INT, sort_INT})), sym_Int_DIV(declareFun_NoScoping_LeftAssoc(tk_int_div, sort_INT, {sort_INT, sort_INT})), sym_Int_MOD(declareFun_NoScoping(tk_int_mod, sort_INT, {sort_INT, sort_INT})), sym_Int_EQ(sortToEquality[sort_INT]), @@ -184,11 +184,11 @@ PTRef ArithLogic::getMinusOneForSort(SRef sort) const { } bool ArithLogic::isLinearFactor(PTRef tr) const { - if (isNumConst(tr) || isNumVarLike(tr)) { return true; } + if (isNumConst(tr) || isMonomial(tr)) { return true; } if (isTimesLin(tr)) { Pterm const & term = getPterm(tr); return term.size() == 2 && - ((isNumConst(term[0]) && (isNumVarLike(term[1]))) || (isNumConst(term[1]) && (isNumVarLike(term[0])))); + ((isNumConst(term[0]) && (isMonomial(term[1]))) || (isNumConst(term[1]) && (isMonomial(term[0])))); } return false; } @@ -202,15 +202,6 @@ bool ArithLogic::isLinearTerm(PTRef tr) const { return false; } -bool ArithLogic::isNonlin(PTRef tr) const { - if (isTimesNonlin(tr)) { return true; } - if (isRealDiv(tr) || isIntDiv(tr) || isMod(getPterm(tr).symb())) { - Pterm const & term = getPterm(tr); - if (not isConstant(term[1])) return true; - } - return false; -}; - Number const & ArithLogic::getNumConst(PTRef tr) const { SymId id = sym_store[getPterm(tr).symb()].getId(); assert(id < static_cast(numbers.size()) && numbers[id] != nullptr); @@ -238,19 +229,16 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { } pair ArithLogic::splitPolyTerm(PTRef term) const { - assert(isTimes(term) || isNumVarLike(term) || isConstant(term)); + assert(isTimes(term) || isMonomial(term) || isConstant(term)); if (isTimesLin(term)) { assert(getPterm(term).size() == 2); PTRef fac = getPterm(term)[0]; PTRef var = getPterm(term)[1]; if (not isConstant(fac)) { std::swap(fac, var); } assert(isConstant(fac)); - assert(isNumVarLike(var) || isTimesNonlin(var)); + assert(isMonomial(var)); return {var, fac}; - } else if (isTimesNonlin(term)) { - PTRef one = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); - return {term, one}; - } else if (isNumVarLike(term)) { + } else if (isMonomial(term)) { assert(yieldsSortInt(term) or yieldsSortReal(term)); PTRef var = term; PTRef fac = yieldsSortInt(term) ? getTerm_IntOne() : getTerm_RealOne(); @@ -263,7 +251,7 @@ pair ArithLogic::splitPolyTerm(PTRef term) const { // Normalize a product of the form (* a v) to either v or (* -1 v) PTRef ArithLogic::normalizeMul(PTRef mul) { - assert(isTimesDefined(mul)); + assert(isTimesLinOrNonlin(mul)); auto [v, c] = splitPolyTerm(mul); if (getNumConst(c) < 0) { return mkNeg(v); @@ -426,7 +414,7 @@ lbool ArithLogic::arithmeticElimination(vec const & top_level_arith, Subs auto coeff = logic.getNumConst(c); poly.addTerm(var, std::move(coeff)); } else { - assert(logic.isPlus(polyTerm) || logic.isTimesDefined(polyTerm)); + assert(logic.isPlus(polyTerm) || logic.isTimesLinOrNonlin(polyTerm)); for (PTRef factor : logic.getPterm(polyTerm)) { auto [var, c] = logic.splitPolyTerm(factor); auto coeff = logic.getNumConst(c); @@ -495,14 +483,14 @@ pair ArithLogic::retrieveSubstitutions(vec const } uint32_t LessThan_deepPTRef::getVarIdFromProduct(PTRef tr) const { - assert(l.isTimesDefined(tr)); + assert(l.isTimesLinOrNonlin(tr)); auto [v, c] = l.splitPolyTerm(tr); return v.x; } bool LessThan_deepPTRef::operator()(PTRef x_, PTRef y_) const { - uint32_t id_x = l.isTimesDefined(x_) ? getVarIdFromProduct(x_) : x_.x; - uint32_t id_y = l.isTimesDefined(y_) ? getVarIdFromProduct(y_) : y_.x; + uint32_t id_x = l.isTimesLinOrNonlin(x_) ? getVarIdFromProduct(x_) : x_.x; + uint32_t id_y = l.isTimesLinOrNonlin(y_) ? getVarIdFromProduct(y_) : y_.x; return id_x < id_y; } @@ -517,10 +505,10 @@ bool ArithLogic::isBuiltinFunction(SymRef const sr) const { return Logic::isBuiltinFunction(sr); } bool ArithLogic::isNumTerm(PTRef tr) const { - if (isNumVarLike(tr)) return true; + if (isMonomial(tr)) return true; Pterm const & t = getPterm(tr); if (t.size() == 2 && isTimesLin(tr)) - return (isNumVarLike(t[0]) && isConstant(t[1])) || (isNumVarLike(t[1]) && isConstant(t[0])); + return (isMonomial(t[0]) && isConstant(t[1])) || (isMonomial(t[1]) && isConstant(t[0])); else if (t.size() == 0) return isNumVar(tr) || isConstant(tr); else @@ -530,11 +518,11 @@ bool ArithLogic::isNumTerm(PTRef tr) const { PTRef ArithLogic::mkNeg(PTRef tr) { assert(!isNeg(tr)); // MB: The invariant now is that there is no "Minus" node SymRef symref = getSymRef(tr); - if (isConstant(symref)) { + if (isConstant(tr)) { Number const & v = getNumConst(tr); return mkConst(getSortRef(tr), -v); } - if (isPlus(symref)) { + if (isPlus(tr)) { vec args; args.capacity(getPterm(tr).size()); // Note: Do this in two phases to avoid calling mkNeg that invalidates the Pterm reference @@ -548,16 +536,12 @@ PTRef ArithLogic::mkNeg(PTRef tr) { PTRef tr_n = mkFun(symref, std::move(args)); return tr_n; } - if (isTimesLin(symref)) { // constant * (var-like \/ times-nonlin) + if (isTimesLin(tr)) { // constant * monomial assert(getPterm(tr).size() == 2); auto [var, constant] = splitPolyTerm(tr); return constant == getMinusOneForSort(getSortRef(symref)) ? var : mkFun(symref, {var, mkNeg(constant)}); } - if (isTimesNonlin(symref)) { - SRef returnSort = getSortRef(tr); - return mkFun(getTimesLinForSort(returnSort), {tr, getMinusOneForSort(returnSort)}); - } - if (isNumVarLike(symref)) { + if (isMonomial(tr)) { auto sortRef = getSortRef(symref); return mkFun(getTimesLinForSort(sortRef), {tr, getMinusOneForSort(sortRef)}); } @@ -744,9 +728,9 @@ PTRef ArithLogic::mkBinaryLeq(PTRef lhs, PTRef rhs) { Number const & v = this->getNumConst(sum_tmp); return v.sign() < 0 ? getTerm_false() : getTerm_true(); } - if (isNumVarLike(sum_tmp) || - isTimesDefined(sum_tmp)) { // "sum_tmp = c * v", just scale to "v" or "-v" without changing the sign - sum_tmp = isTimesDefined(sum_tmp) ? normalizeMul(sum_tmp) : sum_tmp; + if (isMonomial(sum_tmp) || + isTimesLinOrNonlin(sum_tmp)) { // "sum_tmp = c * v", just scale to "v" or "-v" without changing the sign + sum_tmp = isTimesLinOrNonlin(sum_tmp) ? normalizeMul(sum_tmp) : sum_tmp; return mkFun(getLeqForSort(argSort), {getZeroForSort(argSort), sum_tmp}); } else if (isPlus(sum_tmp)) { // Normalize the sum @@ -817,7 +801,7 @@ PTRef ArithLogic::mkBinaryEq(PTRef lhs, PTRef rhs) { if (isConstant(diff)) { Number const & v = this->getNumConst(diff); return v.isZero() ? getTerm_true() : getTerm_false(); - } else if (isNumVarLike(diff) || isTimesDefined(diff)) { + } else if (isMonomial(diff) || isTimesLin(diff)) { auto [var, constant] = splitPolyTerm(diff); return Logic::mkBinaryEq(getZeroForSort(eqSort), var); // Avoid anything that calls Logic::mkEq as this would create a loop @@ -1014,7 +998,7 @@ void SimplifyConst::simplify(SymRef s, vec const & args, SymRef & s_new, } // // A single argument for the operator, and the operator is identity // // in that case - if (args_new.size() == 1 && (l.isPlus(s_new) || l.isTimesDefined(s_new))) { + if (args_new.size() == 1 && (l.isPlus(s_new) || l.isTimesLinOrNonlin(s_new))) { PTRef ch_tr = args_new[0]; args_new.clear(); s_new = l.getPterm(ch_tr).symb(); @@ -1233,7 +1217,7 @@ pair ArithLogic::sumToNormalizedIntPair(PTRef sum) { coeffs.reserve(varFactors.size()); for (PTRef factor : varFactors) { auto [var, coeff] = splitPolyTerm(factor); - assert((ArithLogic::isNumVarLike(var) || ArithLogic::isTimesDefined(var)) and isNumConst(coeff)); + assert(ArithLogic::isMonomial(var) and isNumConst(coeff)); vars.push(var); coeffs.push_back(getNumConst(coeff)); } @@ -1372,8 +1356,8 @@ std::pair ArithLogic::leqToConstantAndTerm(PTRef leq) { } bool ArithLogic::hasNegativeLeadingVariable(PTRef poly) const { - if (isNumConst(poly) or isNumVarLike(poly)) { return false; } - if (isTimesDefined(poly)) { + if (isNumConst(poly) or isMonomial(poly)) { return false; } + if (isTimesLinOrNonlin(poly)) { auto [var, constant] = splitPolyTerm(poly); return isNegative(getNumConst(constant)); } diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index 10d9a387d..b8b7fb6c8 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -164,13 +164,12 @@ class ArithLogic : public Logic { bool isIntNeg(SymRef sr) const { return sr == sym_Int_NEG; } bool isRealNeg(SymRef sr) const { return sr == sym_Real_NEG; } - bool isTimes(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr) or isTimesUnknown(sr); }; - bool isTimesDefined(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr); }; + bool isTimes(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr) or isIntTimes(sr) or isRealTimes(sr); }; + bool isTimesLinOrNonlin(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr); }; bool isTimesLin(SymRef sr) const { return isIntTimesLin(sr) or isRealTimesLin(sr); } - bool isTimesUnknown(SymRef sr) const { return isIntTimes(sr) or isRealTimes(sr); } bool isTimesNonlin(SymRef sr) const { return isIntTimesNonlin(sr) or isRealTimesNonlin(sr); } bool isTimes(PTRef tr) const { return isTimes(getPterm(tr).symb()); } - bool isTimesDefined(PTRef tr) const { return isTimesDefined(getPterm(tr).symb()); }; + bool isTimesLinOrNonlin(PTRef tr) const { return isTimesLinOrNonlin(getPterm(tr).symb()); }; bool isTimesLin(PTRef tr) const { return isTimesLin(getPterm(tr).symb()); } bool isTimesNonlin(PTRef tr) const { return isTimesNonlin(getPterm(tr).symb()); } bool isIntTimesLin(PTRef tr) const { return isIntTimesLin(getPterm(tr).symb()); } @@ -229,10 +228,10 @@ class ArithLogic : public Logic { bool isNumVar(SymRef sr) const { return isVar(sr) and (yieldsSortInt(sr) or yieldsSortReal(sr)); } bool isNumVar(PTRef tr) const { return isNumVar(getPterm(tr).symb()); } - bool isNumVarLike(SymRef sr) const { - return yieldsSortNum(sr) and not isPlus(sr) and not isTimes(sr) and not isNumConst(sr); + bool isMonomial(PTRef tr) const { + SymRef sr = getPterm(tr).symb(); + return yieldsSortNum(sr) and not isPlus(sr) and not isTimesLin(sr) and not isNumConst(sr); } - bool isNumVarLike(PTRef tr) const { return isNumVarLike(getPterm(tr).symb()); } bool isZero(SymRef sr) const { return isIntZero(sr) or isRealZero(sr); } bool isZero(PTRef tr) const { return isZero(getSymRef(tr)); } @@ -252,7 +251,6 @@ 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; PTRef getTerm_IntZero() const { return term_Int_ZERO; } PTRef getTerm_RealZero() const { return term_Real_ZERO; } @@ -355,6 +353,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' @@ -389,6 +388,10 @@ class ArithLogic : public Logic { PTRef mkBinaryGeq(PTRef lhs, PTRef rhs) { return mkBinaryLeq(rhs, lhs); } PTRef mkBinaryLt(PTRef lhs, PTRef rhs) { return mkNot(mkBinaryGeq(lhs, rhs)); } PTRef mkBinaryGt(PTRef lhs, PTRef rhs) { return mkNot(mkBinaryLeq(lhs, rhs)); } + SymRef declareFun_Multiplication_LinNonlin(std::string const & s, SRef rsort, vec const & args) { + SymRef sr = sym_store.newInternalSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc); + return sr; + } PTRef mkBinaryEq(PTRef lhs, PTRef rhs) override; pair sumToNormalizedPair(PTRef sum); pair sumToNormalizedIntPair(PTRef sum); diff --git a/src/logics/Logic.h b/src/logics/Logic.h index b5d0cbc10..9a144ee61 100644 --- a/src/logics/Logic.h +++ b/src/logics/Logic.h @@ -186,10 +186,6 @@ class Logic { SymRef declareFun_Commutative_NoScoping_LeftAssoc(std::string const & s, SRef rsort, vec const & args) { return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc); } - SymRef declareFun_Multiplication_Duplicate(std::string const & s, SRef rsort, vec const & args) { - SymRef sr = sym_store.newUnparsableSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc); - return sr; - } SymRef declareFun_Commutative_NoScoping_Chainable(std::string const & s, SRef rsort, vec const & args) { return declareFun(s, rsort, args, SymConf::CommutativeNoScopingChainable); } diff --git a/src/rewriters/DivModRewriter.h b/src/rewriters/DivModRewriter.h index e7c5f2495..5123fbb5c 100644 --- a/src/rewriters/DivModRewriter.h +++ b/src/rewriters/DivModRewriter.h @@ -11,6 +11,7 @@ #include "Rewriter.h" #include +#include #include namespace opensmt { @@ -36,7 +37,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; } + if (!logic.isConstant(divisor)) throw NonLinException(logic.pp(term)); // collect the definitions to add assert(logic.isConstant(divisor)); auto divisorVal = logic.getNumConst(divisor); diff --git a/src/simplifiers/LA.cc b/src/simplifiers/LA.cc index ec1a51fa8..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.isNumVarLike(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/symbols/SymStore.h b/src/symbols/SymStore.h index b32600f00..2a5a85f40 100644 --- a/src/symbols/SymStore.h +++ b/src/symbols/SymStore.h @@ -41,12 +41,13 @@ class SymStore { SymStore & operator=(SymStore &&) = default; // Constructs a new symbol. - SymRef newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig, - bool subSymb = false); + SymRef newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig) { + return newSymb(fname, rsort, args, symConfig, false); + }; SymRef newSymb(char const * fname, SRef rsort, vec const & args) { - return newSymb(fname, rsort, args, SymConf::Default); + return newSymb(fname, rsort, args, SymConf::Default, false); } - SymRef newUnparsableSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig) { + SymRef newInternalSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig) { return newSymb(fname, rsort, args, symConfig, true); } bool contains(char const * fname) const { return symbolTable.has(fname); } @@ -78,6 +79,9 @@ class SymStore { vec symbols; SymbolAllocator ta{1024}; vec idToName; + + SymRef newSymb(char const * fname, SRef rsort, vec const & args, SymbolConfig const & symConfig, + bool subSymb); }; } // namespace opensmt diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index b4cd98124..b89a726fb 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -11,6 +11,7 @@ #include "CutCreator.h" #include +#include #include #include @@ -91,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.isTimesDefined(sum) || logic.isMod(logic.getPterm(sum).symb()) || - logic.isRealDiv(sum) || logic.isIntDiv(sum)); + assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimesLinOrNonlin(sum) || logic.isRealDiv(sum)); (void) cons; (void)sum; } @@ -243,7 +243,7 @@ LVRef LASolver::getVarForLeq(PTRef ref) const { } LVRef LASolver::getLAVar_single(PTRef expr_in) { - + if (logic.isTimesNonlin(expr_in) || logic.isRealDiv(expr_in)) throw NonLinException(logic.pp(expr_in)); assert(logic.isLinearTerm(expr_in)); PTId id = logic.getPterm(expr_in).getId(); @@ -287,18 +287,6 @@ std::unique_ptr 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()); - } else if(logic.isTimesLin(expr) || logic.isPlus(expr)) { - Pterm const & subterms = logic.getPterm(expr); - for(auto subterm: subterms) { - if (logic.isNonlin(subterm)) { - auto termStr = logic.pp(subterm); - throw LANonLinearException(termStr.c_str()); - } - } - } LVRef x = LVRef::Undef; if (laVarMapper.hasVar(expr)){ x = getVarForTerm(expr); @@ -310,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 bad5a03fc..eb09515b9 100644 --- a/src/tsolvers/lasolver/LASolver.h +++ b/src/tsolvers/lasolver/LASolver.h @@ -24,17 +24,6 @@ #include 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; 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)); } From adaea426005b3b18c66678d0bc09542031c8042e Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Fri, 29 Nov 2024 17:48:10 +0100 Subject: [PATCH 19/20] NonlinWork: Nonlin Real division is no longer supported --- src/api/MainSolver.cc | 4 ++-- src/logics/ArithLogic.cc | 8 +++++--- src/tsolvers/lasolver/LASolver.cc | 4 ++-- test/regression/base/arithmetic/miniexample1.smt2 | 4 ++-- test/regression/base/arithmetic/miniexample4.smt2 | 7 ------- .../base/arithmetic/miniexample4.smt2.expected.err | 0 .../base/arithmetic/miniexample4.smt2.expected.out | 1 - test/regression/base/arithmetic/miniexample4_Ok.smt2 | 8 -------- .../base/arithmetic/miniexample4_Ok.smt2.expected.err | 0 .../base/arithmetic/miniexample4_Ok.smt2.expected.out | 7 ------- 10 files changed, 11 insertions(+), 32 deletions(-) delete mode 100644 test/regression/base/arithmetic/miniexample4.smt2 delete mode 100644 test/regression/base/arithmetic/miniexample4.smt2.expected.err delete mode 100644 test/regression/base/arithmetic/miniexample4.smt2.expected.out delete mode 100644 test/regression/base/arithmetic/miniexample4_Ok.smt2 delete mode 100644 test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.err delete mode 100644 test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 2d5e93730..ee52dd518 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -337,7 +337,7 @@ sstat MainSolver::check() { sstat rval; try { rval = simplifyFormulas(); - } catch (opensmt::NonLinException const & error) { + } catch (NonLinException const & error) { reasonUnknown = error.what(); return s_Undef; } @@ -347,7 +347,7 @@ sstat MainSolver::check() { if (rval == s_Undef) { try { rval = solve(); - } catch (std::overflow_error const & error) { rval = s_Error; } catch (opensmt::NonLinException const & error) { + } catch (std::overflow_error const & error) { rval = s_Error; } catch (NonLinException const & error) { reasonUnknown = error.what(); return s_Undef; } diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 5f2079d2b..bbb30f7b0 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -2,6 +2,7 @@ #include #include +#include #include #include #include @@ -680,8 +681,7 @@ PTRef ArithLogic::mkTimes(vec && args) { if (!isTimes(s_new)) return mkFun(s_new, std::move(args)); PTRef coef = PTRef_Undef; std::vector vars; - // return mkFun(s_new, std::move(args)); - // Splitting Multiplication into constant and variable subterms + // Splitting Multiplication into constant and monomial subterms for (int i = 0; i < args.size(); i++) { if (isConstant(args[i])) { assert(coef == PTRef_Undef); @@ -863,7 +863,9 @@ PTRef ArithLogic::mkRealDiv(vec && args) { vec args_new; SymRef s_new; simp.simplify(get_sym_Real_DIV(), args, s_new, args_new); - if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])) { + // TODO: Currently creation of nonlinear Real divison is not supported + if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0]))) { + if (!isConstant(args_new[1])) throw NonLinException(pp(args[0]) + "/" + pp(args[1])); args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1])); return mkTimes(args_new); } diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index b89a726fb..5f23e93e6 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -92,7 +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.isTimesLinOrNonlin(sum) || logic.isRealDiv(sum)); + assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimesLinOrNonlin(sum)); (void) cons; (void)sum; } @@ -243,7 +243,7 @@ LVRef LASolver::getVarForLeq(PTRef ref) const { } LVRef LASolver::getLAVar_single(PTRef expr_in) { - if (logic.isTimesNonlin(expr_in) || logic.isRealDiv(expr_in)) throw NonLinException(logic.pp(expr_in)); + if (logic.isTimesNonlin(expr_in)) throw NonLinException(logic.pp(expr_in)); assert(logic.isLinearTerm(expr_in)); PTId id = logic.getPterm(expr_in).getId(); diff --git a/test/regression/base/arithmetic/miniexample1.smt2 b/test/regression/base/arithmetic/miniexample1.smt2 index 15bd69389..6915ae214 100644 --- a/test/regression/base/arithmetic/miniexample1.smt2 +++ b/test/regression/base/arithmetic/miniexample1.smt2 @@ -1,5 +1,5 @@ (set-logic QF_LRA) -(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b)) -(assert (= (uninterp_div 1 2) 0.5)) +(define-fun uninterp_div ((a Real) (b Real)) Real (* a b)) +(assert (= (uninterp_div 0.25 2) 0.5)) (check-sat) (exit) diff --git a/test/regression/base/arithmetic/miniexample4.smt2 b/test/regression/base/arithmetic/miniexample4.smt2 deleted file mode 100644 index 4f6320543..000000000 --- a/test/regression/base/arithmetic/miniexample4.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -(set-logic QF_LRA) -(declare-fun x () Real) -(declare-fun y () Real) -(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b)) -(assert (= (uninterp_div y x) 20)) -(check-sat) -(exit) diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.err b/test/regression/base/arithmetic/miniexample4.smt2.expected.err deleted file mode 100644 index e69de29bb..000000000 diff --git a/test/regression/base/arithmetic/miniexample4.smt2.expected.out b/test/regression/base/arithmetic/miniexample4.smt2.expected.out deleted file mode 100644 index 354664565..000000000 --- a/test/regression/base/arithmetic/miniexample4.smt2.expected.out +++ /dev/null @@ -1 +0,0 @@ -unknown diff --git a/test/regression/base/arithmetic/miniexample4_Ok.smt2 b/test/regression/base/arithmetic/miniexample4_Ok.smt2 deleted file mode 100644 index 83b26639b..000000000 --- a/test/regression/base/arithmetic/miniexample4_Ok.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -(set-logic QF_LRA) -(declare-fun x () Real) -(declare-fun y () Real) -(define-fun uninterp_div ((a Real) (b Real)) Real (/ a b)) -(assert (= (uninterp_div y 5) (+ 3 x))) -(check-sat) -(get-model) -(exit) diff --git a/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.err b/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.err deleted file mode 100644 index e69de29bb..000000000 diff --git a/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out b/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out deleted file mode 100644 index e009558ce..000000000 --- a/test/regression/base/arithmetic/miniexample4_Ok.smt2.expected.out +++ /dev/null @@ -1,7 +0,0 @@ -sat -( - (define-fun x () Real - 0) - (define-fun y () Real - 15) -) From cdb31643cb094245268d21ebe6e298f2733c6079 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Mon, 2 Dec 2024 15:40:16 +0100 Subject: [PATCH 20/20] NonlinWork: small fixes and optimisations --- src/logics/ArithLogic.cc | 21 ++++++++++----------- src/logics/ArithLogic.h | 3 +-- 2 files changed, 11 insertions(+), 13 deletions(-) diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index bbb30f7b0..c2ad5c794 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -415,7 +415,7 @@ lbool ArithLogic::arithmeticElimination(vec const & top_level_arith, Subs auto coeff = logic.getNumConst(c); poly.addTerm(var, std::move(coeff)); } else { - assert(logic.isPlus(polyTerm) || logic.isTimesLinOrNonlin(polyTerm)); + assert(logic.isPlus(polyTerm) || logic.isTimesNonlin(polyTerm)); for (PTRef factor : logic.getPterm(polyTerm)) { auto [var, c] = logic.splitPolyTerm(factor); auto coeff = logic.getNumConst(c); @@ -678,7 +678,7 @@ PTRef ArithLogic::mkTimes(vec && args) { args.clear(); SymRef s_new; simp.simplify(getTimesLinForSort(returnSort), flatten_args, s_new, args); - if (!isTimes(s_new)) return mkFun(s_new, std::move(args)); + if (!isTimesLinOrNonlin(s_new)) return mkFun(s_new, std::move(args)); PTRef coef = PTRef_Undef; std::vector vars; // Splitting Multiplication into constant and monomial subterms @@ -691,17 +691,15 @@ PTRef ArithLogic::mkTimes(vec && args) { vars.push_back(args[i]); } assert(!vars.empty()); - PTRef tr; if (vars.size() > 1) { if (coef == PTRef_Undef) { - tr = mkFun(getTimesNonlinForSort(returnSort), vars); + return mkFun(getTimesNonlinForSort(returnSort), vars); } else { - tr = mkFun(s_new, {coef, mkFun(getTimesNonlinForSort(returnSort), vars)}); + return mkFun(s_new, {coef, mkFun(getTimesNonlinForSort(returnSort), vars)}); } } else { - tr = mkFun(s_new, {coef, vars[0]}); + return mkFun(s_new, {coef, vars[0]}); } - return tr; } SymRef ArithLogic::getLeqForSort(SRef sr) const { @@ -859,13 +857,14 @@ PTRef ArithLogic::mkRealDiv(vec && args) { checkSortReal(args); if (args.size() != 2) { throw ApiException("Division operation requires exactly 2 arguments"); } if (isZero(args[1])) { throw ArithDivisionByZeroException(); } + if (not isConstant(args[1])) { throw NonLinException(pp(args[0]) + "/" + pp(args[1])); } SimplifyConstDiv simp(*this); vec args_new; SymRef s_new; simp.simplify(get_sym_Real_DIV(), args, s_new, args_new); - // TODO: Currently creation of nonlinear Real divison is not supported - if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0]))) { - if (!isConstant(args_new[1])) throw NonLinException(pp(args[0]) + "/" + pp(args[1])); + // TODO: Currently creation of nonlinear Real divison (with variable divisor) is not supported + if (isRealDiv(s_new)) { + assert((isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])); args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1])); return mkTimes(args_new); } @@ -1000,7 +999,7 @@ void SimplifyConst::simplify(SymRef s, vec const & args, SymRef & s_new, } // // A single argument for the operator, and the operator is identity // // in that case - if (args_new.size() == 1 && (l.isPlus(s_new) || l.isTimesLinOrNonlin(s_new))) { + if (args_new.size() == 1 && (l.isPlus(s_new) || l.isTimesLin(s_new))) { PTRef ch_tr = args_new[0]; args_new.clear(); s_new = l.getPterm(ch_tr).symb(); diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index b8b7fb6c8..f2d187ff2 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -389,8 +389,7 @@ class ArithLogic : public Logic { PTRef mkBinaryLt(PTRef lhs, PTRef rhs) { return mkNot(mkBinaryGeq(lhs, rhs)); } PTRef mkBinaryGt(PTRef lhs, PTRef rhs) { return mkNot(mkBinaryLeq(lhs, rhs)); } SymRef declareFun_Multiplication_LinNonlin(std::string const & s, SRef rsort, vec const & args) { - SymRef sr = sym_store.newInternalSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc); - return sr; + return sym_store.newInternalSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc); } PTRef mkBinaryEq(PTRef lhs, PTRef rhs) override; pair sumToNormalizedPair(PTRef sum);