summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CMakeLists.txt3
-rw-r--r--src/api/cvc4cpp.cpp4
-rw-r--r--src/api/python/CMakeLists.txt6
-rw-r--r--src/expr/node_trie.cpp4
-rw-r--r--src/parser/CMakeLists.txt2
-rw-r--r--src/preprocessing/passes/bv_to_int.cpp3
-rw-r--r--src/theory/arith/nl/poly_conversion.cpp4
-rw-r--r--src/theory/arrays/theory_arrays.cpp5
-rw-r--r--src/theory/booleans/circuit_propagator.cpp35
-rw-r--r--src/theory/booleans/circuit_propagator.h29
-rw-r--r--src/theory/booleans/proof_checker.cpp2
-rw-r--r--src/theory/quantifiers/ematching/inst_match_generator_simple.cpp2
-rw-r--r--src/theory/quantifiers/skolemize.cpp2
-rw-r--r--src/util/real_algebraic_number_poly_imp.cpp2
-rw-r--r--test/unit/theory/logic_info_white.cpp4
15 files changed, 54 insertions, 53 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 3dd282a8d..c32c10f4d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -234,8 +234,9 @@ include(Config${CMAKE_BUILD_TYPE})
add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
add_check_c_cxx_flag("-Wall")
+add_check_c_cxx_flag("-Werror")
+add_check_c_cxx_flag("-Wno-unused-private-field")
add_check_c_flag("-fexceptions")
-add_check_c_cxx_flag("-Wno-deprecated")
add_check_cxx_flag("-Wsuggest-override")
add_check_cxx_flag("-Wnon-virtual-dtor")
add_check_c_cxx_flag("-Wimplicit-fallthrough")
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 10f39cb38..0c94320c3 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -748,7 +748,7 @@ class CVC4ApiExceptionStream
* default to noexcept(true) (else this triggers a call to std::terminate). */
~CVC4ApiExceptionStream() noexcept(false)
{
- if (!std::uncaught_exception())
+ if (std::uncaught_exceptions() == 0)
{
throw CVC4ApiException(d_stream.str());
}
@@ -769,7 +769,7 @@ class CVC4ApiRecoverableExceptionStream
* default to noexcept(true) (else this triggers a call to std::terminate). */
~CVC4ApiRecoverableExceptionStream() noexcept(false)
{
- if (!std::uncaught_exception())
+ if (std::uncaught_exceptions() == 0)
{
throw CVC4ApiRecoverableException(d_stream.str());
}
diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index dde29110f..211fb5ff8 100644
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -48,6 +48,12 @@ add_library(pycvc4
target_link_libraries(pycvc4 cvc4 ${PYTHON_LIBRARIES})
+# Disable -Werror and other warnings for code generated by Cython.
+set_target_properties(pycvc4
+ PROPERTIES
+ COMPILE_FLAGS
+ "-Wno-error -Wno-shadow -Wno-implicit-fallthrough")
+
python_extension_module(pycvc4)
# Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html
diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp
index 58ad36da9..d2da99509 100644
--- a/src/expr/node_trie.cpp
+++ b/src/expr/node_trie.cpp
@@ -24,7 +24,7 @@ NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::existsTerm(
const NodeTemplateTrie<ref_count>* tnt = this;
typename std::map<NodeTemplate<ref_count>,
NodeTemplateTrie<ref_count>>::const_iterator it;
- for (const NodeTemplate<ref_count> r : reps)
+ for (const NodeTemplate<ref_count>& r : reps)
{
it = tnt->d_data.find(r);
if (it == tnt->d_data.end())
@@ -51,7 +51,7 @@ NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::addOrGetTerm(
NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
{
NodeTemplateTrie<ref_count>* tnt = this;
- for (const NodeTemplate<ref_count> r : reps)
+ for (const NodeTemplate<ref_count>& r : reps)
{
tnt = &(tnt->d_data[r]);
}
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 8e69da34b..2fe92fb45 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -93,7 +93,7 @@ foreach(lang Cvc Smt2 Tptp)
# We don't want to enable -Wall for code generated by ANTLR.
set_source_files_properties(
- ${gen_src_files} PROPERTIES COMPILE_FLAGS -Wno-all)
+ ${gen_src_files} PROPERTIES COMPILE_FLAGS "-Wno-all -Wno-error")
# Add generated source files to the parser source files
list(APPEND libcvc4parser_src_files ${gen_src_files})
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index f5d840a49..4712db91f 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -691,6 +691,9 @@ Node BVToInt::translateWithChildren(Node original,
{
// Exists is eliminated by the rewriter.
Assert(false);
+#ifdef NDEBUG
+ CVC4_FALLTHROUGH;
+#endif
}
default:
{
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);
diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp
index 674850534..e0a56f610 100644
--- a/src/util/real_algebraic_number_poly_imp.cpp
+++ b/src/util/real_algebraic_number_poly_imp.cpp
@@ -60,6 +60,7 @@ RealAlgebraicNumber::RealAlgebraicNumber(const std::vector<long>& coefficients,
long lower,
long upper)
{
+#ifndef NDEBUG
for (long c : coefficients)
{
Assert(std::numeric_limits<std::int32_t>::min() <= c
@@ -67,6 +68,7 @@ RealAlgebraicNumber::RealAlgebraicNumber(const std::vector<long>& coefficients,
<< "Coefficients need to fit within 32 bit integers. Please use the "
"constructor based on Integer instead.";
}
+#endif
d_value = poly::AlgebraicNumber(poly::UPolynomial(coefficients),
poly::DyadicInterval(lower, upper));
}
diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp
index 7ffbd6d2a..5dc8c45cb 100644
--- a/test/unit/theory/logic_info_white.cpp
+++ b/test/unit/theory/logic_info_white.cpp
@@ -27,8 +27,8 @@ namespace test {
class TestTheoryWhiteLogicInfo : public TestInternal
{
-#warning \
- "This test is of questionable compatiblity with contrib/new-theory. Is the new theory id handled correctly by the Logic info."
+ // This test is of questionable compatiblity with contrib/new-theory. Is the
+ // new theory id handled correctly by the Logic info.
protected:
void eq(const LogicInfo& logic1, const LogicInfo& logic2) const
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback