From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 24 Aug 2012 23:23:34 +0000 (+0000)
Subject: * disallow internal uses of mkVar() (you have to mkSkolem())
X-Git-Tag: cvc5-1.0.0~7846
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80afd586eb0865efcc38aa14833d682f1b7cc27f;p=cvc5.git

* disallow internal uses of mkVar() (you have to mkSkolem())
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)
---

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index afac925e2..62885f55f 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -330,7 +330,7 @@ bool Expr::isString() const {
 }
 
 bool Expr::isBoundVar() const {
-  Unimplemented();
+  return getKind() == CVC4::kind::BOUND_VARIABLE;
 }
 
 bool Expr::isLambda() const {
@@ -1857,7 +1857,7 @@ Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Exp
 
 Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& uid,
                                    const Type& type) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  return d_em->mkBoundVar(name, type);
 }
 
 Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body) {
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index a8491c937..5e7aebbec 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -44,16 +44,16 @@ ${includes}
     } \
     ++ *(d_exprStatistics[kind]); \
   }
-  #define INC_STAT_VAR(type) \
+  #define INC_STAT_VAR(type, bound_var) \
   { \
     TypeNode* typeNode = Type::getTypeNode(type); \
     TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst<TypeConstant>() : LAST_TYPE; \
     if (d_exprStatisticsVars[type] == NULL) { \
       stringstream statName; \
       if (type == LAST_TYPE) { \
-        statName << "expr::ExprManager::VARIABLE:Parameterized type"; \
+        statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":Parameterized type"; \
       } else { \
-        statName << "expr::ExprManager::VARIABLE:" << type; \
+        statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \
       } \
       d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
       d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
@@ -62,7 +62,7 @@ ${includes}
   }
 #else
   #define INC_STAT(kind)
-  #define INC_STAT_VAR(type)
+  #define INC_STAT_VAR(type, bound_var)
 #endif
 
 using namespace std;
@@ -791,19 +791,35 @@ Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
 }
 
 Expr ExprManager::mkVar(const std::string& name, Type type) {
+  Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
   NodeManagerScope nms(d_nodeManager);
   Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
-  INC_STAT_VAR(type);
+  INC_STAT_VAR(type, false);
   return Expr(this, n);
 }
 
 Expr ExprManager::mkVar(Type type) {
+  Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
   NodeManagerScope nms(d_nodeManager);
-  INC_STAT_VAR(type);
+  INC_STAT_VAR(type, false);
   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
 }
 
+Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
+  NodeManagerScope nms(d_nodeManager);
+  Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode);
+  Debug("nm") << "set " << name << " on " << *n << std::endl;
+  INC_STAT_VAR(type, true);
+  return Expr(this, n);
+}
+
+Expr ExprManager::mkBoundVar(Type type) {
+  NodeManagerScope nms(d_nodeManager);
+  INC_STAT_VAR(type, true);
+  return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
+}
+
 Expr ExprManager::mkAssociative(Kind kind,
                                 const std::vector<Expr>& children) {
   CheckArgument( kind::isAssociative(kind), kind,
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index b762da3ea..158f17c14 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -450,6 +450,8 @@ public:
   // variables are special, because duplicates are permitted
   Expr mkVar(const std::string& name, Type type);
   Expr mkVar(Type type);
+  Expr mkBoundVar(const std::string& name, Type type);
+  Expr mkBoundVar(Type type);
 
   /** Get a reference to the statistics registry for this ExprManager */
   StatisticsRegistry* getStatisticsRegistry() const throw();
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 18b60738f..27d77a646 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -69,6 +69,10 @@ class NodeManager {
   friend class expr::NodeValue;
   friend class expr::TypeChecker;
 
+  // friends so they can access mkVar() here, which is private
+  friend Expr ExprManager::mkVar(const std::string& name, Type type);
+  friend Expr ExprManager::mkVar(Type type);
+
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {
     bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
@@ -257,6 +261,20 @@ class NodeManager {
 
   void init();
 
+  /**
+   * Create a variable with the given name and type.  NOTE that no
+   * lookup is done on the name.  If you mkVar("a", type) and then
+   * mkVar("a", type) again, you have two variables.  The NodeManager
+   * version of this is private to avoid internal uses of mkVar() from
+   * within CVC4.  Such uses should employ mkSkolem() instead.
+   */
+  Node mkVar(const std::string& name, const TypeNode& type);
+  Node* mkVarPtr(const std::string& name, const TypeNode& type);
+
+  /** Create a variable with the given type. */
+  Node mkVar(const TypeNode& type);
+  Node* mkVarPtr(const TypeNode& type);
+
 public:
 
   explicit NodeManager(context::Context* ctxt, ExprManager* exprManager);
@@ -347,20 +365,15 @@ public:
   template <bool ref_count>
   Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
 
-  /**
-   * Create a variable with the given name and type.  NOTE that no
-   * lookup is done on the name.  If you mkVar("a", type) and then
-   * mkVar("a", type) again, you have two variables.
-   */
-  Node mkVar(const std::string& name, const TypeNode& type);
-  Node* mkVarPtr(const std::string& name, const TypeNode& type);
+  Node mkBoundVar(const std::string& name, const TypeNode& type);
+  Node* mkBoundVarPtr(const std::string& name, const TypeNode& type);
 
-  /** Create a variable with the given type. */
-  Node mkVar(const TypeNode& type);
-  Node* mkVarPtr(const TypeNode& type);
+  Node mkBoundVar(const TypeNode& type);
+  Node* mkBoundVarPtr(const TypeNode& type);
 
   /** Create a skolem constant with the given type. */
   Node mkSkolem(const TypeNode& type);
+  Node mkSkolem(const std::string& name, const TypeNode& type);
 
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
@@ -1356,7 +1369,6 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
 
 inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
   Node n = mkVar(type);
-  setAttribute(n, TypeAttr(), type);
   setAttribute(n, expr::VarNameAttr(), name);
   return n;
 }
@@ -1364,7 +1376,19 @@ inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
 inline Node* NodeManager::mkVarPtr(const std::string& name,
                                    const TypeNode& type) {
   Node* n = mkVarPtr(type);
-  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, expr::VarNameAttr(), name);
+  return n;
+}
+
+inline Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) {
+  Node n = mkBoundVar(type);
+  setAttribute(n, expr::VarNameAttr(), name);
+  return n;
+}
+
+inline Node* NodeManager::mkBoundVarPtr(const std::string& name,
+                                        const TypeNode& type) {
+  Node* n = mkBoundVarPtr(type);
   setAttribute(*n, expr::VarNameAttr(), name);
   return n;
 }
@@ -1383,6 +1407,26 @@ inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
   return n;
 }
 
+inline Node NodeManager::mkBoundVar(const TypeNode& type) {
+  Node n = NodeBuilder<0>(this, kind::BOUND_VARIABLE);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
+  return n;
+}
+
+inline Node* NodeManager::mkBoundVarPtr(const TypeNode& type) {
+  Node* n = NodeBuilder<0>(this, kind::BOUND_VARIABLE).constructNodePtr();
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, TypeCheckedAttr(), true);
+  return n;
+}
+
+inline Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type) {
+  Node n = mkSkolem(type);
+  setAttribute(n, expr::VarNameAttr(), name);
+  return n;
+}
+
 inline Node NodeManager::mkSkolem(const TypeNode& type) {
   Node n = NodeBuilder<0>(this, kind::SKOLEM);
   setAttribute(n, TypeAttr(), type);
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 05fed15ea..3c4a51ad4 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1254,14 +1254,14 @@ prefixFormula[CVC4::Expr& f]
     { PARSER_STATE->pushScope(); } LPAREN
     boundVarDecl[ids,t]
     { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
-        bvs.push_back(PARSER_STATE->mkVar(*i, t));
+        bvs.push_back(PARSER_STATE->mkBoundVar(*i, t));
       }
       ids.clear();
     }
     ( COMMA boundVarDecl[ids,t]
       {
         for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
-          bvs.push_back(PARSER_STATE->mkVar(*i, t));
+          bvs.push_back(PARSER_STATE->mkBoundVar(*i, t));
         }
         ids.clear();
       }
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 29db640c7..bf7c372b7 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -149,6 +149,14 @@ Parser::mkVar(const std::string& name, const Type& type,
   return expr;
 }
 
