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 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp') 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() ); -- cgit v1.2.3