simplify mkSkolem naming system: don't use $$

Short summary: By default NODEID is appeneded, just continue doing what you
were, just don't add the _$$ at the end.

Long summary:

Before this commit there were four (yes!) ways to specify the names for new
skolems, which result in names as given below

1) mkSkolem("name", ..., SKOLEM_FLAG_DEFAULT)  -> "name_NODEID"
2) mkSkolem("name", ..., SKOLEM_EXACT_NAME)  -> "name"
3) mkSkolem("name_$$", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID"
4) mkSkolem("na_$$_me", ..., SKOLEM_FLAG_DEFAULT) -> "na_NODEID_me"

After this commit, only 1) and 2) stay.

90% usage is of 1) or 3), which results in exact same behavior (and
looking at the source code it doesn't look like everyone realized that
the _$$ is just redundant).

Almost no one used 4), which is the only reason to even have $$. Post this
commit if you really want a number in the middle, manually construct the
name and use the SKOLEM_EXACT_NAME flag.

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 22c47da59bc83454e6f49c5c9f8430f877a0c129..ecd3df084804b766851fdba89ba00d5fd4c64811 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -304,26 +304,16 @@ TypeNode NodeManager::getType(TNode n, bool check)
   return typeNode;
 }
 
-Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type, const std::string& comment, int flags) {
+Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, int flags) {
   Node n = NodeBuilder<0>(this, kind::SKOLEM);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   if((flags & SKOLEM_EXACT_NAME) == 0) {
-    size_t pos = name.find("$$");
-    if(pos != string::npos) {
-      // replace a "$$" with the node ID
-      stringstream id;
-      id << n.getId();
-      string newName = name;
-      newName.replace(pos, 2, id.str());
-      setAttribute(n, expr::VarNameAttr(), newName);
-    } else {
-      stringstream newName;
-      newName << name << '_' << n.getId();
-      setAttribute(n, expr::VarNameAttr(), newName.str());
-    }
+    stringstream name;
+    name << prefix << '_' << n.getId();
+    setAttribute(n, expr::VarNameAttr(), name.str());
   } else {
-    setAttribute(n, expr::VarNameAttr(), name);
+    setAttribute(n, expr::VarNameAttr(), prefix);
   }
   if((flags & SKOLEM_NO_NOTIFY) == 0) {
     for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 15c49efd80cb1cf15068dbd9f6954b2b1ca22c45..f533d3ab9e8f6cf98e840be46bf704352182e4c9 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -424,12 +424,11 @@ public:
   /**
    * Create a skolem constant with the given name, type, and comment.
    *
-   * @param name the name of the new skolem variable.  This name can
-   * contain the special character sequence "$$", in which case the
-   * $$ is replaced with the Node ID.  That way a family of skolem
-   * variables can be made with unique identifiers, used in dump,
-   * tracing, and debugging output.  By convention, you should probably
-   * call mkSkolem() with a custom name appended with "_$$".
+   * @param prefix the name of the new skolem variable is the prefix
+   * appended with the Node ID.  This way a family of skolem variables
+   * can be made with unique identifiers, used in dump, tracing, and
+   * debugging output.  Use SKOLEM_EXECT_NAME flag if you don't want
+   * Node ID appended and use prefix as the name.
    *
    * @param type the type of the skolem variable to create
    *
@@ -440,7 +439,7 @@ public:
    * @param flags an optional mask of bits from SkolemFlags to control
    * mkSkolem() behavior
    */
-  Node mkSkolem(const std::string& name, const TypeNode& type,
+  Node mkSkolem(const std::string& prefix, const TypeNode& type,
                 const std::string& comment = "", int flags = SKOLEM_DEFAULT);
 
   /** Create a instantiation constant with the given type. */

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 4f182fb691af8b6d053c739465ea24ddd3f1e6fa..d5dcae72633e82176998c30d6f6259c5217fd561 100644 (file)
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -418,7 +418,7 @@ bool ArithIteUtils::solveBinOr(TNode binor){
 
         Node cnd = findIteCnd(binor[0], binor[1]);
 
-        Node sk = nm->mkSkolem("deor$$", nm->booleanType());
+        Node sk = nm->mkSkolem("deor", nm->booleanType());
         Node ite = sk.iteNode(otherL, otherR);
         d_skolems.insert(sk, cnd);
         d_skolemsAdded.push_back(sk);

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a63de446c56d9e2507974094725baa297b0d60e5..0c8ca7507b4e78c2c0a7052f318febc708912029 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -226,7 +226,7 @@ Node TheoryArithPrivate::getRealDivideBy0Func(){
 
   if(d_realDivideBy0Func.isNull()){
     TypeNode realType = NodeManager::currentNM()->realType();
-    d_realDivideBy0Func = skolemFunction("/by0_$$", realType, realType);
+    d_realDivideBy0Func = skolemFunction("/by0", realType, realType);
   }
   return d_realDivideBy0Func;
 }
@@ -237,7 +237,7 @@ Node TheoryArithPrivate::getIntDivideBy0Func(){
 
   if(d_intDivideBy0Func.isNull()){
     TypeNode intType = NodeManager::currentNM()->integerType();
-    d_intDivideBy0Func = skolemFunction("divby0_$$", intType, intType);
+    d_intDivideBy0Func = skolemFunction("divby0", intType, intType);
   }
   return d_intDivideBy0Func;
 }
@@ -248,7 +248,7 @@ Node TheoryArithPrivate::getIntModulusBy0Func(){
 
   if(d_intModulusBy0Func.isNull()){
     TypeNode intType = NodeManager::currentNM()->integerType();
-    d_intModulusBy0Func = skolemFunction("modby0_$$", intType, intType);
+    d_intModulusBy0Func = skolemFunction("modby0", intType, intType);
   }
   return d_intModulusBy0Func;
 }
@@ -1498,7 +1498,7 @@ Node TheoryArithPrivate::axiomIteForTotalIntDivision(Node int_div_like){
   Polynomial qp = Polynomial::parsePolynomial(q);
 
   Node abs_d = (n.isConstant()) ?
-    d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$");
+    d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs");
 
   Node eq = Comparison::mkComparison(EQUAL, n, d * qp + rp).getNode();
   Node leq0 = currNM->mkNode(LEQ, zero, r);

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index cd9fd249743d385ede1d3652c288e870501b4e82..8aad6788307e702268779e30c4dcddd669a11bfe 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -845,7 +845,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
     else {
       std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
       if (it == d_skolemCache.end()) {
-        rep = nm->mkSkolem("array_collect_model_var_$$", n.getType(), "base model variable for array collectModelInfo");
+        rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo");
         d_skolemCache[n] = rep;
       }
       else {
@@ -963,7 +963,7 @@ void TheoryArrays::check(Effort e) {
           if(fact[0][0].getType().isArray() && !d_conflict) {
             NodeManager* nm = NodeManager::currentNM();
             TypeNode indexType = fact[0][0].getType()[0];
-            TNode k = getSkolem(fact,"array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays", false);
+            TNode k = getSkolem(fact,"array_ext_index", indexType, "an extensional lemma index variable from the theory of arrays", false);
 
             Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
             Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
@@ -1574,18 +1574,18 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain,
       }
 
       // Solve equation for s: select(s,index) op val --> s = store(s',i',v') /\ index = i' /\ v' op val
-      Node newVarArr = getSkolem(s, "array_model_arr_var_$$", s.getType(), "a new array variable from the theory of arrays", false);
+      Node newVarArr = getSkolem(s, "array_model_arr_var", s.getType(), "a new array variable from the theory of arrays", false);
       Assert(d_infoMap.getModelRep(d_equalityEngine.getRepresentative(newVarArr)).isNull());
       Node lookup;
       bool checkIndex1 = false, checkIndex2 = false, checkIndex3 = false;
       if (!isLeaf(index)) {
-        index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays");
+        index = getSkolem(index, "array_model_index", index.getType(), "a new index variable from the theory of arrays");
         if (!index.getType().isArray()) {
           checkIndex1 = true;
         }
       }
       lookup = nm->mkNode(kind::SELECT, s, index);
-      Node newVarVal = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false);
+      Node newVarVal = getSkolem(lookup, "array_model_var", val.getType(), "a new value variable from the theory of arrays", false);
 
       Node newVarVal2;
       Node index2;
@@ -1594,7 +1594,7 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain,
         // Special case: select(s,index) = select(s,j): solution becomes s = store(store(s',j,v'),index,w') /\ v' = w'
         index2 = val[1];
         if (!isLeaf(index2)) {
-          index2 = getSkolem(val, "array_model_index_$$", index2.getType(), "a new index variable from the theory of arrays");
+          index2 = getSkolem(val, "array_model_index", index2.getType(), "a new index variable from the theory of arrays");
           if (!index2.getType().isArray()) {
             checkIndex2 = true;
           }
@@ -1603,7 +1603,7 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain,
           checkIndex3 = true;
         }
         lookup = nm->mkNode(kind::SELECT, s, index2);
-        newVarVal2 = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false);
+        newVarVal2 = getSkolem(lookup, "array_model_var", val.getType(), "a new value variable from the theory of arrays", false);
         newVarArr = nm->mkNode(kind::STORE, newVarArr, index2, newVarVal2);
         preRegisterTermInternal(newVarArr);
         val = newVarVal2;
@@ -1927,7 +1927,7 @@ Node TheoryArrays::removeRepLoops(TNode a, TNode rep)
   // TODO: Change to hasLoop?
   if (!isLeaf(index)) {
     changed = true;
-    index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays", false);
+    index = getSkolem(index, "array_model_index", index.getType(), "a new index variable from the theory of arrays", false);
     if (!d_equalityEngine.hasTerm(index) ||
         !d_equalityEngine.hasTerm(rep[1]) ||
         !d_equalityEngine.areEqual(rep[1], index)) {
@@ -1939,7 +1939,7 @@ Node TheoryArrays::removeRepLoops(TNode a, TNode rep)
   }
   if (!isLeaf(value)) {
     changed = true;
-    value = getSkolem(value, "array_model_var_$$", value.getType(), "a new value variable from the theory of arrays", false);
+    value = getSkolem(value, "array_model_var", value.getType(), "a new value variable from the theory of arrays", false);
     if (!d_equalityEngine.hasTerm(value) ||
         !d_equalityEngine.hasTerm(rep[2]) ||
         !d_equalityEngine.areEqual(rep[2], value)) {

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index c7143bdeb7d40c2e03d608c27fd8c7123bd399c3..0ebcb31e8764398bf2995d12ce08d4641f5e73a3 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -227,7 +227,7 @@ public:
   }
   inline static Node mkGroundTerm(TypeNode type) {
     Assert(type.getKind() == kind::SORT_TYPE);
-    return NodeManager::currentNM()->mkSkolem("groundTerm_$$", type, "a ground term created for type " + type.toString());
+    return NodeManager::currentNM()->mkSkolem("groundTerm", type, "a ground term created for type " + type.toString());
   }
 };/* class SortProperties */
 

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index f35fc28966acb4f22a8aafc6375504c2269328cc..95136598c13526c2160f55b6d9472490ee240a67 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -65,7 +65,7 @@ inline Node mkFalse() {
 
 inline Node mkVar(unsigned size) {
   NodeManager* nm =  NodeManager::currentNM();
-  return nm->mkSkolem("bv_$$", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors"); 
+  return nm->mkSkolem("bv", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors"); 
 }
 
 

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 0c6842222af1aae8409fd16b33cae41f12eea9b6..8396e563ec59884b7d8fc9d5fc4c38a9b9b25bbe 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1107,7 +1107,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index,
         if( dt.isParametric() ){
           tn = TypeNode::fromType( tspec )[i];
         }
-        nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created during model gen" );
+        nc = NodeManager::currentNM()->mkSkolem( "m", tn, "created during model gen" );
       }
       children.push_back( nc );
       if( isActive ){

diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index a4af4f26fc8aa5a163e545a77aaf1d6897ca5084..35330f81a4096b76dd82c222c0a6b7a65ac24fc2 100644 (file)
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -307,7 +307,7 @@ Node ITECompressor::push_back_boolean(Node original, Node compressed){
     return rewritten;
   }else{
     NodeManager* nm = NodeManager::currentNM();
-    Node skolem = nm->mkSkolem("compress_$$", nm->booleanType());
+    Node skolem = nm->mkSkolem("compress", nm->booleanType());
     d_compressed[rewritten] = skolem;
     d_compressed[original] = skolem;
     d_compressed[compressed] = skolem;
@@ -1175,7 +1175,7 @@ Node ITESimplifier::getSimpVar(TypeNode t)
     return (*it).second;
   }
   else {
-    Node var = NodeManager::currentNM()->mkSkolem("iteSimp_$$", t, "is a variable resulting from ITE simplification");
+    Node var = NodeManager::currentNM()->mkSkolem("iteSimp", t, "is a variable resulting from ITE simplification");
     d_simpVars[t] = var;
     return var;
   }

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index bec8ea3502fb3ae048f084bd2cb1aa53b6846834..a294eec5ae544d49136da6f123221e5319bf4691 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -277,7 +277,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
         Node r = d_range[f][v];
         if( r.hasBoundVar() ){
           //introduce a new bound
-          Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );
+          Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" );
           d_nground_range[f][v] = d_range[f][v];
           d_range[f][v] = new_range;
           r = new_range;

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index f3203da4bb1a9744d7fc116f965ad199bd1975f9..d815e0ee8dc1a2c579d16e729a06cc51acafcc81 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -585,7 +585,7 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) {
         types.push_back(NodeManager::currentNM()->integerType());
       }
       TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() );
-      intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" );
+      intervalOp = NodeManager::currentNM()->mkSkolem( "interval", typ, "op representing interval" );
     }
     for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
       it->second->reset();
@@ -611,7 +611,7 @@ bool FirstOrderModelFmc::isStar(Node n) {
 Node FirstOrderModelFmc::getStar(TypeNode tn) {
   std::map<TypeNode, Node >::iterator it = d_type_star.find( tn );
   if( it==d_type_star.end() ){
-    Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );
+    Node st = NodeManager::currentNM()->mkSkolem( "star", tn, "skolem created for full-model checking" );
     d_type_star[tn] = st;
     st.setAttribute(IsStarAttribute(), true );
     return st;

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 6c889781d3e00f47e112fe761bfbbc91020a33de..3b6c8e492fa6b06a61e6b8c4bad21f7558759b57 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -591,7 +591,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
           types.push_back(f[0][i].getType());
         }
         TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );
-        Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );
+        Node op = NodeManager::currentNM()->mkSkolem( "fmc", typ, "op created for full-model checking" );
         d_quant_cond[f] = op;
       }
       //make sure all types are set
@@ -1267,7 +1267,7 @@ Node FullModelChecker::mkArrayCond( Node a ) {
   if( d_array_term_cond.find(a)==d_array_term_cond.end() ){
     if( d_array_cond.find(a.getType())==d_array_cond.end() ){
       TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() );
-      Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );
+      Node op = NodeManager::currentNM()->mkSkolem( "fmc", typ, "op created for full-model checking" );
       d_array_cond[a.getType()] = op;
     }
     std::vector< Node > cond;

diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 435bf7221708c5c0b1af07491ff5c8bd072d72c4..72d42cf4bc01c46b0638cef5e4882c2793f6dd8d 100644 (file)
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -51,7 +51,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
         //if value is null, must generate it
         if( val.isNull() ){
           std::stringstream ss;
-          ss << "mdo_" << it->first << "_$$";
+          ss << "mdo_" << it->first << "";
           Node op = NodeManager::currentNM()->mkSkolem( ss.str(), it->first.getType(), "op created during macro definitions" );
           //will be defined in terms of fresh operator
           std::vector< Node > children;
@@ -273,7 +273,7 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
               if( d_macro_basis[op].empty() ){
                 for( size_t a=0; a<m.getNumChildren(); a++ ){
                   std::stringstream ss;
-                  ss << "mda_" << op << "_$$";
+                  ss << "mda_" << op << "";
                   Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
                   d_macro_basis[op].push_back( v );
                 }

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index a079dbaab3522f47f2adc975e9ecc584742517ad..6af42e1593fb901fa25515850812d942a5fa6d64 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1154,11 +1154,11 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
       for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
         //make the new function symbol
         if( argTypes.empty() ){
-          Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" );
+          Node s = NodeManager::currentNM()->mkSkolem( "sk", n[0][i].getType(), "created during pre-skolemization" );
           subs.push_back( s );
         }else{
           TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
-          Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
+          Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
           //DOTHIS: set attribute on op, marking that it should not be selected as trigger
           vector< Node > funcArgs;
           funcArgs.push_back( op );

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ea1231e7a67589ed59e10bd9619389a9aedbdc9d..cf183dd1861288ad140b205bbb7484ab96146e9f 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -413,7 +413,7 @@ Node TermDb::getSkolemizedBody( Node f ){
   if( d_skolem_body.find( f )==d_skolem_body.end() ){
     std::vector< Node > vars;
     for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
-      Node skv = NodeManager::currentNM()->mkSkolem( "skv_$$", f[0][i].getType(), "is a termdb-created skolemized body" );
+      Node skv = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "is a termdb-created skolemized body" );
       d_skolem_constants[ f ].push_back( skv );
       vars.push_back( f[0][i] );
       //carry information for sort inference
@@ -441,7 +441,7 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){
         Rational z(0);
         d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
       }else{
-           d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar_$$", tn, "is a free variable created by termdb" );
+           d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" );
            Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl;
       }
     }

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 169688243b2ae1fe63ce001672bb4a96ca74ff0d..2e8eb51b1e3bace9afbf112d095baf0c6b04cac6 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -141,7 +141,7 @@ bool RepSetIterator::initialize(){
     TypeNode tn = d_types[i];
     if( tn.isSort() ){
       if( !d_rep_set->hasType( tn ) ){
-        Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" );
+        Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" );
         Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
         d_rep_set->add( var );
       }

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index d719b4e1a10be12077477cd724f5ccdc5fcb5f37..8c07b679da0fe723aedea177d0dff2d2c3502fb6 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -296,7 +296,7 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) {
                                                }\r
                                        }\r
                                        if(ret == 0) {\r
-                                               Node sk = NodeManager::currentNM()->mkSkolem( "rsp_$$", NodeManager::currentNM()->stringType(), "Split RegExp" );\r
+                                               Node sk = NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" );\r
                                                retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk);\r
                                                if(!rest.isNull()) {\r
                                                        retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest));\r
@@ -1038,7 +1038,7 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
                                                emptyflag = true;\r
                                                break;\r
                                        } else {\r
-                                               Node sk = NodeManager::currentNM()->mkSkolem( "rc_$$", s.getType(), "created for regular expression concat" );\r
+                                               Node sk = NodeManager::currentNM()->mkSkolem( "rc", s.getType(), "created for regular expression concat" );\r
                                                Node lem = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk, r[i]);\r
                                                nvec.push_back(lem);\r
                                                cc.push_back(sk);\r
@@ -1098,8 +1098,8 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
                                } else {\r
                                        Node se = s.eqNode(d_emptyString);\r
                                        Node sinr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[0]);\r
-                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );\r
-                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );\r
+                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" );\r
+                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" );\r
                                        Node s1nz = sk1.eqNode(d_emptyString).negate();\r
                                        Node s2nz = sk2.eqNode(d_emptyString).negate();\r
                                        Node s1inr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk1, r[0]);\r

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f2172071de80a594319ac56274ed7626fc8ff558..ac5a97167cf9efa310c0f30cc3dde13348b1b46d 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -427,8 +427,8 @@ void TheoryStrings::preRegisterTerm(TNode n) {
                Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
                Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
                Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
                d_statistics.d_new_skolems += 2;
                Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
                Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
@@ -1091,9 +1091,9 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
                        } else {
                                Trace("strings-loop") << "Strings::Loop: Normal Breaking." << std::endl;
                                //right
-                               Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
-                               Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
-                               Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
+                               Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
+                               Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
+                               Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
                                d_statistics.d_new_skolems += 3;
                                //t1 * ... * tn = y * z
                                Node conc1 = t_yz.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
@@ -1236,7 +1236,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                                NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
                                                                        //split the string
                                                                        Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
-                                                                       Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false );
+                                                                       Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false );
                                                                        d_pending_req_phase[ eq1 ] = true;
                                                                        conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
                                                                        Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
