NonlinWork: added new functions, rework of the accessible parts

Author: BritikovKI

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]),

src/logics/Logic.cc

@@ -728,11 +728,11 @@ PTRef Logic::mkSelect(vec<PTRef> && args) {
 }
 
 SymRef Logic::declareFun(std::string const & fname, SRef rsort, vec<SRef> 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;
 }
 

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<SRef> const & args, SymbolConfig const & symbolConfig,
-                      bool duplicate = false);
+    SymRef declareFun(std::string const & fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symbolConfig);
     SymRef declareFun(std::string const & fname, SRef rsort, vec<SRef> 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<SRef> const & args) {
         return declareFun(s, rsort, args, SymConf::NoScopingPairwise);
     }
-    SymRef declareFun_Commutative_NoScoping_LeftAssoc(std::string const & s, SRef rsort, vec<SRef> 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<SRef> const & args) {
+        return declareFun(s, rsort, args, SymConf::CommutativeNoScopingLeftAssoc);
+    }
+    SymRef declareFun_Multiplication_Duplicate(std::string const & s, SRef rsort, vec<SRef> 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<SRef> const & args) {
         return declareFun(s, rsort, args, SymConf::CommutativeNoScopingChainable);

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<SRef> const & args, SymbolConfig const & symConfig,
                    bool subSymb = false);
     SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args) {
         return newSymb(fname, rsort, args, SymConf::Default);
     }
+    SymRef newUnparsableSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig) {
+        return newSymb(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]; }
     vec<SymRef> & nameToRef(char const * s) { return symbolTable[s]; }