* disallow internal uses of mkVar() (you have to mkSkolem())

* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)

3 files changed, 7 insertions, 7 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 800fa910c..e928010b6 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -384,7 +384,7 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui
       TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->booleanType() );
       std::stringstream ss;
       ss << "cnf_" << n.getKind() << "_" << n.getId();
-      Node op = NodeManager::currentNM()->mkVar( ss.str(), typ );
+      Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ );
       std::vector< Node > predArgs;
       predArgs.push_back( op );
       predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() );
@@ -473,7 +473,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
         for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
           //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
           terms.push_back( body[0][i] );
-          subs.push_back( NodeManager::currentNM()->mkVar( body[0][i].getType() ) );
+          subs.push_back( NodeManager::currentNM()->mkSkolem( body[0][i].getType() ) );
         }
         args.insert( args.end(), subs.begin(), subs.end() );
       }else{
@@ -486,7 +486,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
           terms.push_back( body[0][i] );
           //make the new function symbol
           TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, body[0][i].getType() );
-          Node op = NodeManager::currentNM()->mkVar( typ );
+          Node op = NodeManager::currentNM()->mkSkolem( typ );
           std::vector< Node > funcArgs;
           funcArgs.push_back( op );
           funcArgs.insert( funcArgs.end(), args.begin(), args.end() );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e1cd7e42c..cc74e3e76 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -198,7 +198,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
       std::stringstream ss;
       ss << Expr::setlanguage(options::outputLanguage());
       ss << "e_" << tn;
-      mbt = NodeManager::currentNM()->mkVar( ss.str(), tn );
+      mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn );
     }else{
       mbt = d_type_map[ tn ][ 0 ];
     }
@@ -342,7 +342,7 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){
       d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
     }else{
       if( d_type_map[ tn ].empty() ){
-        d_free_vars[tn] = NodeManager::currentNM()->mkVar( tn );
+        d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( tn );
       }else{
         d_free_vars[tn] = d_type_map[ tn ][ 0 ];
       }
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index ceec36d7b..50d5a8142 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -73,8 +73,8 @@ struct QuantifierBoundVarListTypeRule {
     Assert(n.getKind() == kind::BOUND_VAR_LIST );
     if( check ){
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        if( n[i].getKind()!=kind::VARIABLE ){
-          throw TypeCheckingExceptionPrivate(n, "argument of bound var list is not variable");
+        if( n[i].getKind()!=kind::BOUND_VARIABLE ){
+          throw TypeCheckingExceptionPrivate(n, "argument of bound var list is not bound variable");
         }
       }
     }