From f26477575d4328104ee6882c5d7d55740964543d Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 17 Apr 2014 13:03:30 -0400 Subject: [PATCH] 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/expr/node_manager.cpp | 20 +++-------- src/expr/node_manager.h | 13 ++++--- src/theory/arith/arith_ite_utils.cpp | 2 +- src/theory/arith/theory_arith_private.cpp | 8 ++--- src/theory/arrays/theory_arrays.cpp | 18 +++++----- .../builtin/theory_builtin_type_rules.h | 2 +- src/theory/bv/theory_bv_utils.h | 2 +- src/theory/datatypes/theory_datatypes.cpp | 2 +- src/theory/ite_utilities.cpp | 4 +-- src/theory/quantifiers/bounded_integers.cpp | 2 +- src/theory/quantifiers/first_order_model.cpp | 4 +-- src/theory/quantifiers/full_model_check.cpp | 4 +-- src/theory/quantifiers/macros.cpp | 4 +-- .../quantifiers/quantifiers_rewriter.cpp | 4 +-- src/theory/quantifiers/term_database.cpp | 4 +-- src/theory/rep_set.cpp | 2 +- src/theory/strings/regexp_operation.cpp | 8 ++--- src/theory/strings/theory_strings.cpp | 36 +++++++++---------- .../strings/theory_strings_preprocess.cpp | 34 +++++++++--------- src/theory/unconstrained_simplifier.cpp | 2 +- src/util/ite_removal.cpp | 2 +- src/util/sort_inference.cpp | 6 ++-- 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::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::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::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::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; amkSkolem( 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().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& 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 ); -- 2.30.2