diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-08-11 23:00:08 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-08-11 23:00:08 -0700 |
| commit | 1b2d0bc63191f9c39b852836b38d90c4bec91b0d (patch) | |
| tree | 716018d0590c1b7eb2c600c0714d01aea6be4683 /src/theory/arith/nonlinear_extension.cpp | |
| parent | 4b5460a79838e93f8d417462c930806a77c09d31 (diff) | |
Fix compiler warnings in theory/arith/nonlinear_extension.cpp
Diffstat (limited to 'src/theory/arith/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 3c3301db1..0a70ac807 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -1079,12 +1079,10 @@ std::vector<Node> NonlinearExtension::checkSplitZero() { for (unsigned i = 0; i < d_ms_vars.size(); i++) { Node v = d_ms_vars[i]; if (d_zero_split.insert(v)) { - Node lem = v.eqNode(d_zero); - lem = Rewriter::rewrite(lem); - d_containing.getValuation().ensureLiteral(lem); - d_containing.getOutputChannel().requirePhase(lem, true); - lem = NodeManager::currentNM()->mkNode(kind::OR, lem, lem.negate()); - lemmas.push_back(lem); + Node eq = v.eqNode(d_zero); + Node literal = d_containing.getValuation().ensureLiteral(eq); + d_containing.getOutputChannel().requirePhase(literal, true); + lemmas.push_back(literal.orNode(literal.negate())); } } return lemmas; @@ -1406,12 +1404,10 @@ void NonlinearExtension::check(Theory::Effort e) { if( stv0!=stv1 ){ Trace("nl-ext-mv") << "Bad shared term value : " << shared_term << " : " << stv1 << ", actual is " << stv0 << std::endl; //split on the value, FIXME : this is non-terminating in general, improve this - Node lem = shared_term.eqNode(stv0); - lem = Rewriter::rewrite(lem); - d_containing.getValuation().ensureLiteral(lem); - d_containing.getOutputChannel().requirePhase(lem, true); - lem = NodeManager::currentNM()->mkNode(kind::OR, lem, lem.negate()); - lemmas.push_back(lem); + Node eq = shared_term.eqNode(stv0); + Node literal = d_containing.getValuation().ensureLiteral(eq); + d_containing.getOutputChannel().requirePhase(literal, true); + lemmas.push_back(literal.orNode(literal.negate())); } } if( !lemmas.empty() ){ |