@@ -1267,8 +1267,8 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                                }
                                                                        }
 
-                                                                       Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true );
-                                                                       Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true );
+                                                                       Node eq1 = mkSplitEq( "v_spt_l", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true );
+                                                                       Node eq2 = mkSplitEq( "v_spt_r", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true );
                                                                        conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
 
                                                                        Node ant = mkExplain( antec, antec_new_lits );
@@ -1569,9 +1569,9 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
                                                }
                                                antec_new_lits.push_back( li.eqNode( lj ).negate() );
                                                std::vector< Node > conc;
-                                               Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" );
-                                               Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" );
-                                               Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" );
+                                               Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit", ni.getType(), "created for disequality normalization" );
+                                               Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit", ni.getType(), "created for disequality normalization" );
+                                               Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit", ni.getType(), "created for disequality normalization" );
                                                d_statistics.d_new_skolems += 3;
                                                //Node nemp = sk1.eqNode(d_emptyString).negate();
                                                //conc.push_back(nemp);
@@ -1894,7 +1894,7 @@ bool TheoryStrings::checkSimple() {
                                        Node sk;
                                        //if( d_length_inst.find(n)==d_length_inst.end() ) {
                                                //Node nr = d_equalityEngine.getRepresentative( n );
-                                               sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" );
+                                               sk = NodeManager::currentNM()->mkSkolem( "lsym", n.getType(), "created for length" );
                                                d_statistics.d_new_skolems += 1;
                                                d_length_intro_vars.insert( sk );
                                                Node eq = sk.eqNode(n);
@@ -2481,10 +2481,10 @@ bool TheoryStrings::checkMemberships() {
                                                }else{
                                                        Trace("strings-regexp-debug") << "Case 2\n";
                                                        std::vector< Node > conc_c;
-                                                       Node s11 = NodeManager::currentNM()->mkSkolem( "s11_$$", NodeManager::currentNM()->stringType(), "created for re" );
-                                                       Node s12 = NodeManager::currentNM()->mkSkolem( "s12_$$", NodeManager::currentNM()->stringType(), "created for re" );
-                                                       Node s21 = NodeManager::currentNM()->mkSkolem( "s21_$$", NodeManager::currentNM()->stringType(), "created for re" );
-                                                       Node s22 = NodeManager::currentNM()->mkSkolem( "s22_$$", NodeManager::currentNM()->stringType(), "created for re" );
+                                                       Node s11 = NodeManager::currentNM()->mkSkolem( "s11", NodeManager::currentNM()->stringType(), "created for re" );
+                                                       Node s12 = NodeManager::currentNM()->mkSkolem( "s12", NodeManager::currentNM()->stringType(), "created for re" );
+                                                       Node s21 = NodeManager::currentNM()->mkSkolem( "s21", NodeManager::currentNM()->stringType(), "created for re" );
+                                                       Node s22 = NodeManager::currentNM()->mkSkolem( "s22", NodeManager::currentNM()->stringType(), "created for re" );
                                                        conc = p1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s11, s12));
                                                        conc_c.push_back(conc);
                                                        conc = p2.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s21, s22));
