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

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

14 files changed, 20 insertions, 19 deletions

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index e3eae88b3..83ba49257 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -28,7 +28,7 @@ namespace arith {
 
 inline Node makeIntegerVariable(){
   NodeManager* curr = NodeManager::currentNM();
-  return curr->mkVar(curr->integerType());
+  return curr->mkSkolem(curr->integerType());
 }
 
 DioSolver::DioSolver(context::Context* ctxt) :
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
index 1682897ae..51e3a6638 100644
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -412,7 +412,7 @@ Node InstantiatorTheoryArith::getDelta( Node n ){
   if( it==d_deltas.end() ){
     std::ostringstream os;
     os << "delta_" << d_deltas.size();
-    Node delta = NodeManager::currentNM()->mkVar( os.str(), n.getType() );
+    Node delta = NodeManager::currentNM()->mkSkolem( os.str(), n.getType() );
     d_deltas[ n.getType() ] = delta;
     Node gt = NodeManager::currentNM()->mkNode( GT, delta, NodeManager::currentNM()->mkConst( Rational(0) ) );
     //add split
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 4f2497d2b..4beab2d61 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -694,7 +694,7 @@ void TheoryArrays::check(Effort e) {
             TNode k;
             std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact);
             if (it == d_diseqCache.end()) {
-              Node newk = nm->mkVar(indexType);
+              Node newk = nm->mkSkolem(indexType);
 	      Dump.declareVar(newk.toExpr(),
                               "an extensional lemma index variable from the theory of arrays");
               d_diseqCache[fact] = newk;
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
index 7a574fac1..5c969060d 100644
--- a/src/theory/arrays/theory_arrays_model.cpp
+++ b/src/theory/arrays/theory_arrays_model.cpp
@@ -29,7 +29,7 @@ using namespace CVC4::theory::arrays;
 ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){
   Assert( arr.getKind()!=STORE );
   //look at ground assertions
-  Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) );
+  Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkSkolem( arr.getType().getArrayIndexType() ) );
   Node sel_op = sel.getOperator();  //FIXME: easier way to do this?
   for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){
     Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i];
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 285eb651f..48fe4d84a 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -293,8 +293,9 @@ parameterized APPLY FUNCTION 0: "defined function application"
 
 operator EQUAL 2 "equality"
 operator DISTINCT 2: "disequality"
-variable SKOLEM "skolem var"
 variable VARIABLE "variable"
+variable BOUND_VARIABLE "bound variable"
+variable SKOLEM "skolem var"
 operator TUPLE 1: "a tuple"
 
 constant TYPE_CONSTANT \
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index ef7078624..68d9e8702 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -152,7 +152,7 @@ public:
   }
   inline static Node mkGroundTerm(TypeNode type) {
     Assert(type.getKind() == kind::SORT_TYPE);
-    return NodeManager::currentNM()->mkVar( type );
+    return NodeManager::currentNM()->mkSkolem( type );
   }
 };/* class SortProperties */
 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index a0d418c4b..8349a1479 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -68,7 +68,7 @@ inline Node mkFalse() {
 
 inline Node mkVar(unsigned size) {
   NodeManager* nm =  NodeManager::currentNM();
-  return nm->mkVar(nm->mkBitVectorType(size)); 
+  return nm->mkSkolem(nm->mkBitVectorType(size)); 
 }
 
 inline Node mkAnd(std::vector<TNode>& children) {
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
index ab8f159a9..6eb777ad5 100644
--- a/src/theory/ite_simplifier.cpp
+++ b/src/theory/ite_simplifier.cpp
@@ -148,7 +148,7 @@ Node ITESimplifier::getSimpVar(TypeNode t)
     return (*it).second;
   }
   else {
-    Node var = NodeManager::currentNM()->mkVar(t);
+    Node var = NodeManager::currentNM()->mkSkolem(t);
     d_simpVars[t] = var;
     return var;
   }
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 2260e86d3..a194336fb 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -236,7 +236,7 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){
     }while( true );
   }else{
     //otherwise must make a variable  FIXME: how to make constants for other sorts?
-    //return NodeManager::currentNM()->mkVar( tn );
+    //return NodeManager::currentNM()->mkSkolem( tn );
     return Node::null();
   }
 }
@@ -374,7 +374,7 @@ Node DefaultModel::getInterpretedValue( TNode n ){
           default_v = v;
         }
         if( default_v.isNull() ){
-          default_v = getInterpretedValue( NodeManager::currentNM()->mkVar( type.getRangeType() ) );
+          default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( type.getRangeType() ) );
         }
         ufmt.setDefaultValue( this, default_v );
         ufmt.simplify();
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");
         }
       }
     }
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 2ee8b6c93..f0b386cae 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1048,7 +1048,7 @@ Node StrongSolverTheoryUf::ConflictFind::getCardinalityLemma(){
       std::stringstream ss;
       ss << Expr::setlanguage(options::outputLanguage());
       ss << "t_" << d_type;
-      d_cardinality_lemma_term = NodeManager::currentNM()->mkVar( ss.str(), d_type );
+      d_cardinality_lemma_term = NodeManager::currentNM()->mkSkolem( ss.str(), d_type );
     }
     Node lem = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_lemma_term,
                                   NodeManager::currentNM()->mkConst( Rational( d_cardinality ) ) );
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 58254df33..c23a72c91 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -93,7 +93,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
 
 Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var)
 {
-  Node n = NodeManager::currentNM()->mkVar(t);
+  Node n = NodeManager::currentNM()->mkSkolem(t);
   Dump.declareVar(n.toExpr(), "a new var introduced because of unconstrained variable " + var.toString());
   return n;
 }