diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-17 13:03:30 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-17 13:40:15 -0400 |
commit | f26477575d4328104ee6882c5d7d55740964543d (patch) | |
tree | 8dc248031d8cc213762f0fa30ff13a7b8f851984 /src/theory/quantifiers | |
parent | 4b02944c70522de78713f9870d2eccbf348bfcf6 (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 4 |
6 files changed, 11 insertions, 11 deletions
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; } } |