diff options
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/bv_gauss.cpp | 8 | ||||
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 4 | ||||
| -rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 4 | ||||
| -rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 6 | ||||
| -rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 4 |
5 files changed, 13 insertions, 13 deletions
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index 6b8b7af2f..ebdc9aba2 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -263,7 +263,7 @@ BVGauss::Result BVGauss::gaussElim(Integer prime, size_t nrows = lhs.size(); size_t ncols = lhs[0].size(); - #ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for (size_t i = 1; i < nrows; ++i) Assert(lhs[i].size() == ncols); #endif /* (1) if element in pivot column is non-zero and != 1, divide row elements @@ -284,7 +284,7 @@ BVGauss::Result BVGauss::gaussElim(Integer prime, /* lhs[j][pcol]: element in pivot column */ for (size_t j = prow; j < nrows; ++j) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for (size_t k = 0; k < pcol; ++k) { Assert(lhs[j][k] == 0); @@ -577,7 +577,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( return BVGauss::Result::INVALID; } size_t nrows = vars.begin()->second.size(); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for (const auto& p : vars) { Assert(p.second.size() == nrows); @@ -597,7 +597,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( } } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for (const auto& row : lhs) { Assert(row.size() == nvars); diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 28dcc1949..9809adf63 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -155,7 +155,7 @@ Node BVToInt::eliminationPass(Node n) current = toVisit.back(); // assert that the node is binarized // The following variable is only used in assertions - CVC4_UNUSED kind::Kind_t k = current.getKind(); + CVC5_UNUSED kind::Kind_t k = current.getKind(); uint64_t numChildren = current.getNumChildren(); Assert((numChildren == 2) || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT @@ -342,7 +342,7 @@ Node BVToInt::translateWithChildren(Node original, Assert(oldKind != kind::BITVECTOR_ULTBV); Assert(oldKind != kind::BITVECTOR_SLTBV); // The following variable will only be used in assertions. - CVC4_UNUSED uint64_t originalNumChildren = original.getNumChildren(); + CVC5_UNUSED uint64_t originalNumChildren = original.getNumChildren(); Node returnNode; switch (oldKind) { diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 9ca58c334..687cb3a96 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -537,8 +537,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node n = Rewriter::rewrite(geq.andNode(leq)); assertionsToPreprocess->push_back(n); TrustSubstitutionMap tnullMap(&fakeContext, nullptr); - CVC4_UNUSED SubstitutionMap& nullMap = tnullMap.get(); - Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions + CVC5_UNUSED SubstitutionMap& nullMap = tnullMap.get(); + Theory::PPAssertStatus status CVC5_UNUSED; // just for assertions status = te->solve(tgeq, tnullMap); Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED) << "unexpected solution from arith's ppAssert()"; diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index e5b0cd39b..8992dad5e 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -131,7 +131,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // No conflict, go through the literals and solve them context::Context* u = d_preprocContext->getUserContext(); TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions(); - CVC4_UNUSED SubstitutionMap& top_level_substs = ttls.get(); + CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get(); // constant propagations std::shared_ptr<TrustSubstitutionMap> constantPropagations = std::make_shared<TrustSubstitutionMap>( @@ -261,7 +261,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS // NOTE: When debugging this code, consider moving this check inside of the // loop over propagator->getLearnedLiterals(). This check has been moved // outside because it is costly for certain inputs (see bug 508). @@ -288,7 +288,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( Assert(Rewriter::rewrite((*pos).first) == (*pos).first); Assert(cps.apply((*pos).second) == (*pos).second); } -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ // Resize the learnt Trace("non-clausal-simplify") diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 2c01bd6d2..69ca1fa84 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -280,7 +280,7 @@ void UnconstrainedSimplifier::processUnconstrained() checkParent = true; break; } - CVC4_FALLTHROUGH; + CVC5_FALLTHROUGH; case kind::BITVECTOR_COMP: case kind::LT: case kind::LEQ: @@ -454,7 +454,7 @@ void UnconstrainedSimplifier::processUnconstrained() { break; } - CVC4_FALLTHROUGH; + CVC5_FALLTHROUGH; case kind::XOR: case kind::BITVECTOR_XOR: case kind::BITVECTOR_XNOR: |