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/theory/quantifiers/quantifiers_rewriter.cpp | 6 +++--- src/theory/quantifiers/term_database.cpp | 4 ++-- src/theory/quantifiers/theory_quantifiers_type_rules.h | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) (limited to 'src/theory/quantifiers') 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"); } } } -- cgit v1.2.3