diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-30 14:06:27 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-30 14:06:34 -0500 |
commit | 2abcda1cfcb0c6388c00d65f8a6b3e63de9d96df (patch) | |
tree | 6c72c3145cef49e76b1f8e5577947d441e14f938 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | f7c6707fa38a850d6798c747b3c45ef10769fa7c (diff) |
Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index b0340d630..9e0e40911 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -324,7 +324,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else if( isLiteral( body[0] ) ){ return body; }else{ - std::vector< Node > children; + std::vector< Node > children; Kind k = body[0].getKind(); if( body[0].getKind()==OR || body[0].getKind()==AND ){ @@ -1546,7 +1546,7 @@ bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& q }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ return options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_NNF ){ - return options::nnfQuant(); + return true; }else if( computeOption==COMPUTE_PROCESS_TERMS ){ return true; //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); |