summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node_manager.cpp20
-rw-r--r--src/expr/node_manager.h13
-rw-r--r--src/theory/arith/arith_ite_utils.cpp2
-rw-r--r--src/theory/arith/theory_arith_private.cpp8
-rw-r--r--src/theory/arrays/theory_arrays.cpp18
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h2
-rw-r--r--src/theory/bv/theory_bv_utils.h2
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp2
-rw-r--r--src/theory/ite_utilities.cpp4
-rw-r--r--src/theory/quantifiers/bounded_integers.cpp2
-rw-r--r--src/theory/quantifiers/first_order_model.cpp4
-rw-r--r--src/theory/quantifiers/full_model_check.cpp4
-rw-r--r--src/theory/quantifiers/macros.cpp4
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp4
-rw-r--r--src/theory/quantifiers/term_database.cpp4
-rw-r--r--src/theory/rep_set.cpp2
-rw-r--r--src/theory/strings/regexp_operation.cpp8
-rw-r--r--src/theory/strings/theory_strings.cpp36
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp34
-rw-r--r--src/theory/unconstrained_simplifier.cpp2
-rw-r--r--src/util/ite_removal.cpp2
-rw-r--r--src/util/sort_inference.cpp6
22 files changed, 86 insertions, 97 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 22c47da59..ecd3df084 100644
--- 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 15c49efd8..f533d3ab9 100644
--- 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 4f182fb69..d5dcae726 100644
--- 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 a63de446c..0c8ca7507 100644
--- 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 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)) {
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index c7143bdeb..0ebcb31e8 100644
--- 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 f35fc2896..95136598c 100644
--- 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 0c6842222..8396e563e 100644
--- 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 a4af4f26f..35330f81a 100644
--- 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 bec8ea350..a294eec5a 100644
--- 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 f3203da4b..d815e0ee8 100644
--- 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 6c889781d..3b6c8e492 100644
--- 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 435bf7221..72d42cf4b 100644
--- 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 a079dbaab..6af42e159 100644
--- 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 ea1231e7a..cf183dd18 100644
--- 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 169688243..2e8eb51b1 100644
--- 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 d719b4e1a..8c07b679d 100644
--- 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 ) {
}
}
if(ret == 0) {
- Node sk = NodeManager::currentNM()->mkSkolem( "rsp_$$", NodeManager::currentNM()->stringType(), "Split RegExp" );
+ Node sk = NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" );
retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk);
if(!rest.isNull()) {
retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest));
@@ -1038,7 +1038,7 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
emptyflag = true;
break;
} else {
- Node sk = NodeManager::currentNM()->mkSkolem( "rc_$$", s.getType(), "created for regular expression concat" );
+ Node sk = NodeManager::currentNM()->mkSkolem( "rc", s.getType(), "created for regular expression concat" );
Node lem = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk, r[i]);
nvec.push_back(lem);
cc.push_back(sk);
@@ -1098,8 +1098,8 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
} else {
Node se = s.eqNode(d_emptyString);
Node sinr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[0]);
- Node sk1 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );
- Node sk2 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" );
+ Node sk2 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" );
Node s1nz = sk1.eqNode(d_emptyString).negate();
Node s2nz = sk2.eqNode(d_emptyString).negate();
Node s1inr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk1, r[0]);
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f2172071d..ac5a97167 100644
--- 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 1b040f71c..85ab73691 100644
--- 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 115788639..7509c7f4f 100644
--- 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 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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback