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 {
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);
}
// 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;
// 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;
}
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;
// 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)) {
}
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)) {