diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-08-24 23:23:34 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-08-24 23:23:34 +0000 |
| commit | 80afd586eb0865efcc38aa14833d682f1b7cc27f (patch) | |
| tree | aac37b28e0330bf3b72083e979ae94ee71918771 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
| parent | 3619c784bd5dd4b91ab0a2ad429ea145636d3424 (diff) | |
* disallow internal uses of mkVar() (you have to mkSkolem())
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
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() ); |