diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-09 17:22:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 17:22:07 -0700 |
commit | f87f038c5f0821d0fefb01cea00bfdec6004da91 (patch) | |
tree | d948178e1c0d2dc459a976f0d187d2d41a5437c0 /src/theory/arith/nl/cad_solver.cpp | |
parent | 550c49a7dd2b13ea29743458336f0c0a0fb6099a (diff) |
Rename CVC4_ macros to CVC5_. (#6327)
Diffstat (limited to 'src/theory/arith/nl/cad_solver.cpp')
-rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
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; |