diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-21 10:07:12 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-21 10:07:19 +0200 |
commit | fb746fdd4e60e7d166b0fa1e5788bea925d22ee7 (patch) | |
tree | 1a8b8dc8c2b4f57352ab10365e2b2765c06285c9 /src/theory/quantifiers/quant_util.cpp | |
parent | 60f6d09d7ad9e37f5a23e6a2b0e47a7b0e47df81 (diff) |
Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Enable redundant ITE branch elimination in quantifiers rewriter.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 2c65b62b3..938245871 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -313,15 +313,20 @@ 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 || ( n.getKind()==IMPLIES && child==0 ) ){ + if( n.getKind()==AND || n.getKind()==OR ){ + newHasPol = hasPol; + newPol = pol; + }else if( n.getKind()==IMPLIES ){ + newHasPol = hasPol; + newPol = child==0 ? !pol : pol; + }else if( n.getKind()==NOT ){ + newHasPol = hasPol; newPol = !pol; - }else if( n.getKind()==IFF || n.getKind()==XOR ){ - newHasPol = false; }else if( n.getKind()==ITE ){ - if( child==0 ){ - newHasPol = false; - } + newHasPol = (child!=0) && hasPol; + newPol = pol; + }else{ + newHasPol = false; + newPol = pol; } } |