# Whether to mini-scope quantifiers.
# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
# ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
-option miniscopeQuant /--disable-miniscope-quant bool :default true
+option miniscopeQuant --miniscope-quant bool :default true :read-write
disable miniscope quantifiers
# Whether to mini-scope quantifiers based on formulas with no free variables.
# For example, forall x. ( P( x ) V Q ) will be rewritten to
# ( forall x. P( x ) ) V Q
-option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true
+option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
disable miniscope quantifiers for ground subformulas
# Whether to prenex (nested universal) quantifiers
# Whether to variable-eliminate quantifiers.
# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
# forall y. P( c, y )
-option varElimQuant /--disable-var-elim-quant bool :default true
+option varElimQuant --var-elim-quant bool :default true
disable simple variable elimination for quantified formulas
option dtVarExpandQuant --dt-var-exp-quant bool :default true
expand datatype variables bound to one constructor in quantifiers
option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
split variables occurring as conditions of ITE in quantifiers
-option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
+option simpleIteLiftQuant --ite-lift-quant bool :default true
disable simple ite lifting for quantified formulas
# Whether to CNF quantifier bodies
option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h"
which ground terms to consider for instantiation
# Whether to use smart triggers
-option smartTriggers /--disable-smart-triggers bool :default true
+option smartTriggers --smart-triggers bool :default true
disable smart triggers
# Whether to use relevent triggers
option relevantTriggers --relevant-triggers bool :default false
option flipDecision --flip-decision/ bool :default false
turns on flip decision heuristic
-option internalReps /--disable-quant-internal-reps bool :default true
+option internalReps --quant-internal-reps bool :default true
disables instantiating with representatives chosen by quantifiers engine
option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
option fmfInstEngine --fmf-inst-engine bool :default false
use instantiation engine in conjunction with finite model finding
-option fmfInstGen /--disable-fmf-inst-gen bool :default true
+option fmfInstGen --fmf-inst-gen bool :default true
disable Inst-Gen instantiation techniques for finite model finding
option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
only perform Inst-Gen instantiation techniques on one quantifier per round
option fmfFreshDistConst --fmf-fresh-dc bool :default false
use fresh distinguished representative when applying Inst-Gen techniques
-option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
+option fmfFmcSimple --fmf-fmc-simple bool :default true
disable simple models in full model check for finite model finding
option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
finite model finding on bounded integer quantification
}
}
-void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){
- std::vector< Node > processed;
- setNestedQuantifiers2( n, q, processed );
-}
-
-void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ) {
- if( std::find( processed.begin(), processed.end(), n )==processed.end() ){
- processed.push_back( n );
- if( n.getKind()==FORALL || n.getKind()==EXISTS ){
- Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl;
- NestedQuantAttribute nqai;
- n[0].setAttribute(nqai,q);
- }
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- setNestedQuantifiers2( n[i], q, processed );
- }
- }
-}
-
RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
- Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in[0].hasAttribute(NestedQuantAttribute()) << std::endl;
- if( !in.hasAttribute(NestedQuantAttribute()) ){
- setNestedQuantifiers( in[ 1 ], in );
- }
+ Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << std::endl;
std::vector< Node > args;
for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
args.push_back( in[0][i] );
}
Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
if( in!=n ){
- setAttributes( in, n );
Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
Trace("quantifiers-pre-rewrite") << " to " << std::endl;
Trace("quantifiers-pre-rewrite") << n << std::endl;
RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
- Trace("quantifiers-rewrite-debug") << "Attributes : " << in[0].hasAttribute(NestedQuantAttribute()) << std::endl;
+ Trace("quantifiers-rewrite-debug") << "Attributes : " << std::endl;
if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){
RewriteStatus status = REWRITE_DONE;
Node ret = in;
ret = ret.negate();
status = REWRITE_AGAIN_FULL;
}else{
- bool isNested = in[0].hasAttribute(NestedQuantAttribute());
for( int op=0; op<COMPUTE_LAST; op++ ){
+ //TODO : compute isNested (necessary?)
+ bool isNested = false;
if( doOperation( in, isNested, op ) ){
ret = computeOperation( in, isNested, op );
if( ret!=in ){
}
//print if changed
if( in!=ret ){
- setAttributes( in, ret );
Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
Trace("quantifiers-rewrite") << " to " << std::endl;
Trace("quantifiers-rewrite") << ret << std::endl;
- //Trace("quantifiers-rewrite-debug") << "Attributes : " << ret[0].hasAttribute(NestedQuantAttribute()) << std::endl;
}
return RewriteResponse( status, ret );
}
}
}
-void QuantifiersRewriter::setAttributes( Node in, Node n ) {
- if( n.getKind()==FORALL && in.getKind()==FORALL ){
- if( in[0].hasAttribute(NestedQuantAttribute()) ){
- setNestedQuantifiers( n[0], in[0].getAttribute(NestedQuantAttribute()) );
- }
- }
-}
-
Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){
if( isLiteral( n ) ){
return n;
}
}
-Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested ){
+Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ){
//Notice() << "rewrite quant " << body << std::endl;
if( body.getKind()==FORALL ){
//combine arguments
}
newArgs.insert( newArgs.end(), args.begin(), args.end() );
return mkForAll( newArgs, body[ 1 ], ipl );
- }else if( !isNested ){
+ }else{
if( body.getKind()==NOT ){
//push not downwards
if( body[0].getKind()==NOT ){
//}
}
-Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested ){
- if( !isNested ){
- std::map< Node, std::vector< Node > > varLits;
- std::map< Node, std::vector< Node > > litVars;
- if( body.getKind()==OR ){
- Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
- for( size_t i=0; i<body.getNumChildren(); i++ ){
- std::vector< Node > activeArgs;
- computeArgVec( args, activeArgs, body[i] );
- for (unsigned j=0; j<activeArgs.size(); j++ ){
- varLits[activeArgs[j]].push_back( body[i] );
- }
- litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() );
+Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){
+ std::map< Node, std::vector< Node > > varLits;
+ std::map< Node, std::vector< Node > > litVars;
+ if( body.getKind()==OR ){
+ Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
+ for( size_t i=0; i<body.getNumChildren(); i++ ){
+ std::vector< Node > activeArgs;
+ computeArgVec( args, activeArgs, body[i] );
+ for (unsigned j=0; j<activeArgs.size(); j++ ){
+ varLits[activeArgs[j]].push_back( body[i] );
}
- //find the variable in the least number of literals
- Node bestVar;
- for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
- if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
- bestVar = it->first;
- }
+ litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() );
+ }
+ //find the variable in the least number of literals
+ Node bestVar;
+ for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
+ if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
+ bestVar = it->first;
}
- Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl;
- if( !bestVar.isNull() && varLits[bestVar].size()<body.getNumChildren() ){
- //we can miniscope
- Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
- //make the bodies
- std::vector< Node > qlit1;
- qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
- std::vector< Node > qlitt;
- //for all literals not containing bestVar
- for( size_t i=0; i<body.getNumChildren(); i++ ){
- if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
- qlitt.push_back( body[i] );
- }
+ }
+ Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl;
+ if( !bestVar.isNull() && varLits[bestVar].size()<body.getNumChildren() ){
+ //we can miniscope
+ Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
+ //make the bodies
+ std::vector< Node > qlit1;
+ qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
+ std::vector< Node > qlitt;
+ //for all literals not containing bestVar
+ for( size_t i=0; i<body.getNumChildren(); i++ ){
+ if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
+ qlitt.push_back( body[i] );
}
- //make the variable lists
- std::vector< Node > qvl1;
- std::vector< Node > qvl2;
- std::vector< Node > qvsh;
- for( unsigned i=0; i<args.size(); i++ ){
- bool found1 = false;
- bool found2 = false;
- for( size_t j=0; j<varLits[args[i]].size(); j++ ){
- if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
- found1 = true;
- }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
- found2 = true;
- }
- if( found1 && found2 ){
- break;
- }
+ }
+ //make the variable lists
+ std::vector< Node > qvl1;
+ std::vector< Node > qvl2;
+ std::vector< Node > qvsh;
+ for( unsigned i=0; i<args.size(); i++ ){
+ bool found1 = false;
+ bool found2 = false;
+ for( size_t j=0; j<varLits[args[i]].size(); j++ ){
+ if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
+ found1 = true;
+ }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
+ found2 = true;
}
- if( found1 ){
- if( found2 ){
- qvsh.push_back( args[i] );
- }else{
- qvl1.push_back( args[i] );
- }
- }else{
- Assert(found2);
- qvl2.push_back( args[i] );
+ if( found1 && found2 ){
+ break;
}
}
- Assert( !qvl1.empty() );
- Assert( !qvl2.empty() || !qvsh.empty() );
- //check for literals that only contain shared variables
- std::vector< Node > qlitsh;
- std::vector< Node > qlit2;
- for( size_t i=0; i<qlitt.size(); i++ ){
- bool hasVar2 = false;
- for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
- if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
- hasVar2 = true;
- break;
- }
- }
- if( hasVar2 ){
- qlit2.push_back( qlitt[i] );
+ if( found1 ){
+ if( found2 ){
+ qvsh.push_back( args[i] );
}else{
- qlitsh.push_back( qlitt[i] );
+ qvl1.push_back( args[i] );
}
+ }else{
+ Assert(found2);
+ qvl2.push_back( args[i] );
}
- varLits.clear();
- litVars.clear();
- Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
- Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
- Node n1 = qlit1.size()==1 ? qlit1[0] : NodeManager::currentNM()->mkNode( OR, qlit1 );
- n1 = computeAggressiveMiniscoping( qvl1, n1 );
- qlitsh.push_back( n1 );
- if( !qlit2.empty() ){
- Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 );
- n2 = computeAggressiveMiniscoping( qvl2, n2 );
- qlitsh.push_back( n2 );
+ }
+ Assert( !qvl1.empty() );
+ Assert( !qvl2.empty() || !qvsh.empty() );
+ //check for literals that only contain shared variables
+ std::vector< Node > qlitsh;
+ std::vector< Node > qlit2;
+ for( size_t i=0; i<qlitt.size(); i++ ){
+ bool hasVar2 = false;
+ for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
+ if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
+ hasVar2 = true;
+ break;
+ }
}
- Node n = NodeManager::currentNM()->mkNode( OR, qlitsh );
- if( !qvsh.empty() ){
- Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh);
- n = NodeManager::currentNM()->mkNode( FORALL, bvl, n );
+ if( hasVar2 ){
+ qlit2.push_back( qlitt[i] );
+ }else{
+ qlitsh.push_back( qlitt[i] );
}
- Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
- return n;
}
+ varLits.clear();
+ litVars.clear();
+ Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
+ Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
+ Node n1 = qlit1.size()==1 ? qlit1[0] : NodeManager::currentNM()->mkNode( OR, qlit1 );
+ n1 = computeAggressiveMiniscoping( qvl1, n1 );
+ qlitsh.push_back( n1 );
+ if( !qlit2.empty() ){
+ Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 );
+ n2 = computeAggressiveMiniscoping( qvl2, n2 );
+ qlitsh.push_back( n2 );
+ }
+ Node n = NodeManager::currentNM()->mkNode( OR, qlitsh );
+ if( !qvsh.empty() ){
+ Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh);
+ n = NodeManager::currentNM()->mkNode( FORALL, bvl, n );
+ }
+ Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
+ return n;
}
}
return mkForAll( args, body, Node::null() );
n = computeElimSymbols( n );
}else if( computeOption==COMPUTE_MINISCOPING ){
//return directly
- return computeMiniscoping( f, args, n, ipl, isNested );
+ return computeMiniscoping( f, args, n, ipl );
}else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
- return computeAggressiveMiniscoping( args, n, isNested );
+ return computeAggressiveMiniscoping( args, n );
}else if( computeOption==COMPUTE_NNF ){
n = computeNNF( n );
}else if( computeOption==COMPUTE_PROCESS_ITE ){
projects / cvc5.git / commitdiff