diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-16 18:06:27 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-16 18:06:27 +0200 |
| commit | 7a36dd1e29c6d0160f949d5f805044768fb549d1 (patch) | |
| tree | bb2fea5fac3879868895c2c1dfaf0f969d94dd1d /src/theory/quantifiers/quant_util.cpp | |
| parent | 9b32405be875e7d20289d8eabbe85d036a31f301 (diff) | |
Avoid completion for large finite types. Fix bug for --fmf-fun.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index c10f1db53..2c65b62b3 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -313,12 +313,11 @@ 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 ) { - Assert( n.getKind()!=IMPLIES && n.getKind()!=XOR ); newHasPol = hasPol; newPol = pol; - if( n.getKind()==NOT ){ + if( n.getKind()==NOT || ( n.getKind()==IMPLIES && child==0 ) ){ newPol = !pol; - }else if( n.getKind()==IFF ){ + }else if( n.getKind()==IFF || n.getKind()==XOR ){ newHasPol = false; }else if( n.getKind()==ITE ){ if( child==0 ){ |