@@ -2650,8 +2650,8 @@ bool TheoryStrings::checkPosContains() {
                        Node s = atom[1];
                        if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
                                if(d_pos_ctn_cached.find(atom) == d_pos_ctn_cached.end()) {
-                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for contain" );
-                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for contain" );
+                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1", s.getType(), "created for contain" );
+                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2", s.getType(), "created for contain" );
                                        d_statistics.d_new_skolems += 2;
                                        Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
                                        sendLemma( atom, eq, "POS-INC" );

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1b040f71c1d75b7706df1bfd913e7dee79cd7b5d..85ab73691bda24ab0f9f1aff1937eb2c0fa73312 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -184,8 +184,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
                Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero);
                Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
                Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) );
                Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
                Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, 
@@ -196,11 +196,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                d_cache[t] = t;
        } else if( t.getKind() == kind::STRING_STRIDOF ) {
                if(options::stringExp()) {
-                       Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" );
-                       Node sk2 = NodeManager::currentNM()->mkSkolem( "io2_$$", t[0].getType(), "created for indexof" );
-                       Node sk3 = NodeManager::currentNM()->mkSkolem( "io3_$$", t[0].getType(), "created for indexof" );
-                       Node sk4 = NodeManager::currentNM()->mkSkolem( "io4_$$", t[0].getType(), "created for indexof" );
-                       Node skk = NodeManager::currentNM()->mkSkolem( "iok_$$", t[2].getType(), "created for indexof" );
+                       Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", t[0].getType(), "created for indexof" );
+                       Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", t[0].getType(), "created for indexof" );
+                       Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", t[0].getType(), "created for indexof" );
+                       Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", t[0].getType(), "created for indexof" );
+                       Node skk = NodeManager::currentNM()->mkSkolem( "iok", t[2].getType(), "created for indexof" );
                        Node eq = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3, sk4 ) );
                        new_nodes.push_back( eq );
                        Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
