diff options
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 59995a510..31a95fb8a 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -239,3 +239,17 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } } } + +void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { + newHasPol = hasPol; + newPol = pol; + if( n.getKind()==NOT ){ + newPol = !pol; + }else if( n.getKind()==IFF ){ + newHasPol = false; + }else if( n.getKind()==ITE ){ + if( child==0 ){ + newHasPol = false; + } + } +}
\ No newline at end of file |