NonlinWork: PR cleanup

usi-verification-and-security · Oct 31, 2024 · b300ed9 · b300ed9
1 parent 1518467
commit b300ed9
Show file tree

Hide file tree

Showing 7 changed files with 6 additions and 58 deletions.
diff --git 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<PTRef>&& 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
@@ -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
@@ -108,7 +108,8 @@ class MainSolver {
     vec<PTRef> const & getAssertionsAtCurrentLevel() const { return getAssertionsAtLevel(getAssertionLevel()); }
     vec<PTRef> 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
@@ -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<Number, vec<PTRef>> 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<Number, vec<PTRef>> ArithLogic::getConstantAndFactors(PTRef sum) const {
     return {std::move(constantValue), std::move(varFactors)};
 }
 
-pair<PTRef, PTRef> ArithLogic::splitTerm(PTRef term) const {
-    PTRef fac = getPterm(term)[0];
-    PTRef var = getPterm(term)[1];
-    return {var, fac};
-}
-
 pair<PTRef, PTRef> ArithLogic::splitTermToVarAndConst(PTRef term) const {
     assert(isTimes(term) || isNumVarLike(term) || isConstant(term));
     if (isTimes(term)) {
@@ -506,9 +495,8 @@ pair<lbool, Logic::SubstMap> ArithLogic::retrieveSubstitutions(vec<PtAsgn> 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<PTRef> && args) {
     };
     std::vector<Entry> 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<PTRef> && 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<PTRef> && 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<PTRef> && 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<PTRef> 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
@@ -8,16 +8,6 @@
 #include <numeric>
 
 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<PTRef, PTRef> 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
@@ -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
@@ -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());