@@ -274,11 +274,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        
                        std::vector< TypeNode > argTypes;
                        argTypes.push_back(NodeManager::currentNM()->integerType());
-                       Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$", 
+                       Node ufP = NodeManager::currentNM()->mkSkolem("ufP", 
                                                                NodeManager::currentNM()->mkFunctionType(
                                                                        argTypes, NodeManager::currentNM()->integerType()),
                                                                "uf type conv P");
-                       Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", 
+                       Node ufM = NodeManager::currentNM()->mkSkolem("ufM", 
                                                                NodeManager::currentNM()->mkFunctionType(
                                                                        argTypes, NodeManager::currentNM()->integerType()),
                                                                "uf type conv M");
@@ -368,11 +368,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
                        std::vector< TypeNode > argTypes;
                        argTypes.push_back(NodeManager::currentNM()->integerType());
-                       Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$", 
+                       Node ufP = NodeManager::currentNM()->mkSkolem("ufP", 
                                                                NodeManager::currentNM()->mkFunctionType(
                                                                        argTypes, NodeManager::currentNM()->integerType()),
                                                                "uf type conv P");
-                       Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", 
+                       Node ufM = NodeManager::currentNM()->mkSkolem("ufM", 
                                                                NodeManager::currentNM()->mkFunctionType(
                                                                        argTypes, NodeManager::currentNM()->integerType()),
                                                                "uf type conv M");
