NonlinWork: review fixes

Author: BritikovKI

src/common/NonLinException.h

@@ -7,16 +7,12 @@
 #ifndef OPENSMT_NONLINEXCEPTION_H
 #define OPENSMT_NONLINEXCEPTION_H
 
+#include <stdexcept>
+
 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;
+    NonLinException(std::string_view const reason_) : runtime_error("Term " + std::string(reason_) + " is non-linear"){}
 };
 }
 

src/logics/ArithLogic.cc

@@ -115,8 +115,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_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_TIMES_LIN(declareFunMultiplicationLinNonlin(tk_real_times, sort_REAL, {sort_REAL, sort_REAL})),
+      sym_Real_TIMES_NONLIN(declareFunMultiplicationLinNonlin(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})),
@@ -137,8 +137,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_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_TIMES_LIN(declareFunMultiplicationLinNonlin(tk_int_times, sort_INT, {sort_INT, sort_INT})),
+      sym_Int_TIMES_NONLIN(declareFunMultiplicationLinNonlin(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]),

src/logics/ArithLogic.h

@@ -228,6 +228,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()); }
+    // isMonomial property is related to PTRef only
     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);
@@ -388,14 +389,15 @@ 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<SRef> const & args) {
-        return sym_store.newInternalSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc);
-    }
     PTRef mkBinaryEq(PTRef lhs, PTRef rhs) override;
     pair<Number, PTRef> sumToNormalizedPair(PTRef sum);
     pair<Number, PTRef> sumToNormalizedIntPair(PTRef sum);
     pair<Number, PTRef> sumToNormalizedRealPair(PTRef sum);
 
+    SymRef declareFunMultiplicationLinNonlin(std::string const & s, SRef rsort, vec<SRef> const & args) {
+        return sym_store.newInternalSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc);
+    }
+
     bool hasNegativeLeadingVariable(PTRef poly) const;
 
     std::vector<Number *> numbers;

src/rewriters/DivModRewriter.h

@@ -37,7 +37,7 @@ class DivModConfig : public DefaultRewriterConfig {
             PTRef modVar = divMod.mod;
             PTRef rewritten = logic.isIntDiv(symRef) ? divVar : modVar;
             if (not inCache) {
-                if (!logic.isConstant(divisor)) throw NonLinException(logic.pp(term));
+                if (not logic.isConstant(divisor)) { throw NonLinException(logic.pp(term)); }
                 // collect the definitions to add
                 assert(logic.isConstant(divisor));
                 auto divisorVal = logic.getNumConst(divisor);

src/symbols/SymStore.cc

@@ -39,12 +39,12 @@ SymStore::~SymStore() {
         free(idToName[i]);
 }
 
-SymRef SymStore::newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
-                         bool subSymb) {
+SymRef SymStore::newSymbImpl(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
+                             bool isInternal) {
     // Check if there already is a term called fname with same number of arguments of the same sort
     auto * symrefs = getRefOrNull(fname);
 
-    if (symrefs && !subSymb) {
+    if (symrefs && !isInternal) {
         vec<SymRef> 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<SRef> const & args,
         vec<SymRef> trs;
         trs.push(tr);
         symbolTable.insert(tmp_name, trs);
-    } else if (!subSymb) {
+    } else if (!isInternal) {
         symbolTable[tmp_name].push(tr); // Map the name to term reference (why not id?), used in parsing
     }
     return tr;

src/symbols/SymStore.h

@@ -42,13 +42,13 @@ class SymStore {
     // Constructs a new symbol.
 
     SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig) {
-        return newSymb(fname, rsort, args, symConfig, false);
+        return newSymbImpl(fname, rsort, args, symConfig, false);
     };
     SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args) {
-        return newSymb(fname, rsort, args, SymConf::Default, false);
+        return newSymbImpl(fname, rsort, args, SymConf::Default, false);
     }
     SymRef newInternalSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig) {
-        return newSymb(fname, rsort, args, symConfig, true);
+        return newSymbImpl(fname, rsort, args, symConfig, true);
     }
     bool contains(char const * fname) const { return symbolTable.has(fname); }
     vec<SymRef> const & nameToRef(char const * s) const { return symbolTable[s]; }
@@ -80,8 +80,8 @@ class SymStore {
     SymbolAllocator ta{1024};
     vec<char *> idToName;
 
-    SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
-                   bool subSymb);
+    SymRef newSymbImpl(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
+                       bool isInternal);
 };
 } // namespace opensmt
 

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));
+    assert(logic.isPlus(sum) or logic.isTimesLin(sum) or logic.isMonomial(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)) 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();
 
@@ -298,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);
-        x = getLAVar_single(v);
         assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v))));
+        x = getLAVar_single(v);
         simplex.newNonbasicVar(x);
         notifyVar(x);
     }