From 80afd586eb0865efcc38aa14833d682f1b7cc27f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 24 Aug 2012 23:23:34 +0000 Subject: * disallow internal uses of mkVar() (you have to mkSkolem()) * add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars) --- src/compat/cvc3_compat.cpp | 4 +- src/expr/expr_manager_template.cpp | 28 +++++++-- src/expr/expr_manager_template.h | 2 + src/expr/node_manager.h | 68 ++++++++++++++++++---- src/parser/cvc/Cvc.g | 4 +- src/parser/parser.cpp | 17 ++++-- src/parser/parser.h | 3 + src/parser/smt/Smt.g | 2 +- src/parser/smt2/Smt2.g | 6 +- src/parser/tptp/Tptp.g | 4 +- src/printer/dagification_visitor.cpp | 2 +- src/theory/arith/dio_solver.cpp | 2 +- src/theory/arith/theory_arith_instantiator.cpp | 2 +- src/theory/arrays/theory_arrays.cpp | 2 +- src/theory/arrays/theory_arrays_model.cpp | 2 +- src/theory/builtin/kinds | 3 +- src/theory/builtin/theory_builtin_type_rules.h | 2 +- src/theory/bv/theory_bv_utils.h | 2 +- src/theory/ite_simplifier.cpp | 2 +- src/theory/model.cpp | 4 +- src/theory/quantifiers/quantifiers_rewriter.cpp | 6 +- src/theory/quantifiers/term_database.cpp | 4 +- .../quantifiers/theory_quantifiers_type_rules.h | 4 +- src/theory/uf/theory_uf_strong_solver.cpp | 2 +- src/theory/unconstrained_simplifier.cpp | 2 +- src/util/datatype.cpp | 33 +++++++---- src/util/datatype.h | 5 ++ src/util/ite_removal.cpp | 2 +- 28 files changed, 154 insertions(+), 65 deletions(-) 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& 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() : 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& 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 Node* mkNodePtr(TNode opNode, const std::vector >& 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::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::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 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& 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& 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 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::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; igetTermDatabase()->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& 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::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& 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"); -- cgit v1.2.3