diff options
Diffstat (limited to 'src/theory')
59 files changed, 230 insertions, 220 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index caa052065..76737976a 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -30,7 +30,7 @@ #include "theory/arith/normal_form.h" #include "theory/eager_proof_generator.h" -#ifdef CVC4_USE_GLPK +#ifdef CVC5_USE_GLPK #include "theory/arith/partial_model.h" #endif @@ -372,7 +372,7 @@ public: } // namespace cvc5 /* Begin the declaration of GLPK specific code. */ -#ifdef CVC4_USE_GLPK +#ifdef CVC5_USE_GLPK extern "C" { #include <glpk.h> }/* extern "C" */ @@ -538,7 +538,7 @@ int ApproxGLPK::s_verbosity = 0; } // namespace arith } // namespace theory } // namespace cvc5 -#endif /*#ifdef CVC4_USE_GLPK */ +#endif /*#ifdef CVC5_USE_GLPK */ /* End the declaration of GLPK specific code. */ /* Begin GPLK/NOGLPK Glue code. */ @@ -546,14 +546,14 @@ namespace cvc5 { namespace theory { namespace arith { ApproximateSimplex* ApproximateSimplex::mkApproximateSimplexSolver(const ArithVariables& vars, TreeLog& l, ApproximateStatistics& s){ -#ifdef CVC4_USE_GLPK +#ifdef CVC5_USE_GLPK return new ApproxGLPK(vars, l, s); #else return new ApproxNoOp(vars, l, s); #endif } bool ApproximateSimplex::enabled() { -#ifdef CVC4_USE_GLPK +#ifdef CVC5_USE_GLPK return true; #else return false; @@ -565,12 +565,12 @@ bool ApproximateSimplex::enabled() { /* End GPLK/NOGLPK Glue code. */ /* Begin GPLK implementation. */ -#ifdef CVC4_USE_GLPK +#ifdef CVC5_USE_GLPK namespace cvc5 { namespace theory { namespace arith { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS static CutInfoKlass fromGlpkClass(int klass){ switch(klass){ case GLP_RF_GMI: return GmiCutKlass; @@ -1430,7 +1430,7 @@ static GmiInfo* gmiCut(glp_tree *tree, int exec_ord, int cut_ord){ int M = gmi->getMAtCreation(); // Get the tableau row - int nrows CVC4_UNUSED = glp_ios_cut_get_aux_nrows(tree, gmi->poolOrdinal()); + int nrows CVC5_UNUSED = glp_ios_cut_get_aux_nrows(tree, gmi->poolOrdinal()); Assert(nrows == 1); int rows[1+1]; glp_ios_cut_get_aux_rows(tree, gmi->poolOrdinal(), rows, NULL); @@ -3177,5 +3177,5 @@ void ApproxGLPK::tryCut(int nid, CutInfo& cut) } // namespace arith } // namespace theory } // namespace cvc5 -#endif /*#ifdef CVC4_USE_GLPK */ +#endif /*#ifdef CVC5_USE_GLPK */ /* End GPLK implementation. */ diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index ce54133c5..2b90a133a 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -259,7 +259,7 @@ void ArithStaticLearner::addBound(TNode n) { DeltaRational bound = constant; switch(Kind k = n.getKind()) { - case kind::LT: bound = DeltaRational(constant, -1); CVC4_FALLTHROUGH; + case kind::LT: bound = DeltaRational(constant, -1); CVC5_FALLTHROUGH; case kind::LEQ: if (maxFind == d_maxMap.end() || (*maxFind).second > bound) { @@ -267,7 +267,7 @@ void ArithStaticLearner::addBound(TNode n) { Debug("arith::static") << "adding bound " << n << endl; } break; - case kind::GT: bound = DeltaRational(constant, 1); CVC4_FALLTHROUGH; + case kind::GT: bound = DeltaRational(constant, 1); CVC5_FALLTHROUGH; case kind::GEQ: if (minFind == d_minMap.end() || (*minFind).second < bound) { diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 6ceab1933..5c39b7fc6 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -619,7 +619,7 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::solveIndex(DioS Debug("arith::dio") << "before solveIndex("<<i<<":"<<si.getNode()<< ")" << endl; -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS const Polynomial& p = si.getPolynomial(); #endif @@ -655,7 +655,7 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::decomposeIndex( Debug("arith::dio") << "before decomposeIndex("<<i<<":"<<si.getNode()<< ")" << endl; -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS const Polynomial& p = si.getPolynomial(); #endif diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 52dd20779..ec791856a 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -212,7 +212,7 @@ bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingI //DeltaRational beta_i = d_variables.getAssignment(x_i); ArithVar x_j = ARITHVAR_SENTINEL; - int32_t prevErrorSize CVC4_UNUSED = d_errorSet.errorSize(); + int32_t prevErrorSize CVC5_UNUSED = d_errorSet.errorSize(); if(d_variables.cmpAssignmentLowerBound(x_i) < 0 ){ x_j = d_linEq.selectSlackUpperBound(x_i, pf); @@ -248,7 +248,7 @@ bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingI Assert(x_j != ARITHVAR_SENTINEL); bool conflict = processSignals(); - int32_t currErrorSize CVC4_UNUSED = d_errorSet.errorSize(); + int32_t currErrorSize CVC5_UNUSED = d_errorSet.errorSize(); d_pivots++; if(Debug.isOn("arith::dual")){ diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index 4788d2697..acfe526a6 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -85,10 +85,10 @@ private: // // typedef FocusSet::handle_type FocusSetHandle; -// typedef CVC4_PB_DS_NAMESPACE::priority_queue< +// typedef CVC5_PB_DS_NAMESPACE::priority_queue< // ArithVar, // ComparatorPivotRule, -// CVC4_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet; +// CVC5_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet; // typedef FocusSet::point_iterator FocusSetHandle; diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index c9f3ce3da..4cd9077ca 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -17,7 +17,7 @@ #include "theory/arith/nl/cad/cdcac.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include "options/arith_options.h" #include "theory/arith/nl/cad/projections.h" diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index 0d5d4ce74..58aa41bd1 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -20,7 +20,7 @@ #ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_H #define CVC5__THEORY__ARITH__NL__CAD__CDCAC_H -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp index 999e491f6..3ceb36bd3 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.cpp +++ b/src/theory/arith/nl/cad/cdcac_utils.cpp @@ -16,7 +16,7 @@ #include "theory/arith/nl/cad/cdcac_utils.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include "theory/arith/nl/cad/projections.h" diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h index 3cfbb138c..50f2f8bc9 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.h +++ b/src/theory/arith/nl/cad/cdcac_utils.h @@ -19,7 +19,7 @@ #ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H #define CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp index 75d1cb723..b244bd358 100644 --- a/src/theory/arith/nl/cad/constraints.cpp +++ b/src/theory/arith/nl/cad/constraints.cpp @@ -16,7 +16,7 @@ #include "theory/arith/nl/cad/constraints.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <algorithm> diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index efc69d468..1ddbfc821 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/cad/constraints.h @@ -19,7 +19,7 @@ #ifndef CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H #define CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp index 1bac0c160..8aea538f1 100644 --- a/src/theory/arith/nl/cad/projections.cpp +++ b/src/theory/arith/nl/cad/projections.cpp @@ -16,7 +16,7 @@ #include "theory/arith/nl/cad/projections.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include "base/check.h" diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index c1ce91303..f3c8aa0f1 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -19,7 +19,7 @@ #ifndef CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H #define CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H -#ifdef CVC4_USE_POLY +#ifdef CVC5_USE_POLY #include <poly/polyxx.h> diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index 73e19aa28..291447647 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -14,7 +14,7 @@ #include "theory/arith/nl/cad/proof_generator.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include "theory/lazy_tree_proof_generator.h" #include "theory/arith/nl/poly_conversion.h" diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index 9365cc337..993524504 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -17,7 +17,7 @@ #ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H #define CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp index 7ebbc90dd..e7c8b214a 100644 --- a/src/theory/arith/nl/cad/variable_ordering.cpp +++ b/src/theory/arith/nl/cad/variable_ordering.cpp @@ -16,7 +16,7 @@ #include "theory/arith/nl/cad/variable_ordering.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include "util/poly_util.h" diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h index b4336d395..fb40a7b7d 100644 --- a/src/theory/arith/nl/cad/variable_ordering.h +++ b/src/theory/arith/nl/cad/variable_ordering.h @@ -19,7 +19,7 @@ #ifndef CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H #define CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index aa9bce776..202788ba1 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -31,7 +31,7 @@ CadSolver::CadSolver(InferenceManager& im, context::Context* ctx, ProofNodeManager* pnm) : -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP d_CAC(ctx, pnm), #endif d_foundSatisfiability(false), @@ -42,7 +42,7 @@ CadSolver::CadSolver(InferenceManager& im, SkolemManager* sm = nm->getSkolemManager(); d_ranVariable = sm->mkDummySkolem( "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME); -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; if (pc != nullptr) { @@ -56,7 +56,7 @@ CadSolver::~CadSolver() {} void CadSolver::initLastCall(const std::vector<Node>& assertions) { -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP if (Trace.isOn("nl-cad")) { Trace("nl-cad") << "CadSolver::initLastCall" << std::endl; @@ -83,7 +83,7 @@ void CadSolver::initLastCall(const std::vector<Node>& assertions) void CadSolver::checkFull() { -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP if (d_CAC.getConstraints().getConstraints().empty()) { Trace("nl-cad") << "No constraints. Return." << std::endl; return; @@ -115,7 +115,7 @@ void CadSolver::checkFull() void CadSolver::checkPartial() { -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP if (d_CAC.getConstraints().getConstraints().empty()) { Trace("nl-cad") << "No constraints. Return." << std::endl; return; @@ -165,7 +165,7 @@ void CadSolver::checkPartial() bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions) { -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP if (!d_foundSatisfiability) { return false; diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 2ea27fce7..1d51cf9c5 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -87,7 +87,7 @@ class CadSolver */ Node d_ranVariable; -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP /** * The object implementing the actual decision procedure. */ diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp index 31b7b085b..4a6d0748a 100644 --- a/src/theory/arith/nl/icp/candidate.cpp +++ b/src/theory/arith/nl/icp/candidate.cpp @@ -14,7 +14,7 @@ #include "theory/arith/nl/icp/candidate.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <iostream> diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h index 524342658..d65db52b5 100644 --- a/src/theory/arith/nl/icp/candidate.h +++ b/src/theory/arith/nl/icp/candidate.h @@ -17,7 +17,7 @@ #include "cvc4_private.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> #include "expr/node.h" diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index 2f6cdf220..39504c3aa 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -32,7 +32,7 @@ namespace arith { namespace nl { namespace icp { -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP namespace { /** A simple wrapper to nicely print an interval assignment. */ @@ -366,7 +366,7 @@ void ICPSolver::check() } } -#else /* CVC4_POLY_IMP */ +#else /* CVC5_POLY_IMP */ void ICPSolver::reset(const std::vector<Node>& assertions) { @@ -378,7 +378,7 @@ void ICPSolver::check() Unimplemented() << "ICPSolver requires CVC4 to be configured with LibPoly"; } -#endif /* CVC4_POLY_IMP */ +#endif /* CVC5_POLY_IMP */ } // namespace icp } // namespace nl diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index b392dc430..0efb2021f 100644 --- a/src/theory/arith/nl/icp/icp_solver.h +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -17,9 +17,9 @@ #include "cvc4_private.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> -#endif /* CVC4_POLY_IMP */ +#endif /* CVC5_POLY_IMP */ #include "expr/node.h" #include "theory/arith/bound_inference.h" @@ -37,7 +37,7 @@ class InferenceManager; namespace nl { namespace icp { -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP /** * This class implements an ICP-based solver. As it is intended to be used in @@ -137,7 +137,7 @@ class ICPSolver void check(); }; -#else /* CVC4_POLY_IMP */ +#else /* CVC5_POLY_IMP */ class ICPSolver { @@ -147,7 +147,7 @@ class ICPSolver void check(); }; -#endif /* CVC4_POLY_IMP */ +#endif /* CVC5_POLY_IMP */ } // namespace icp } // namespace nl diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index e0e93e1dd..6a914bc03 100644 --- a/src/theory/arith/nl/icp/intersection.cpp +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -14,7 +14,7 @@ #include "theory/arith/nl/icp/intersection.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <iostream> diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index a77a605d0..a82ad6b8e 100644 --- a/src/theory/arith/nl/icp/intersection.h +++ b/src/theory/arith/nl/icp/intersection.h @@ -17,7 +17,7 @@ #include "cvc4_private.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <cstddef> diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h index 7716d029f..42f2084e0 100644 --- a/src/theory/arith/nl/icp/interval.h +++ b/src/theory/arith/nl/icp/interval.h @@ -17,7 +17,7 @@ #include "cvc4_private.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> #include "expr/node.h" diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index c7b549655..f708896a6 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -16,7 +16,7 @@ #include "poly_conversion.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include "expr/node.h" #include "expr/node_manager_attributes.h" @@ -451,7 +451,7 @@ 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))); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS int su = poly::sign_at(get_defining_polynomial(alg), poly::get_upper(poly::get_isolating_interval(alg))); Assert(sl != 0 && su != 0 && sl != su); @@ -507,7 +507,7 @@ 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))); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS int sl = poly::sign_at(get_defining_polynomial(alg), poly::get_lower(poly::get_isolating_interval(alg))); #endif diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 0a9d0f313..c97923f23 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -19,7 +19,7 @@ #include "cvc4_private.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index fe3408a43..6075853c7 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -193,7 +193,7 @@ bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& void ArithVariables::releaseArithVar(ArithVar v){ VarInfo& vi = d_vars.get(v); - size_t removed CVC4_UNUSED = d_nodeToArithVarMap.erase(vi.d_node); + size_t removed CVC5_UNUSED = d_nodeToArithVarMap.erase(vi.d_node); Assert(removed == 1); vi.uninitialize(); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 7ad0bbfbb..887d78082 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -213,7 +213,7 @@ static void drop( ConstraintCPVec& v, ConstraintP con){ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec& pos, const ConstraintCPVec& neg){ - unsigned posPos CVC4_UNUSED = pos.size(); + unsigned posPos CVC5_UNUSED = pos.size(); for(unsigned i = 0, N = pos.size(); i < N; ++i){ if(pos[i] == c){ posPos = i; @@ -223,7 +223,7 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec& } Assert(posPos < pos.size()); ConstraintP negc = c->getNegation(); - unsigned negPos CVC4_UNUSED = neg.size(); + unsigned negPos CVC5_UNUSED = neg.size(); for(unsigned i = 0, N = neg.size(); i < N; ++i){ if(neg[i] == negc){ negPos = i; @@ -2373,8 +2373,8 @@ struct SizeOrd { void TheoryArithPrivate::subsumption( std::vector<ConstraintCPVec> &confs) const { - int checks CVC4_UNUSED = 0; - int subsumed CVC4_UNUSED = 0; + int checks CVC5_UNUSED = 0; + int subsumed CVC5_UNUSED = 0; for (size_t i = 0, N = confs.size(); i < N; ++i) { ConstraintCPVec &conf = confs[i]; @@ -3336,7 +3336,7 @@ void TheoryArithPrivate::preNotifyFact(TNode atom, bool pol, TNode fact) ConstraintP curr = constraintFromFactQueue(fact); if (curr != NullConstraint) { - bool res CVC4_UNUSED = assertionCases(curr); + bool res CVC5_UNUSED = assertionCases(curr); Assert(!res || anyConflict()); } } @@ -3350,7 +3350,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) d_learnedBounds.pop(); Debug("arith::learned") << curr << endl; - bool res CVC4_UNUSED = assertionCases(curr); + bool res CVC5_UNUSED = assertionCases(curr); Assert(!res || anyConflict()); if(anyConflict()){ break; } @@ -5035,7 +5035,7 @@ std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const Arith } // intentionally fall through to DISTINCT case! // entailments of negations are eager exit cases for EQUAL - CVC4_FALLTHROUGH; + CVC5_FALLTHROUGH; case DISTINCT: if(!bestPrimDiff.first.isNull()){ // primDir [dm * dp] <= primDir * dm * U < primDir * sep diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index d0a653410..29cd94c1d 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -788,8 +788,8 @@ void TheoryArrays::preRegisterTermInternal(TNode node) Assert(weakEquivGetRep(node) == node); d_infoMap.setWeakEquivPointer(node, node[0]); d_infoMap.setWeakEquivIndex(node, node[1]); -#ifdef CVC4_ASSERTIONS - checkWeakEquiv(false); +#ifdef CVC5_ASSERTIONS + checkWeakEquiv(false); #endif } @@ -867,7 +867,7 @@ void TheoryArrays::notifySharedTerm(TNode t) d_sharedArrays.insert(t); } else { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS d_sharedOther.insert(t); #endif d_sharedTerms = true; @@ -940,7 +940,7 @@ void TheoryArrays::checkPair(TNode r1, TNode r2) // Should have been propagated to us Assert(false); break; - case EQUALITY_FALSE: CVC4_FALLTHROUGH; + case EQUALITY_FALSE: CVC5_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; @@ -1238,11 +1238,11 @@ void TheoryArrays::postCheck(Effort level) d_infoMap.setWeakEquivPointer(b, a); d_infoMap.setWeakEquivIndex(b, TNode()); } -#ifdef CVC4_ASSERTIONS - checkWeakEquiv(false); +#ifdef CVC5_ASSERTIONS + checkWeakEquiv(false); #endif } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS checkWeakEquiv(true); #endif diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index ea56209ce..6ff91e5cb 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -103,7 +103,7 @@ class CircuitPropagator * @return a trust node encapsulating the proof for a conflict as a lemma that * proves false, or the null trust node otherwise */ - TrustNode propagate() CVC4_WARN_UNUSED_RESULT; + TrustNode propagate() CVC5_WARN_UNUSED_RESULT; /** * Get the back edges of this circuit. diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index fb5adb54c..4dd4419a4 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -24,7 +24,7 @@ #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" -#ifdef CVC4_USE_ABC +#ifdef CVC5_USE_ABC extern "C" { #include "base/abc/abc.h" @@ -168,7 +168,7 @@ AigBitblaster::AigBitblaster() solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(), "AigBitblaster"); break; - default: CVC4_FATAL() << "Unknown SAT solver type"; + default: CVC5_FATAL() << "Unknown SAT solver type"; } d_satSolver.reset(solver); } @@ -497,4 +497,4 @@ AigBitblaster::Statistics::~Statistics() { } // namespace bv } // namespace theory } // namespace cvc5 -#endif // CVC4_USE_ABC +#endif // CVC5_USE_ABC diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 2f4666a9b..37fac03af 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -40,7 +40,7 @@ class SatSolver; namespace theory { namespace bv { -#ifdef CVC4_USE_ABC +#ifdef CVC5_USE_ABC class AigBitblaster : public TBitblaster<Abc_Obj_t*> { @@ -106,7 +106,7 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> Statistics d_statistics; }; -#else /* CVC4_USE_ABC */ +#else /* CVC5_USE_ABC */ /** * Dummy version of the AigBitblaster class that cannot be instantiated s.t. we @@ -117,7 +117,7 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> AigBitblaster() = delete; }; -#endif /* CVC4_USE_ABC */ +#endif /* CVC5_USE_ABC */ } // namespace bv } // namespace theory diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 97df17c58..365817676 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -48,7 +48,7 @@ void EagerBitblastSolver::turnOffAig() { void EagerBitblastSolver::initialize() { Assert(!isInitialized()); if (d_useAig) { -#ifdef CVC4_USE_ABC +#ifdef CVC5_USE_ABC d_aigBitblaster.reset(new AigBitblaster()); #else Unreachable(); @@ -77,7 +77,7 @@ void EagerBitblastSolver::assertFormula(TNode formula) { d_assertionSet.insert(formula); // ensures all atoms are bit-blasted and converted to AIG if (d_useAig) { -#ifdef CVC4_USE_ABC +#ifdef CVC5_USE_ABC d_aigBitblaster->bbFormula(formula); #else Unreachable(); @@ -96,7 +96,7 @@ bool EagerBitblastSolver::checkSat() { } if (d_useAig) { -#ifdef CVC4_USE_ABC +#ifdef CVC5_USE_ABC const std::vector<Node> assertions = {d_assertionSet.key_begin(), d_assertionSet.key_end()}; Assert(!assertions.empty()); diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index c0bce9097..397a01b78 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -607,7 +607,7 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) z = nc > 1 ? zb.constructNode() : zb[0]; } m = utils::getSize(x); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS uint32_t n = utils::getSize(c); #endif my = y.isNull() ? 0 : utils::getSize(y); diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 1d124045b..5b2f586ba 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -22,7 +22,7 @@ #include "util/floatingpoint.h" #include "util/floatingpoint_literal_symfpu.h" -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" #include "symfpu/core/compare.h" @@ -39,11 +39,11 @@ #include "symfpu/utils/properties.h" #endif -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU namespace symfpu { using namespace ::cvc5::theory::fp::symfpuSymbolic; -#define CVC4_SYM_ITE_DFN(T) \ +#define CVC5_SYM_ITE_DFN(T) \ template <> \ struct ite<symbolicProposition, T> \ { \ @@ -114,12 +114,12 @@ using namespace ::cvc5::theory::fp::symfpuSymbolic; } // Can (unsurprisingly) only ITE things which contain Nodes -CVC4_SYM_ITE_DFN(traits::rm); -CVC4_SYM_ITE_DFN(traits::prop); -CVC4_SYM_ITE_DFN(traits::sbv); -CVC4_SYM_ITE_DFN(traits::ubv); +CVC5_SYM_ITE_DFN(traits::rm); +CVC5_SYM_ITE_DFN(traits::prop); +CVC5_SYM_ITE_DFN(traits::sbv); +CVC5_SYM_ITE_DFN(traits::ubv); -#undef CVC4_SYM_ITE_DFN +#undef CVC5_SYM_ITE_DFN template <> traits::ubv orderEncode<traits, traits::ubv>(const traits::ubv &b) @@ -144,7 +144,7 @@ void probabilityAnnotation<traits, traits::prop>(const traits::prop &p, }; #endif -#ifndef CVC4_USE_SYMFPU +#ifndef CVC5_USE_SYMFPU #define SYMFPU_NUMBER_OF_ROUNDING_MODES 5 #endif @@ -241,7 +241,7 @@ symbolicProposition symbolicProposition::operator^( bool symbolicRoundingMode::checkNodeType(const TNode n) { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES); #else return false; @@ -253,7 +253,7 @@ symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n) Assert(checkNodeType(*this)); } -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU symbolicRoundingMode::symbolicRoundingMode(const unsigned v) : nodeWrapper(NodeManager::currentNM()->mkConst( BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v))) @@ -754,7 +754,7 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const FpConverter::FpConverter(context::UserContext* user) : d_additionalAssertions(user) -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU , d_fpMap(user), d_rmMap(user), @@ -767,7 +767,7 @@ FpConverter::FpConverter(context::UserContext* user) FpConverter::~FpConverter() {} -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Node FpConverter::ufToNode(const fpt &format, const uf &u) const { NodeManager *nm = NodeManager::currentNM(); @@ -844,11 +844,11 @@ FpConverter::uf FpConverter::buildComponents(TNode current) // Non-convertible things should only be added to the stack at the very start, // thus... -#define CVC4_FPCONV_PASSTHROUGH Assert(workStack.empty()) +#define CVC5_FPCONV_PASSTHROUGH Assert(workStack.empty()) Node FpConverter::convert(TNode node) { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU std::vector<TNode> workStack; TNode result = node; @@ -1397,7 +1397,7 @@ Node FpConverter::convert(TNode node) } else { - CVC4_FPCONV_PASSTHROUGH; + CVC5_FPCONV_PASSTHROUGH; return result; } } @@ -1534,7 +1534,7 @@ Node FpConverter::convert(TNode node) /* Fall through... */ default: - CVC4_FPCONV_PASSTHROUGH; + CVC5_FPCONV_PASSTHROUGH; return result; break; } @@ -1652,7 +1652,7 @@ Node FpConverter::convert(TNode node) case kind::ROUNDINGMODE_BITBLAST: /* Fall through ... */ - default: CVC4_FPCONV_PASSTHROUGH; break; + default: CVC5_FPCONV_PASSTHROUGH; break; } } else if (t.isReal()) @@ -1691,12 +1691,12 @@ Node FpConverter::convert(TNode node) "expandDefinition"; break; - default: CVC4_FPCONV_PASSTHROUGH; break; + default: CVC5_FPCONV_PASSTHROUGH; break; } } else { - CVC4_FPCONV_PASSTHROUGH; + CVC5_FPCONV_PASSTHROUGH; } } @@ -1706,13 +1706,13 @@ Node FpConverter::convert(TNode node) #endif } -#undef CVC4_FPCONV_PASSTHROUGH +#undef CVC5_FPCONV_PASSTHROUGH Node FpConverter::getValue(Valuation &val, TNode var) { Assert(Theory::isLeafOf(var, THEORY_FP)); -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU TypeNode t(var.getType()); Assert(t.isRoundingMode() || t.isFloatingPoint()) diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index f3341f442..3a74627d5 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -32,11 +32,11 @@ #include "util/floatingpoint_size.h" #include "util/hash.h" -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU #include "symfpu/core/unpackedFloat.h" #endif -#ifdef CVC4_SYM_SYMBOLIC_EVAL +#ifdef CVC5_SYM_SYMBOLIC_EVAL // This allows debugging of the CVC4 symbolic back-end. // By enabling this and disabling constant folding in the rewriter, // SMT files that have operations on constants will be evaluated @@ -102,12 +102,12 @@ typedef traits::bwt bwt; class nodeWrapper : public Node { protected: -/* CVC4_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues. +/* CVC5_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues. * Enable this and disabling constant folding will mean that operations * that are input with constant args are 'folded' using the symbolic encoding * allowing them to be traced via GDB. */ -#ifdef CVC4_SYM_SYMBOLIC_EVAL +#ifdef CVC5_SYM_SYMBOLIC_EVAL nodeWrapper(const Node &n) : Node(theory::Rewriter::rewrite(n)) {} #else nodeWrapper(const Node &n) : Node(n) {} @@ -119,7 +119,7 @@ class symbolicProposition : public nodeWrapper protected: bool checkNodeType(const TNode node); -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE #endif @@ -140,7 +140,7 @@ class symbolicRoundingMode : public nodeWrapper protected: bool checkNodeType(const TNode n); -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE #endif @@ -182,7 +182,7 @@ class symbolicBitVector : public nodeWrapper bool checkNodeType(const TNode n); friend symbolicBitVector<!isSigned>; // To allow conversion between the types -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicBitVector<isSigned> >; // For ITE #endif @@ -313,7 +313,7 @@ class FpConverter context::CDList<Node> d_additionalAssertions; protected: -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU typedef symfpuSymbolic::traits traits; typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf; typedef symfpuSymbolic::traits::rm rm; diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index ba94dca13..51d2e5bd7 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -194,7 +194,7 @@ namespace rewrite { // Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder RewriteResponse compactMinMax (TNode node, bool isPreRewrite) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS Kind k = node.getKind(); Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX) || (k == kind::FLOATINGPOINT_MIN_TOTAL) @@ -885,7 +885,7 @@ namespace constantFold { bool result; switch (k) { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break; case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break; case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break; @@ -909,7 +909,7 @@ namespace constantFold { // \todo Add a proper interface for this sort of thing to FloatingPoint #1915 return RewriteResponse( REWRITE_DONE, -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent()) #else node @@ -925,7 +925,7 @@ namespace constantFold { return RewriteResponse( REWRITE_DONE, -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand()) #else node @@ -939,7 +939,7 @@ namespace constantFold { BitVector value; -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU /* \todo fix the numbering of rounding modes so this doesn't need * to call symfpu at all and remove the dependency on fp_converter.h #1915 */ RoundingMode arg0(node[0].getConst<RoundingMode>()); diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index d7060ad98..44936c440 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -711,7 +711,7 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager, } } -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU /* Need to create some symfpu objects as the size of bit-vector * that is needed for this component is dependent on the encoding * used (i.e. whether subnormals are forcibly normalised or not). @@ -751,7 +751,7 @@ TypeNode FloatingPointComponentSignificand::computeType( } } -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU /* As before we need to use some of sympfu. */ FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps); @@ -783,7 +783,7 @@ TypeNode RoundingModeBitBlast::computeType(NodeManager* nodeManager, } } - return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES); + return nodeManager->mkBitVectorType(CVC5_NUM_ROUNDING_MODES); } Cardinality CardinalityComputer::computeCardinality(TypeNode type) diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp index 61279ee11..b67f2dc8c 100644 --- a/src/theory/model_manager_distributed.cpp +++ b/src/theory/model_manager_distributed.cpp @@ -67,7 +67,7 @@ bool ModelManagerDistributed::prepareModel() // Consult each active theory to get all relevant information concerning the // model, which includes both dump their equality information and assigning // values. Notice the order of theories here is important and is the same - // as the list in CVC4_FOR_EACH_THEORY in theory_engine.cpp. + // as the list in CVC5_FOR_EACH_THEORY in theory_engine.cpp. for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index 7ada36dc2..d6bf5c8bd 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -237,7 +237,7 @@ bool CandidateRewriteFilter::notify(Node s, Trace("crf-match") << " " << vars[i] << " -> " << subs[i] << std::endl; } } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for (unsigned i = 0, size = vars.size(); i < size; i++) { // By using internal representation of terms, we ensure polymorphism is diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp index 0a544f785..a1ae0a5d7 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -136,7 +136,7 @@ Node normalizePvMult( return result; } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS namespace { bool isLinearPlus( TNode n, diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index 9a3d465d5..f2ccb0806 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -139,7 +139,7 @@ Node FunDefEvaluator::evaluate(Node n) const << cur[childIdxToEval] << "\n"; continue; } - unsigned child CVC4_UNUSED = 0; + unsigned child CVC5_UNUSED = 0; for (const Node& cn : cur) { it = visited.find(cn); diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 8fc1c4d13..c716554f9 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -131,7 +131,7 @@ bool Instantiate::addInstantiation(Node q, << std::endl; return false; } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS bool bad_inst = false; if (TermUtil::containsUninterpretedConstant(terms[i])) { diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 9dfac1d68..7f60ddbbd 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -1362,7 +1362,7 @@ Node SygusUnifIo::constructSol( // for ITE Node split_cond_enum; unsigned split_cond_res_index = 0; - CVC4_UNUSED bool set_split_cond_res_index = false; + CVC5_UNUSED bool set_split_cond_res_index = false; for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++) { diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index e4e63787e..77d7771d1 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -153,7 +153,7 @@ class TermTupleEnumeratorBase : public TermTupleEnumeratorInterface virtual size_t prepareTerms(size_t variableIx) = 0; /** Get a given term for a given variable. */ virtual Node getTerm(size_t variableIx, - size_t term_index) CVC4_WARN_UNUSED_RESULT = 0; + size_t term_index) CVC5_WARN_UNUSED_RESULT = 0; }; /** diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index c247d8f08..a00e4dad4 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -191,7 +191,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, TConvProofGenerator* tcpg) { RewriteWithProofsAttribute rpfa; -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); if (d_rewriteStack == nullptr) @@ -329,21 +329,21 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, // In the post rewrite if we've changed theories, we must do a full rewrite Assert(response.d_node != rewriteStackTop.d_node); //TODO: this is not thread-safe - should make this assertion dependent on sequential build -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS Assert(d_rewriteStack->find(response.d_node) == d_rewriteStack->end()); d_rewriteStack->insert(response.d_node); #endif Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg); rewriteStackTop.d_node = rewritten; -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS d_rewriteStack->erase(response.d_node); #endif break; } else if (response.d_status == REWRITE_DONE) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS RewriteResponse r2 = d_theoryRewriters[newTheoryId]->postRewrite(response.d_node); Assert(r2.d_node == response.d_node) @@ -504,7 +504,7 @@ RewriteResponse Rewriter::processTrustRewriteResponse( void Rewriter::clearCaches() { Rewriter* rewriter = getInstance(); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS rewriter->d_rewriteStack.reset(nullptr); #endif diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 94057aa54..ab3e70719 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -225,10 +225,10 @@ class Rewriter { /** The proof generator */ std::unique_ptr<TConvProofGenerator> d_tpg; -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack = nullptr; -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ };/* class Rewriter */ } // namespace theory diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index a1b2c487f..f98f6514e 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -174,7 +174,7 @@ bool ArithEntail::checkApprox(Node ar) { if (approxMsums.find(aa) == approxMsums.end()) { - CVC4_UNUSED bool ret = + CVC5_UNUSED bool ret = ArithMSum::getMonomialSum(aa, approxMsums[aa]); Assert(ret); } diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index f38acfac2..cfe80eea2 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -608,7 +608,7 @@ void CoreSolver::normalizeEquivalenceClass(Node eqc, TypeNode stype) Node emp = Word::mkEmptyWord(stype); if (d_state.areEqual(eqc, emp)) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for( unsigned j=0; j<d_eqc[eqc].size(); j++ ){ Node n = d_eqc[eqc][j]; for( unsigned i=0; i<n.getNumChildren(); i++ ){ diff --git a/src/theory/theory.h b/src/theory/theory.h index 8a3b4f293..b17d10d52 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -434,12 +434,15 @@ class Theory { EFFORT_LAST_CALL = 200 }; /* enum Effort */ - static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION - { return e >= EFFORT_STANDARD; } - static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION - { return e >= EFFORT_STANDARD && e < EFFORT_FULL; } - static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION - { return e == EFFORT_FULL; } + static inline bool standardEffortOrMore(Effort e) CVC5_CONST_FUNCTION + { + return e >= EFFORT_STANDARD; } + static inline bool standardEffortOnly(Effort e) CVC5_CONST_FUNCTION + { + return e >= EFFORT_STANDARD && e < EFFORT_FULL; } + static inline bool fullEffort(Effort e) CVC5_CONST_FUNCTION + { + return e == EFFORT_FULL; } /** * Get the id for this Theory. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index dd130e28a..d1cc4dfc1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -65,20 +65,20 @@ namespace theory { * Do not change this order. */ -#define CVC4_FOR_EACH_THEORY \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BUILTIN) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BOOL) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_UF) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_ARITH) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BV) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_FP) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_ARRAYS) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_DATATYPES) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_SEP) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_SETS) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BAGS) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_STRINGS) \ - CVC4_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_QUANTIFIERS) +#define CVC5_FOR_EACH_THEORY \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BUILTIN) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BOOL) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_UF) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_ARITH) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BV) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_FP) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_ARRAYS) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_DATATYPES) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_SEP) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_SETS) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_BAGS) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_STRINGS) \ + CVC5_FOR_EACH_THEORY_STATEMENT(cvc5::theory::THEORY_QUANTIFIERS) } // namespace theory @@ -128,12 +128,12 @@ void TheoryEngine::finishInit() { // NOTE: This seems to be required since // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without - // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR + // using the CVC5_FOR_EACH_THEORY_STATEMENT macro. -AJR std::vector<theory::Theory*> paraTheories; -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::isParametric \ && d_logicInfo.isTheoryEnabled(THEORY)) \ { \ @@ -141,7 +141,7 @@ void TheoryEngine::finishInit() } // Collect the parametric theories, which are given to the theory combination // manager below - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; // Initialize the theory combination architecture if (options::tcMode() == options::TcMode::CARE_GRAPH) @@ -411,10 +411,10 @@ void TheoryEngine::check(Theory::Effort effort) { // Reset the interrupt flag d_interrupted = false; -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasCheck \ && d_logicInfo.isTheoryEnabled(THEORY)) \ { \ @@ -471,7 +471,7 @@ void TheoryEngine::check(Theory::Effort effort) { d_factsAsserted = false; // Do the checking - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl; @@ -562,19 +562,21 @@ void TheoryEngine::propagate(Theory::Effort effort) d_interrupted = false; // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \ - theoryOf(THEORY)->propagate(effort); \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPropagate \ + && d_logicInfo.isTheoryEnabled(THEORY)) \ + { \ + theoryOf(THEORY)->propagate(effort); \ } // Reset the interrupt flag d_interrupted = false; // Propagate for each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } Node TheoryEngine::getNextDecisionRequest() @@ -665,19 +667,21 @@ bool TheoryEngine::presolve() { try { // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPresolve) { \ - theoryOf(THEORY)->presolve(); \ - if(d_inConflict) { \ - return true; \ - } \ - } +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPresolve) \ + { \ + theoryOf(THEORY)->presolve(); \ + if (d_inConflict) \ + { \ + return true; \ + } \ + } // Presolve for each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl; } @@ -690,14 +694,14 @@ void TheoryEngine::postsolve() { d_inSatMode = false; // Reset the interrupt flag d_interrupted = false; - bool CVC4_UNUSED wasInConflict = d_inConflict; + bool CVC5_UNUSED wasInConflict = d_inConflict; try { // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasPostsolve) \ { \ theoryOf(THEORY)->postsolve(); \ @@ -706,7 +710,7 @@ void TheoryEngine::postsolve() { } // Postsolve for each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl; } @@ -718,16 +722,18 @@ void TheoryEngine::notifyRestart() { d_interrupted = false; // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \ - theoryOf(THEORY)->notifyRestart(); \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasNotifyRestart \ + && d_logicInfo.isTheoryEnabled(THEORY)) \ + { \ + theoryOf(THEORY)->notifyRestart(); \ } // notify each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder& learned) @@ -736,16 +742,17 @@ void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder& learned) d_interrupted = false; // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \ - theoryOf(THEORY)->ppStaticLearn(in, learned); \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) \ + { \ + theoryOf(THEORY)->ppStaticLearn(in, learned); \ } // static learning for each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; } bool TheoryEngine::isRelevant(Node lit) const @@ -1089,14 +1096,14 @@ void TheoryEngine::declareSepHeap(TypeNode locT, TypeNode dataT) } // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT +#ifdef CVC5_FOR_EACH_THEORY_STATEMENT +#undef CVC5_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ +#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ theoryOf(THEORY)->declareSepHeap(locT, dataT); // notify each theory using the statement above - CVC4_FOR_EACH_THEORY; + CVC5_FOR_EACH_THEORY; // remember the types we have set d_sepLocType = locT; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 814aa7ee4..357343a3c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -353,7 +353,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ Debug("model") << "Add substitution in model " << x << " -> " << t << std::endl; d_substitutions.addSubstitution( x, t, invalidateCache ); } else { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS Node oldX = d_substitutions.getSubstitution(x); // check that either the old substitution is the same, or it now maps to the new substitution if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) { @@ -363,7 +363,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ << "old mapping: " << d_substitutions.apply(oldX) << "\n" << "new mapping: " << d_substitutions.apply(t); } -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ } } diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index a8dd647f0..c06c6cd89 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -459,7 +459,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) bool evaluable = false; // Set to true if a term in the current equivalence class has been given an // assignment exclusion set. - bool hasESet CVC4_UNUSED = false; + bool hasESet CVC5_UNUSED = false; // Set to true if we found that a term in the current equivalence class has // been given an assignment exclusion set, and we have not seen this term // as part of a previous assignment exclusion group. In other words, when @@ -838,7 +838,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) isCorecursive = dt.isCodatatype() && (!dt.isFinite(t) || dt.isRecursiveSingleton(t)); } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS bool isUSortFiniteRestricted = false; if (options::finiteModelFind()) { @@ -861,7 +861,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) } Trace("model-builder") << " Assign phase, working on type: " << t << endl; - bool assignable, evaluable CVC4_UNUSED; + bool assignable, evaluable CVC5_UNUSED; std::map<Node, Assigner>::iterator itAssigner; std::map<Node, Node>::iterator itAssignerM; set<Node>* repSet = typeRepSet.getSet(t); @@ -935,7 +935,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) success = true; Trace("model-builder-debug") << "Check if excluded : " << n << std::endl; -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS if (isUSortFiniteRestricted) { // must not involve uninterpreted constants beyond cardinality @@ -1012,7 +1012,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) } } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS // Assert that all representatives have been converted to constants for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) { @@ -1024,7 +1024,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) Assert(false); } } -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ Trace("model-builder") << "Copy representatives to model..." << std::endl; tm->d_reps.clear(); @@ -1081,7 +1081,7 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, TheoryModel* m) void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS if (tm->hasApproximations()) { // models with approximations may fail the assertions below @@ -1125,7 +1125,7 @@ void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm) } } } -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ // builder-specific debugging debugModel(tm); diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 84d9ad03d..4ad449517 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -125,7 +125,7 @@ class TypeEnumerator { // On Mac clang, there appears to be a code generation bug in an exception // block here. For now, there doesn't appear a good workaround; just disable // assertions on that setup. -#if defined(CVC4_ASSERTIONS) && !(defined(__clang__)) +#if defined(CVC5_ASSERTIONS) && !(defined(__clang__)) if(d_te->isFinished()) { try { **d_te; @@ -145,7 +145,7 @@ class TypeEnumerator { Assert(false) << "didn't expect a NoMoreValuesException to be thrown"; } } -#endif /* CVC4_ASSERTIONS && !(APPLE || clang) */ +#endif /* CVC5_ASSERTIONS && !(APPLE || clang) */ return d_te->isFinished(); } Node operator*() @@ -153,7 +153,7 @@ class TypeEnumerator { // On Mac clang, there appears to be a code generation bug in an exception // block above (and perhaps here, too). For now, there doesn't appear a // good workaround; just disable assertions on that setup. -#if defined(CVC4_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__)) +#if defined(CVC5_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__)) try { Node n = **d_te; Assert(n.isConst()) << "Term " << n @@ -164,9 +164,9 @@ class TypeEnumerator { Assert(isFinished()); throw; } -#else /* CVC4_ASSERTIONS && !(APPLE || clang) */ +#else /* CVC5_ASSERTIONS && !(APPLE || clang) */ return **d_te; -#endif /* CVC4_ASSERTIONS && !(APPLE || clang) */ +#endif /* CVC5_ASSERTIONS && !(APPLE || clang) */ } TypeEnumerator& operator++() { diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 5fbbd3700..17c2d5a5c 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1387,7 +1387,7 @@ void EqualityEngine::getExplanation( cache[cacheKey] = eqp; // We can only explain the nodes that got merged -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS bool canExplain = getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind() || (d_done && isConstant(t1Id) && isConstant(t2Id)); @@ -2385,7 +2385,7 @@ EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet( bool EqualityEngine::hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNodeId rhsId) const { EqualityPair eq(lhsId, rhsId); bool propagated = d_propagatedDisequalities.find(eq) != d_propagatedDisequalities.end(); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS bool stored = d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end(); Assert(propagated == stored) << "These two should be in sync"; #endif @@ -2439,7 +2439,7 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs Assert(d_disequalityReasonsMap.find(pair1) == d_disequalityReasonsMap.end()) << "There can't be a proof if you're adding a new one"; DisequalityReasonRef ref(d_deducedDisequalityReasonsSize, d_deducedDisequalityReasons.size()); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS // Check that the reasons are valid for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i) { diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 0586da6a0..b52e39ebc 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -370,7 +370,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) { Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl; } } - CVC4_FALLTHROUGH; + CVC5_FALLTHROUGH; case kind::XOR: // commutative binary operator handling return n[1] < n[0] ? NodeManager::currentNM()->mkNode(k, n[1], n[0]) : Node(n); @@ -438,7 +438,7 @@ void SymmetryBreaker::assertFormula(TNode phi) { d_permutations.insert(p); } d_template.reset(); - bool good CVC4_UNUSED = d_template.match(phi); + bool good CVC5_UNUSED = d_template.match(phi); Assert(good); } } diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 806b0dd8e..bad06b716 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -150,7 +150,7 @@ public: * differ from the input due to theory-rewriting and preprocessing, * as well as CNF conversion */ - Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT; + Node ensureLiteral(TNode n) CVC5_WARN_UNUSED_RESULT; /** * This returns the theory-preprocessed form of term n. The theory |