+Expr
+Parser::mkBoundVar(const std::string& name, const Type& type) {
+  Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
+  Expr expr = d_exprManager->mkBoundVar(name, type);
+  defineVar(name, expr, false);
+  return expr;
+}
+
 Expr
 Parser::mkFunction(const std::string& name, const Type& type,
                             bool levelZero) {
@@ -178,7 +186,8 @@ Parser::mkVars(const std::vector<std::string> names,
 
 void
 Parser::defineVar(const std::string& name, const Expr& val,
-                       bool levelZero) {
+                  bool levelZero) {
+  Debug("parser") << "defineVar( " << name << " := " << val << " , " << levelZero << ")" << std::endl;;
   d_symtab->bind(name, val, levelZero);
   Assert( isDeclared(name) );
 }
@@ -300,14 +309,14 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
       Expr::printtypes::Scope pts(Debug("parser-idt"), true);
       Expr constructor = ctor.getConstructor();
       Debug("parser-idt") << "+ define " << constructor << std::endl;
-      string constructorName = constructor.toString();
+      string constructorName = ctor.getName();
       if(isDeclared(constructorName, SYM_VARIABLE)) {
         throw ParserException(constructorName + " already declared");
       }
       defineVar(constructorName, constructor);
       Expr tester = ctor.getTester();
       Debug("parser-idt") << "+ define " << tester << std::endl;
-      string testerName = tester.toString();
+      string testerName = ctor.getTesterName();
       if(isDeclared(testerName, SYM_VARIABLE)) {
         throw ParserException(testerName + " already declared");
       }
@@ -318,7 +327,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
           ++k) {
         Expr selector = (*k).getSelector();
         Debug("parser-idt") << "+++ define " << selector << std::endl;
-        string selectorName = selector.toString();
+        string selectorName = (*k).getName();
         if(isDeclared(selectorName, SYM_VARIABLE)) {
           throw ParserException(selectorName + " already declared");
         }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index f3210ae29..7efc4d78c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -347,6 +347,9 @@ public:
     mkVars(const std::vector<std::string> names, const Type& type,
            bool levelZero = false);
 
+  /** Create a new CVC4 bound variable expression of the given type. */
+  Expr mkBoundVar(const std::string& name, const Type& type);
+
   /** Create a new CVC4 function expression of the given type. */
   Expr mkFunction(const std::string& name, const Type& type,
                   bool levelZero = false);
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index f9c38385f..0298497e9 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -253,7 +253,7 @@ annotatedFormula[CVC4::Expr& expr]
     ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } )
     { PARSER_STATE->pushScope(); }
     ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK
-      { args.push_back(PARSER_STATE->mkVar(name, t)); }
+      { args.push_back(PARSER_STATE->mkBoundVar(name, t)); }
     )+
     annotatedFormula[expr] RPAREN_TOK
     { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) );
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 456e3c656..d8157acbc 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -407,7 +407,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
           ++i) {
-        args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+        args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
       }
       bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
     }
@@ -448,7 +448,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
           ++i) {
-        args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+        args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
       }
       bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
     }
@@ -597,7 +597,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
           ++i) {
-        args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+        args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
       }
       Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
       args.clear();
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 63774a087..068e92cd7 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -327,7 +327,7 @@ variable[CVC4::Expr & expr]
       if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)){
         expr = PARSER_STATE->getVariable(name);
       } else {
-        expr = PARSER_STATE->mkVar(name, PARSER_STATE->d_unsorted);
+        expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
         if(PARSER_STATE->cnf) PARSER_STATE->addFreeVar(expr);
       }
     }
