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")
* 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());
}
* 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());
}
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
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())
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]);
}
# 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})
{
// Exists is eliminated by the rewriter.
Assert(false);
+#ifdef NDEBUG
+ CVC4_FALLTHROUGH;
+#endif
}
default:
{
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)
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);
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;
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));
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));
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,
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
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,
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
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.
*/
{
if (lits[j] == rhsElim)
{
- rhsElim == Node::null();
+ rhsElim = Node::null();
continue;
}
auto it = lhsElim.find(lits[j]);
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)
{
{
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);
long lower,
long upper)
{
+#ifndef NDEBUG
for (long c : coefficients)
{
Assert(std::numeric_limits<std::int32_t>::min() <= c
<< "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));
}
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
{
projects / cvc5.git / commitdiff