Merge pull request #25 from kbansal/sets

Sets

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 d5c2b0e9d..098a7819a 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 126b30b81..0f3e53827 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 e6ee8f53b..3168d21a0 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;
       }
     }