diff options
author | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
---|---|---|
committer | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
commit | 3395c5c13cd61d98aec0d9806e3b9bc3d707968a (patch) | |
tree | 0eadad9799862ec77d29f7abe03a46c300d80de8 /src/theory/quantifiers/quant_util.cpp | |
parent | 773e7d27d606b71ff0f78e84efe1deef2653f016 (diff) | |
parent | 5f415d4585134612bc24e9a823289fee35541a01 (diff) |
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts:
src/options/quantifiers_options
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rwxr-xr-x | src/theory/quantifiers/quant_util.cpp | 104 |
1 files changed, 104 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b9aab0236..f4284a8ab 100755 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -419,3 +419,107 @@ 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( tn.isBoolean() ? IFF : 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; + } +} + |