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.

2 files changed, 4 insertions, 4 deletions

diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 1b29f9ef8..f1dce413c 100644
--- 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 682e1e1e7..ce12b59f1 100644
--- 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 );