From 1b2d0bc63191f9c39b852836b38d90c4bec91b0d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 11 Aug 2017 23:00:08 -0700 Subject: [PATCH] Fix compiler warnings in theory/arith/nonlinear_extension.cpp --- src/theory/arith/nonlinear_extension.cpp | 20 ++++++++------------ 1 file 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 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() ){ -- 2.30.2