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.

1 files changed, 9 insertions, 9 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index cd9fd2497..8aad67883 100644
--- 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)) {