@@ -404,9 +404,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
                        //cc2
                        std::vector< Node > vec_n;
-                       Node z1 = NodeManager::currentNM()->mkSkolem("z1_$$", NodeManager::currentNM()->stringType());
-                       Node z2 = NodeManager::currentNM()->mkSkolem("z2_$$", NodeManager::currentNM()->stringType());
-                       Node z3 = NodeManager::currentNM()->mkSkolem("z3_$$", NodeManager::currentNM()->stringType());
+                       Node z1 = NodeManager::currentNM()->mkSkolem("z1", NodeManager::currentNM()->stringType());
+                       Node z2 = NodeManager::currentNM()->mkSkolem("z2", NodeManager::currentNM()->stringType());
+                       Node z3 = NodeManager::currentNM()->mkSkolem("z3", NodeManager::currentNM()->stringType());
                        Node g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
                        vec_n.push_back(g);
                        g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
@@ -499,9 +499,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        Node x = t[0];
                        Node y = t[1];
                        Node z = t[2];
-                       Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1_$$", t[0].getType(), "created for replace" );
-                       Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2_$$", t[0].getType(), "created for replace" );
-                       Node skw = NodeManager::currentNM()->mkSkolem( "rpw_$$", t[0].getType(), "created for replace" );
+                       Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" );
+                       Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" );
+                       Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" );
                        Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
                        Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
                        Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 1157886396e5148b29439b51e72eccc244556e82..7509c7f4f2624d52fefa64c2dca3ab7690384591 100644 (file)
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -92,7 +92,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
 
 Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var)
 {
-  Node n = NodeManager::currentNM()->mkSkolem("unconstrained_$$", t, "a new var introduced because of unconstrained variable " + var.toString());
+  Node n = NodeManager::currentNM()->mkSkolem("unconstrained", t, "a new var introduced because of unconstrained variable " + var.toString());
   return n;
 }
 

diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 1b29f9ef8649b637da10741f46b7500f5b83f99b..f1dce413c4706d078721070af52c1f86eccecc7c 100644 (file)
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -93,7 +93,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
     if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
       Node skolem;
       // Make the skolem to represent the ITE
-      skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
+      skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal");
 
       // The new assertion
       Node newAssertion =

diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 682e1e1e73c242419f5d2bd0f05000e782644f11..ce12b59f12ff255e9861ee76fd8d797624a44f13 100644 (file)
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -504,7 +504,7 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){
     return NodeManager::currentNM()->mkBoundVar( ss.str(), tn );
   }else{
     std::stringstream ss;
-    ss << "i_$$_" << old;
+    ss << "i_" << old;
     return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" );
   }
 }
@@ -576,7 +576,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
       }
       if( opChanged ){
         std::stringstream ss;
-        ss << "io_$$_" << op;
+        ss << "io_" << op;
         TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType );
         d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" );
       }else{
@@ -622,7 +622,7 @@ Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) {
   std::vector< TypeNode > tns;
   tns.push_back( tn1 );
   TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 );
-  Node f = NodeManager::currentNM()->mkSkolem( "inj_$$", typ, "injection for monotonicity constraint" );
+  Node f = NodeManager::currentNM()->mkSkolem( "inj", typ, "injection for monotonicity constraint" );
   Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl;
   Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 );
   Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 );