diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 23:20:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 23:20:09 -0500 |
commit | 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 (patch) | |
tree | b5c785e9a5e16d430f45b2a40f78e40247111233 /src/theory/quantifiers/quant_util.cpp | |
parent | 4b580ea3876055f701b13e67e0e4e78abbe47674 (diff) |
(Move-only) Split quant util (#1306)
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 238 |
1 files changed, 4 insertions, 234 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 88fdec6f3..b8e29280d 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -19,11 +19,11 @@ #include "theory/quantifiers_engine.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; +namespace CVC4 { +namespace theory { unsigned QuantifiersModule::needsModel( Theory::Effort e ) { return QuantifiersEngine::QEFFORT_NONE; @@ -291,62 +291,6 @@ void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char Trace(c) << std::endl; } - -void QuantRelevance::registerQuantifier( Node f ){ - //compute symbols in f - std::vector< Node > syms; - computeSymbols( f[1], syms ); - d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() ); - //set initial relevance - int minRelevance = -1; - for( int i=0; i<(int)syms.size(); i++ ){ - d_syms_quants[ syms[i] ].push_back( f ); - int r = getRelevance( syms[i] ); - if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){ - minRelevance = r; - } - } - if( minRelevance!=-1 ){ - setRelevance( f, minRelevance+1 ); - } -} - - -/** compute symbols */ -void QuantRelevance::computeSymbols( Node n, std::vector< Node >& syms ){ - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( std::find( syms.begin(), syms.end(), op )==syms.end() ){ - syms.push_back( op ); - } - } - if( n.getKind()!=FORALL ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - computeSymbols( n[i], syms ); - } - } -} - -/** set relevance */ -void QuantRelevance::setRelevance( Node s, int r ){ - if( d_computeRel ){ - int rOld = getRelevance( s ); - if( rOld==-1 || r<rOld ){ - d_relevance[s] = r; - if( s.getKind()==FORALL ){ - for( int i=0; i<(int)d_syms[s].size(); i++ ){ - setRelevance( d_syms[s][i], r ); - } - }else{ - for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){ - setRelevance( d_syms_quants[s][i], r+1 ); - } - } - } - } -} - - QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ initialize( n, computeEq ); } @@ -456,179 +400,5 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, } } -void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ) { - int vindex = hasPol ? ( pol ? 1 : -1 ) : 0; - if( visited[vindex].find( n )==visited[vindex].end() ){ - visited[vindex][n] = true; - Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl; - if( n.getKind()==FORALL ){ - if( beneathQuant || !hasPol || !pol ){ - for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ - TypeNode tn = n[0][i].getType(); - if( d_non_epr.find( tn )==d_non_epr.end() ){ - Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested or possible existential quantification." << std::endl; - d_non_epr[tn] = true; - } - } - }else{ - beneathQuant = true; - } - } - TypeNode tn = n.getType(); - - if( n.getNumChildren()>0 ){ - if( tn.isSort() ){ - if( d_non_epr.find( tn )==d_non_epr.end() ){ - Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n << std::endl; - d_non_epr[tn] = true; - } - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - bool newHasPol; - bool newPol; - QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); - registerNode( n[i], visited, beneathQuant, newHasPol, newPol ); - } - }else if( tn.isSort() ){ - if( n.getKind()==BOUND_VARIABLE ){ - if( d_consts.find( tn )==d_consts.end() ){ - //mark that at least one constant must occur - d_consts[tn].clear(); - } - }else if( std::find( d_consts[tn].begin(), d_consts[tn].end(), n )==d_consts[tn].end() ){ - d_consts[tn].push_back( n ); - Trace("quant-epr") << "...constant of type " << tn << " : " << n << std::endl; - } - } - } -} - -void QuantEPR::registerAssertion( Node assertion ) { - std::map< int, std::map< Node, bool > > visited; - registerNode( assertion, visited, false, true, true ); -} - -void QuantEPR::finishInit() { - Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl; - for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){ - Assert( d_epr_axiom.find( it->first )==d_epr_axiom.end() ); - Trace("quant-epr-debug") << "process " << it->first << std::endl; - if( d_non_epr.find( it->first )!=d_non_epr.end() ){ - Trace("quant-epr-debug") << "...non-epr" << std::endl; - it->second.clear(); - }else{ - Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() << std::endl; - if( it->second.empty() ){ - it->second.push_back( NodeManager::currentNM()->mkSkolem( "e", it->first, "EPR base constant" ) ); - } - if( Trace.isOn("quant-epr") ){ - Trace("quant-epr") << "Type " << it->first << " is EPR, with constants : " << std::endl; - for( unsigned i=0; i<it->second.size(); i++ ){ - Trace("quant-epr") << " " << it->second[i] << std::endl; - } - } - } - } -} - -bool QuantEPR::isEPRConstant( TypeNode tn, Node k ) { - return std::find( d_consts[tn].begin(), d_consts[tn].end(), k )!=d_consts[tn].end(); -} - -void QuantEPR::addEPRConstant( TypeNode tn, Node k ) { - Assert( isEPR( tn ) ); - Assert( d_epr_axiom.find( tn )==d_epr_axiom.end() ); - if( !isEPRConstant( tn, k ) ){ - d_consts[tn].push_back( k ); - } -} - -Node QuantEPR::mkEPRAxiom( TypeNode tn ) { - Assert( isEPR( tn ) ); - std::map< TypeNode, Node >::iterator ita = d_epr_axiom.find( tn ); - if( ita==d_epr_axiom.end() ){ - std::vector< Node > disj; - Node x = NodeManager::currentNM()->mkBoundVar( tn ); - for( unsigned i=0; i<d_consts[tn].size(); i++ ){ - disj.push_back( NodeManager::currentNM()->mkNode( EQUAL, x, d_consts[tn][i] ) ); - } - Assert( !disj.empty() ); - d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) ); - return d_epr_axiom[tn]; - }else{ - return ita->second; - } -} - - -void TermRecBuild::addTerm( Node n ) { - d_term.push_back( n ); - std::vector< Node > currc; - d_kind.push_back( n.getKind() ); - if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){ - currc.push_back( n.getOperator() ); - d_has_op.push_back( true ); - }else{ - d_has_op.push_back( false ); - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - currc.push_back( n[i] ); - } - d_children.push_back( currc ); -} - -void TermRecBuild::init( Node n ) { - Assert( d_term.empty() ); - addTerm( n ); -} - -void TermRecBuild::push( unsigned p ) { - Assert( !d_term.empty() ); - unsigned curr = d_term.size()-1; - Assert( d_pos.size()==curr ); - Assert( d_pos.size()+1==d_children.size() ); - Assert( p<d_term[curr].getNumChildren() ); - addTerm( d_term[curr][p] ); - d_pos.push_back( p ); -} - -void TermRecBuild::pop() { - Assert( !d_pos.empty() ); - d_pos.pop_back(); - d_kind.pop_back(); - d_has_op.pop_back(); - d_children.pop_back(); - d_term.pop_back(); -} - -void TermRecBuild::replaceChild( unsigned i, Node n ) { - Assert( !d_term.empty() ); - unsigned curr = d_term.size()-1; - unsigned o = d_has_op[curr] ? 1 : 0; - d_children[curr][i+o] = n; -} - -Node TermRecBuild::getChild( unsigned i ) { - unsigned curr = d_term.size()-1; - unsigned o = d_has_op[curr] ? 1 : 0; - return d_children[curr][i+o]; -} - -Node TermRecBuild::build( unsigned d ) { - Assert( d_pos.size()+1==d_term.size() ); - Assert( d<d_term.size() ); - int p = d<d_pos.size() ? d_pos[d] : -2; - std::vector< Node > children; - unsigned o = d_has_op[d] ? 1 : 0; - for( unsigned i=0; i<d_children[d].size(); i++ ){ - Node nc; - if( p+o==i ){ - nc = build( d+1 ); - }else{ - nc = d_children[d][i]; - } - children.push_back( nc ); - } - return NodeManager::currentNM()->mkNode( d_kind[d], children ); -} - +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ |