diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-02-24 16:26:44 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-24 16:26:44 -0800 |
commit | e36aeda0e759c5328ba76412dde8afbecf34970b (patch) | |
tree | 47f6795c587710c78cc558abbb3576f397c7e3b7 /src/theory | |
parent | c3e16e447aed037806f874a54ae74d6850415fd7 (diff) |
Enable -Werror. (#5969)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/nl/poly_conversion.cpp | 4 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 5 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 35 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 29 | ||||
-rw-r--r-- | src/theory/booleans/proof_checker.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator_simple.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 2 |
7 files changed, 34 insertions, 45 deletions
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 0e4e21b76..5b7edb3ef 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -452,9 +452,11 @@ Node lower_bound_as_node(const Node& var, poly::get_upper(poly::get_isolating_interval(alg))); int sl = poly::sign_at(get_defining_polynomial(alg), poly::get_lower(poly::get_isolating_interval(alg))); +#ifndef NDEBUG int su = poly::sign_at(get_defining_polynomial(alg), poly::get_upper(poly::get_isolating_interval(alg))); Assert(sl != 0 && su != 0 && sl != su); +#endif // open: var <= l or (var < u and sgn(poly(var)) == sl) // !open: var <= l or (var < u and sgn(poly(var)) == sl/0) @@ -506,8 +508,10 @@ Node upper_bound_as_node(const Node& var, poly::get_lower(poly::get_isolating_interval(alg))); Rational u = poly_utils::toRational( poly::get_upper(poly::get_isolating_interval(alg))); +#ifndef NDEBUG int sl = poly::sign_at(get_defining_polynomial(alg), poly::get_lower(poly::get_isolating_interval(alg))); +#endif int su = poly::sign_at(get_defining_polynomial(alg), poly::get_upper(poly::get_isolating_interval(alg))); Assert(sl != 0 && su != 0 && sl != su); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f07140d4e..4dd7dcafd 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -936,7 +936,10 @@ void TheoryArrays::checkPair(TNode r1, TNode r2) case EQUALITY_FALSE_AND_PROPAGATED: // Should have been propagated to us Assert(false); - case EQUALITY_FALSE: +#ifdef NDEBUG + CVC4_FALLTHROUGH; +#endif + case EQUALITY_FALSE: CVC4_FALLTHROUGH; case EQUALITY_FALSE_IN_MODEL: // This is unlikely, but I think it could happen Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair called when false in model" << std::endl; diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 24e821e33..726160d83 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -252,8 +252,10 @@ void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) else { // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) - TNode::iterator holdout = find_if_unique( - parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + TNode::iterator holdout = + find_if_unique(parent.begin(), parent.end(), [this](TNode x) { + return !isAssignedTo(x, true); + }); if (holdout != parent.end()) { assignAndEnqueue(*holdout, false, prover.andFalse(parent, holdout)); @@ -264,8 +266,10 @@ void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) if (parentAssignment) { // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) - TNode::iterator holdout = find_if_unique( - parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + TNode::iterator holdout = + find_if_unique(parent.begin(), parent.end(), [this](TNode x) { + return !isAssignedTo(x, false); + }); if (holdout != parent.end()) { assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout)); @@ -450,8 +454,10 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) if (childAssignment) { TNode::iterator holdout; - holdout = find_if( - parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + holdout = find_if(parent.begin(), parent.end(), [this](TNode x) { + return !isAssignedTo(x, true); + }); + if (holdout == parent.end()) { // all children are assigned TRUE // AND ...(x=TRUE)...: if all children now assigned to TRUE, @@ -461,8 +467,10 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) else if (isAssignedTo(parent, false)) { // the AND is FALSE // is the holdout unique ? - TNode::iterator other = find_if( - holdout + 1, parent.end(), not1(IsAssignedTo(*this, true))); + TNode::iterator other = + find_if(holdout + 1, parent.end(), [this](TNode x) { + return !isAssignedTo(x, true); + }); if (other == parent.end()) { // the holdout is unique // AND ...(x=TRUE)...: if all children BUT ONE now assigned to @@ -487,8 +495,9 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) else { TNode::iterator holdout; - holdout = find_if( - parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + holdout = find_if(parent.begin(), parent.end(), [this](TNode x) { + return !isAssignedTo(x, false); + }); if (holdout == parent.end()) { // all children are assigned FALSE // OR ...(x=FALSE)...: if all children now assigned to FALSE, @@ -498,8 +507,10 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) else if (isAssignedTo(parent, true)) { // the OR is TRUE // is the holdout unique ? - TNode::iterator other = find_if( - holdout + 1, parent.end(), not1(IsAssignedTo(*this, false))); + TNode::iterator other = + find_if(holdout + 1, parent.end(), [this](TNode x) { + return !isAssignedTo(x, false); + }); if (other == parent.end()) { // the holdout is unique // OR ...(x=FALSE)...: if all children BUT ONE now assigned to diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 3546a4d35..469a01815 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -169,35 +169,6 @@ class CircuitPropagator T& d_data; }; /* class DataClearer<T> */ - /** Predicate for use in STL functions. */ - class IsAssigned : public std::unary_function<TNode, bool> - { - CircuitPropagator& d_circuit; - - public: - IsAssigned(CircuitPropagator& circuit) : d_circuit(circuit) {} - - bool operator()(TNode in) const { return d_circuit.isAssigned(in); } - }; /* class IsAssigned */ - - /** Predicate for use in STL functions. */ - class IsAssignedTo : public std::unary_function<TNode, bool> - { - CircuitPropagator& d_circuit; - bool d_value; - - public: - IsAssignedTo(CircuitPropagator& circuit, bool value) - : d_circuit(circuit), d_value(value) - { - } - - bool operator()(TNode in) const - { - return d_circuit.isAssignedTo(in, d_value); - } - }; /* class IsAssignedTo */ - /** * Assignment status of each node. */ diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 83662a50f..405dae250 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -272,7 +272,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, { if (lits[j] == rhsElim) { - rhsElim == Node::null(); + rhsElim = Node::null(); continue; } auto it = lhsElim.find(lits[j]); diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 39dd8ed22..6b2f1b7f8 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -131,7 +131,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, TNode t = tat->getData(); Debug("simple-trigger") << "Actual term is " << t << std::endl; // convert to actual used terms - for (const std::pair<unsigned, int>& v : d_var_num) + for (const auto& v : d_var_num) { if (v.second >= 0) { diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 2e9093b82..a9ac7d0d2 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -383,7 +383,7 @@ void Skolemize::getSkolemTermVectors( { std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::const_iterator itk; - for (const std::pair<const Node, Node>& p : d_skolemized) + for (const auto& p : d_skolemized) { Node q = p.first; itk = d_skolem_constants.find(q); |