diff options
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; |