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 6a3e16491..c2d1eff55 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -182,10 +182,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; } @@ -226,7 +222,6 @@ pair> ArithLogic::getConstantAndFactors(PTRef sum) const { assert(constant == PTRef_Undef); constant = arg; } else { - // assert(isLinearFactor(arg) || isNonlinearFactor(arg)); varFactors.push(arg); } } @@ -237,12 +232,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)) { @@ -506,9 +495,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 { @@ -561,7 +549,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)}); } @@ -633,6 +620,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); @@ -703,12 +691,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 { @@ -848,7 +831,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); } @@ -869,18 +851,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 d2375f54d..f19a915ab 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());