@@ -402,7 +402,7 @@ bindvariable[CVC4::Expr & expr]
   : UPPER_WORD
     {
       std::string name = AntlrInput::tokenText($UPPER_WORD);
-      expr = PARSER_STATE->mkVar(name, PARSER_STATE->d_unsorted);
+      expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
     }
     ;
 
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index f22b35152..cb56c3430 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -135,7 +135,7 @@ void DagificationVisitor::done(TNode node) {
     // construct the let binder
     std::stringstream ss;
     ss << d_letVarPrefix << d_letVar++;
-    Node letvar = NodeManager::currentNM()->mkVar(ss.str(), (*i).getType());
+    Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType());
 
     // apply previous substitutions to the rhs, enabling cascading LETs
     Node n = d_substitutions->apply(*i);
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;
 }
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 86a43c878..bdefe6755 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -392,6 +392,12 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
                 "cannot resolve a Datatype constructor twice; "
                 "perhaps the same constructor was added twice, "
                 "or to two datatypes?");
+
+  // we're using some internals, so we have to set up this library context
+  ExprManagerScope ems(*em);
+
+  NodeManager* nm = NodeManager::fromExprManager(em);
+  TypeNode selfTypeNode = TypeNode::fromType(self);
   size_t index = 0;
   for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
     if((*i).d_selector.isNull()) {
@@ -399,7 +405,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
       string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
       (*i).d_name.resize((*i).d_name.find('\0'));
       if(typeName == "") {
-        (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, self));
+        (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode)).toExpr();
       } else {
         map<string, DatatypeType>::const_iterator j = resolutions.find(typeName);
         if(j == resolutions.end()) {
@@ -409,7 +415,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
               << "of constructor \"" << d_name << "\"";
           throw DatatypeResolutionException(msg.str());
         } else {
-          (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, (*j).second));
+          (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second))).toExpr();
         }
       }
     } else {
@@ -422,7 +428,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
       if(!paramTypes.empty() ) {
         range = doParametricSubstitution( range, paramTypes, paramReplacements );
       }
-      (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, range));
+      (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range))).toExpr();
     }
     Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
     (*i).d_resolved = true;
@@ -435,9 +441,8 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
   // fails above, we want Constuctor::isResolved() to remain "false".
   // Further, mkConstructorType() iterates over the selectors, so
   // should get the results of any resolutions we did above.
-  d_tester = em->mkVar(d_name.substr(d_name.find('\0') + 1), em->mkTesterType(self));
-  d_name.resize(d_name.find('\0'));
-  d_constructor = em->mkVar(d_name, em->mkConstructorType(*this, self));
+  d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode)).toExpr();
+  d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode)).toExpr();
   // associate constructor with all selectors
   for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
     (*i).d_constructor = d_constructor;
@@ -503,7 +508,11 @@ void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // create the proper selector type)
   CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
   CheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
-  Expr type = selectorType.getExprManager()->mkVar(selectorType);
+
+  // we're using some internals, so we have to set up this library context
+  ExprManagerScope ems(selectorType);
+
+  Expr type = NodeManager::currentNM()->mkSkolem(TypeNode::fromType(selectorType)).toExpr();
   Debug("datatypes") << type << endl;
   d_args.push_back(DatatypeConstructorArg(selectorName, type));
 }
@@ -529,11 +538,11 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
 }
 
 std::string DatatypeConstructor::getName() const throw() {
-  string name = d_name;
-  if(!isResolved()) {
-    name.resize(name.find('\0'));
-  }
-  return name;
+  return d_name.substr(0, d_name.find('\0'));
+}
+
+std::string DatatypeConstructor::getTesterName() const throw() {
+  return d_name.substr(d_name.find('\0') + 1);
 }
 
 Expr DatatypeConstructor::getConstructor() const {
diff --git a/src/util/datatype.h b/src/util/datatype.h
index c7631ae7b..60d2c7acd 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -232,6 +232,11 @@ public:
    */
   Expr getTester() const;
 
+  /**
+   * Get the tester name for this Datatype constructor.
+   */
+  std::string getTesterName() const throw();
+
   /**
    * Get the number of arguments (so far) of this Datatype constructor.
    */
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 9a4fc8dc2..50713e2b4 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -55,7 +55,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
     TypeNode nodeType = node.getType();
     if(!nodeType.isBoolean()) {
       // Make the skolem to represent the ITE
-      Node skolem = nodeManager->mkVar(nodeType);
+      Node skolem = nodeManager->mkSkolem(nodeType);
 
       Dump.declareVar(skolem.toExpr(), "a variable introduced due to term-level ITE removal");