From f26477575d4328104ee6882c5d7d55740964543d Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 17 Apr 2014 13:03:30 -0400 Subject: 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. --- src/theory/arrays/theory_arrays.cpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'src/theory/arrays/theory_arrays.cpp') 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::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)) { -- cgit v1.2.3