diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-11 11:59:58 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-11 11:59:58 -0600 |
commit | 2309ba28f0fc364013b73554d4a08eaf53d85676 (patch) | |
tree | 93b50a49b0e530fcbe62d77262dc955c72026552 /src | |
parent | 31930926314011d25ee0836bc690d37f9d3d360f (diff) |
Fix term simplification based on entailment in quantifiers rewriter (#3746)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 74d8ac3a6..e35595287 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -416,23 +416,38 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ } } } + else if (n.isConst()) + { + return n.getConst<bool>() ? 1 : -1; + } return 0; } bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) { + if (n.isConst()) + { + Trace("quantifiers-rewrite-term-debug") + << "constant cond : " << n << " -> " << pol << std::endl; + if (n.getConst<bool>() != pol) + { + conflict = true; + } + return false; + } std::map< Node, bool >::iterator it = currCond.find( n ); if( it==currCond.end() ){ Trace("quantifiers-rewrite-term-debug") << "cond : " << n << " -> " << pol << std::endl; new_cond.push_back( n ); currCond[n] = pol; return true; - }else{ - if( it->second!=pol ){ - Trace("quantifiers-rewrite-term-debug") << "CONFLICTING cond : " << n << " -> " << pol << std::endl; - conflict = true; - } - return false; } + else if (it->second != pol) + { + Trace("quantifiers-rewrite-term-debug") + << "CONFLICTING cond : " << n << " -> " << pol << std::endl; + conflict = true; + } + return false; } void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) { |