diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-15 13:04:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-15 20:04:55 +0000 |
commit | 77bca094a140b35341257f125a55212ff0108250 (patch) | |
tree | 1d3369b9be5fc4c3e8cb279ae5ea662e59cbcb3e /src/theory | |
parent | 63647b1d79df6f287ea6599958b16fce44b8271d (diff) |
Rename occurrences of CVC4 to CVC5. (#6351)
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
Diffstat (limited to 'src/theory')
38 files changed, 228 insertions, 231 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index f299459f8..536a38739 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -629,8 +629,8 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& var, if (s_verbosity >= 2) { - // CVC4Message() << v << " "; - // d_vars.printModel(v, CVC4Message()); + // CVC5Message() << v << " "; + // d_vars.printModel(v, CVC5Message()); } int type; @@ -764,8 +764,8 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{ if (s_verbosity >= 2) { - CVC4Message() << v << " "; - d_vars.printModel(v, CVC4Message()); + CVC5Message() << v << " "; + d_vars.printModel(v, CVC5Message()); } int type; @@ -868,9 +868,9 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{ if(len >= rowLengthReq){ if (s_verbosity >= 1) { - CVC4Message() << "high row " << r << " " << len << " " << avgRowLength + CVC5Message() << "high row " << r << " " << len << " " << avgRowLength << " " << dir << endl; - d_vars.printModel(r, CVC4Message()); + d_vars.printModel(r, CVC5Message()); } ret.push_back(ArithRatPair(r, Rational(dir))); } @@ -891,9 +891,9 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{ if(ubScore >= .9 || lbScore >= .9){ if (s_verbosity >= 1) { - CVC4Message() << "high col " << c << " " << bc << " " << ubScore + CVC5Message() << "high col " << c << " " << bc << " " << ubScore << " " << lbScore << " " << dir << endl; - d_vars.printModel(c, CVC4Message()); + d_vars.printModel(c, CVC5Message()); } ret.push_back(ArithRatPair(c, Rational(c))); } @@ -1016,14 +1016,14 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const : glp_get_col_stat(prob, glpk_index); if (s_verbosity >= 2) { - CVC4Message() << "assignment " << vi << endl; + CVC5Message() << "assignment " << vi << endl; } bool useDefaultAssignment = false; switch(status){ case GLP_BS: - // CVC4Message() << "basic" << endl; + // CVC5Message() << "basic" << endl; newBasis.add(vi); useDefaultAssignment = true; break; @@ -1032,7 +1032,7 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const if(!mip){ if (s_verbosity >= 2) { - CVC4Message() << "non-basic lb" << endl; + CVC5Message() << "non-basic lb" << endl; } newValues.set(vi, d_vars.getLowerBound(vi)); }else{// intentionally fall through otherwise @@ -1043,7 +1043,7 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const if(!mip){ if (s_verbosity >= 2) { - CVC4Message() << "non-basic ub" << endl; + CVC5Message() << "non-basic ub" << endl; } newValues.set(vi, d_vars.getUpperBound(vi)); }else {// intentionally fall through otherwise @@ -1060,7 +1060,7 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const if(useDefaultAssignment){ if (s_verbosity >= 2) { - CVC4Message() << "non-basic other" << endl; + CVC5Message() << "non-basic other" << endl; } double newAssign; @@ -1077,7 +1077,7 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const && roughlyEqual(newAssign, d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA))) { - // CVC4Message() << " to lb" << endl; + // CVC5Message() << " to lb" << endl; newValues.set(vi, d_vars.getLowerBound(vi)); } @@ -1087,20 +1087,20 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA))) { newValues.set(vi, d_vars.getUpperBound(vi)); - // CVC4Message() << " to ub" << endl; + // CVC5Message() << " to ub" << endl; } else { double rounded = round(newAssign); if (roughlyEqual(newAssign, rounded)) { - // CVC4Message() << "roughly equal " << rounded << " " << newAssign << + // CVC5Message() << "roughly equal " << rounded << " " << newAssign << // " " << oldAssign << endl; newAssign = rounded; } else { - // CVC4Message() << "not roughly equal " << rounded << " " << + // CVC5Message() << "not roughly equal " << rounded << " " << // newAssign << " " << oldAssign << endl; } @@ -1117,26 +1117,26 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const if (roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))) { - // CVC4Message() << " to prev value" << newAssign << " " << oldAssign + // CVC5Message() << " to prev value" << newAssign << " " << oldAssign // << endl; proposal = d_vars.getAssignment(vi); } if (d_vars.strictlyLessThanLowerBound(vi, proposal)) { - // CVC4Message() << " round to lb " << d_vars.getLowerBound(vi) << + // CVC5Message() << " round to lb " << d_vars.getLowerBound(vi) << // endl; proposal = d_vars.getLowerBound(vi); } else if (d_vars.strictlyGreaterThanUpperBound(vi, proposal)) { - // CVC4Message() << " round to ub " << d_vars.getUpperBound(vi) << + // CVC5Message() << " round to ub " << d_vars.getUpperBound(vi) << // endl; proposal = d_vars.getUpperBound(vi); } else { - // CVC4Message() << " use proposal" << proposal << " " << oldAssign + // CVC5Message() << " use proposal" << proposal << " " << oldAssign // << endl; } newValues.set(vi, proposal); diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index d74385d3b..33b0e2e26 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -120,12 +120,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol) Assert(toAdd != ARITHVAR_SENTINEL); Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl; - // CVC4Message() << toRemove << " " << toAdd << endl; + // CVC5Message() << toRemove << " " << toAdd << endl; d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]); Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl; - // CVC4Message() << needsToBeAdded.size() << "to go" << endl; + // CVC5Message() << needsToBeAdded.size() << "to go" << endl; needsToBeAdded.remove(toAdd); bool conflict = processSignals(); diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index dcd699d88..fc2506f84 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -185,7 +185,7 @@ std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){ return o; } -void Constraint::debugPrint() const { CVC4Message() << *this << endl; } +void Constraint::debugPrint() const { CVC5Message() << *this << endl; } ValueCollection::ValueCollection() : d_lowerBound(NullConstraint), diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 1ad23f8ca..1cd092abc 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -776,8 +776,8 @@ void DioSolver::debugPrintTrail(DioSolver::TrailIndex i) const{ const SumPair& eq = d_trail[i].d_eq; const Polynomial& proof = d_trail[i].d_proof; - CVC4Message() << "d_trail[" << i << "].d_eq = " << eq.getNode() << endl; - CVC4Message() << "d_trail[" << i << "].d_proof = " << proof.getNode() << endl; + CVC5Message() << "d_trail[" << i << "].d_eq = " << eq.getNode() << endl; + CVC5Message() << "d_trail[" << i << "].d_proof = " << proof.getNode() << endl; } void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){ diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 13cc29a58..543cb9587 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -104,15 +104,15 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ { if (result == Result::UNSAT) { - CVC4Message() << "diff order found unsat" << endl; + CVC5Message() << "diff order found unsat" << endl; } else if (d_errorSet.errorEmpty()) { - CVC4Message() << "diff order found model" << endl; + CVC5Message() << "diff order found model" << endl; } else { - CVC4Message() << "diff order missed" << endl; + CVC5Message() << "diff order missed" << endl; } } } @@ -136,15 +136,15 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ { if (result == Result::UNSAT) { - CVC4Message() << "restricted var order found unsat" << endl; + CVC5Message() << "restricted var order found unsat" << endl; } else if (d_errorSet.errorEmpty()) { - CVC4Message() << "restricted var order found model" << endl; + CVC5Message() << "restricted var order found model" << endl; } else { - CVC4Message() << "restricted var order missed" << endl; + CVC5Message() << "restricted var order missed" << endl; } } } diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index de13f4eb9..49c17172f 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -78,9 +78,9 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){ Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl; Assert(d_conflictVariables.empty()); - //if (verbose) + // if (verbose) //{ - // CVC4Message() << "fcFindModel(" << instance << ") trivial" << endl; + // CVC5Message() << "fcFindModel(" << instance << ") trivial" << endl; //} return Result::SAT; } @@ -95,15 +95,15 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ d_conflictVariables.purge(); if (verbose) { - CVC4Message() << "fcFindModel(" << instance << ") early conflict" << endl; + CVC5Message() << "fcFindModel(" << instance << ") early conflict" << endl; } Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl; Assert(d_conflictVariables.empty()); return Result::UNSAT; }else if(d_errorSet.errorEmpty()){ - //if (verbose) + // if (verbose) //{ - // CVC4Message() << "fcFindModel(" << instance << ") fixed itself" << endl; + // CVC5Message() << "fcFindModel(" << instance << ") fixed itself" << endl; //} Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl; if (verbose) Assert(!d_errorSet.moreSignals()); @@ -133,25 +133,25 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ ++(d_statistics.d_fcFoundUnsat); if (verbose) { - CVC4Message() << "fc found unsat"; + CVC5Message() << "fc found unsat"; } }else if(d_errorSet.errorEmpty()){ ++(d_statistics.d_fcFoundSat); if (verbose) { - CVC4Message() << "fc found model"; + CVC5Message() << "fc found model"; } }else{ ++(d_statistics.d_fcMissed); if (verbose) { - CVC4Message() << "fc missed"; + CVC5Message() << "fc missed"; } } } if (verbose) { - CVC4Message() << "(" << instance << ") pivots " << d_pivots << endl; + CVC5Message() << "(" << instance << ") pivots " << d_pivots << endl; } Assert(!d_errorSet.moreSignals()); @@ -523,7 +523,7 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit } if(degenerate(w) && selected.describesPivot()){ ArithVar leaving = selected.leaving(); - CVC4Message() << "degenerate " << leaving << ", atBounds " + CVC5Message() << "degenerate " << leaving << ", atBounds " << d_linEq.basicsAtBounds(selected) << ", len " << d_tableau.basicRowLength(leaving) << ", bc " << d_linEq.debugBasicAtBoundCount(leaving) << endl; @@ -574,8 +574,8 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit if (verbose) { - CVC4Message() << "conflict variable " << selected << endl; - CVC4Message() << ss.str(); + CVC5Message() << "conflict variable " << selected << endl; + CVC5Message() << ss.str(); } if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); } @@ -791,7 +791,7 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ if (verbose) { - debugDualLike(w, CVC4Message(), instance, prevFocusSize, prevErrorSize); + debugDualLike(w, CVC5Message(), instance, prevFocusSize, prevErrorSize); } Assert(debugDualLike( w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize)); diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index f9f88cddf..e1eda5d85 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -90,7 +90,7 @@ parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root p operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)" -operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)" +operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in cvc5, as integer is a subtype of real)" # CAST_TO_REAL is added to distinguish between integers casted to reals internally, and # integers casted to reals or using the API \ diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 57dbdfc82..82cc02815 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -167,12 +167,12 @@ void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){ Assert(toAdd != ARITHVAR_SENTINEL); Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl; - CVC4Message() << toRemove << " " << toAdd << endl; + CVC5Message() << toRemove << " " << toAdd << endl; d_tableau.pivot(toRemove, toAdd, d_trackCallback); d_basicVariableUpdates(toAdd); Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl; - CVC4Message() << needsToBeAdded.size() << "to go" << endl; + CVC5Message() << needsToBeAdded.size() << "to go" << endl; needsToBeAdded.remove(toAdd); } } diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index f8a12065f..4321800f2 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/cad/constraints.h @@ -75,7 +75,7 @@ class Constraints ConstraintVector d_constraints; /** - * A mapping from CVC4 variables to poly variables. + * A mapping from cvc5 variables to poly variables. */ VariableMapper d_varMapper; diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index 5c4391d68..b0d785b2a 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -69,7 +69,7 @@ std::pair<std::size_t, std::size_t> getRootIDs( * @param zero A node representing Rational(0) * @param k The index of the root (starting with 1) * @param poly The polynomial whose root shall be considered - * @param vm A variable mapper from CVC4 to libpoly variables + * @param vm A variable mapper from cvc5 to libpoly variables */ Node mkIRP(const Node& var, Kind rel, diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index 27a711f75..b493455a6 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -89,7 +89,7 @@ class CADProofGenerator * and the origin of this is constraint. * * @param var The variable for which the interval is excluded - * @param vm A variable mapper between CVC4 and libpoly variables + * @param vm A variable mapper between cvc5 and libpoly variables * @param p The polynomial of the constraint * @param a The current partial assignment * @param sc The sign condition of the constraint @@ -113,7 +113,7 @@ class CADProofGenerator * @param i The concrete interval that is excluded * @param a The current partial assignment * @param s The sample point that is refuted for var - * @param vm A variable mapper between CVC4 and libpoly variables + * @param vm A variable mapper between cvc5 and libpoly variables */ std::vector<Node> constructCell(Node var, const CACInterval& i, diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index ed50b85cf..6e96cfe7b 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -371,12 +371,12 @@ void ICPSolver::check() void ICPSolver::reset(const std::vector<Node>& assertions) { - Unimplemented() << "ICPSolver requires CVC4 to be configured with LibPoly"; + Unimplemented() << "ICPSolver requires cvc5 to be configured with LibPoly"; } void ICPSolver::check() { - Unimplemented() << "ICPSolver requires CVC4 to be configured with LibPoly"; + Unimplemented() << "ICPSolver requires cvc5 to be configured with LibPoly"; } #endif /* CVC5_POLY_IMP */ diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index d80dacd78..e5fa31aad 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -218,7 +218,7 @@ struct CollectMonomialData { CollectMonomialData(VariableMapper& v) : d_vm(v) {} - /** Mapper from poly variables to CVC4 variables */ + /** Mapper from poly variables to cvc5 variables */ VariableMapper& d_vm; /** Collections of the monomial terms */ std::vector<Node> d_terms; diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 3213df0ce..db64320d5 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -37,17 +37,17 @@ class BoundInference; namespace nl { -/** Bijective mapping between CVC4 variables and poly variables. */ +/** Bijective mapping between cvc5 variables and poly variables. */ struct VariableMapper { - /** A mapping from CVC4 variables to poly variables. */ + /** A mapping from cvc5 variables to poly variables. */ std::map<cvc5::Node, poly::Variable> mVarCVCpoly; - /** A mapping from poly variables to CVC4 variables. */ + /** A mapping from poly variables to cvc5 variables. */ std::map<poly::Variable, cvc5::Node> mVarpolyCVC; /** Retrieves the according poly variable. */ poly::Variable operator()(const cvc5::Node& n); - /** Retrieves the according CVC4 variable. */ + /** Retrieves the according cvc5 variable. */ cvc5::Node operator()(const poly::Variable& n); }; diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 1b22bc81c..fc2ed8fa9 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -97,7 +97,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ d_conflictVariables.purge(); if (verbose) { - CVC4Message() << "fcFindModel(" << instance << ") early conflict" << endl; + CVC5Message() << "fcFindModel(" << instance << ") early conflict" << endl; } Debug("soi::findModel") << "fcFindModel("<< instance <<") early conflict" << endl; Assert(d_conflictVariables.empty()); @@ -131,25 +131,25 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ ++(d_statistics.d_soiFoundUnsat); if (verbose) { - CVC4Message() << "fc found unsat"; + CVC5Message() << "fc found unsat"; } }else if(d_errorSet.errorEmpty()){ ++(d_statistics.d_soiFoundSat); if (verbose) { - CVC4Message() << "fc found model"; + CVC5Message() << "fc found model"; } }else{ ++(d_statistics.d_soiMissed); if (verbose) { - CVC4Message() << "fc missed"; + CVC5Message() << "fc missed"; } } } if (verbose) { - CVC4Message() << "(" << instance << ") pivots " << d_pivots << endl; + CVC5Message() << "(" << instance << ") pivots " << d_pivots << endl; } Assert(!d_errorSet.moreSignals()); @@ -360,7 +360,7 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes } if(degenerate(w) && selected.describesPivot()){ ArithVar leaving = selected.leaving(); - CVC4Message() << "degenerate " << leaving << ", atBounds " + CVC5Message() << "degenerate " << leaving << ", atBounds " << d_linEq.basicsAtBounds(selected) << ", len " << d_tableau.basicRowLength(leaving) << ", bc " << d_linEq.debugBasicAtBoundCount(leaving) << endl; @@ -411,8 +411,8 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes if (verbose) { - CVC4Message() << "conflict variable " << selected << endl; - CVC4Message() << ss.str(); + CVC5Message() << "conflict variable " << selected << endl; + CVC5Message() << ss.str(); } if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); } @@ -971,7 +971,7 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ if (verbose) { - debugSOI(w, CVC4Message(), instance); + debugSOI(w, CVC5Message(), instance); } Assert(debugSOI(w, Debug("dualLike"), instance)); } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index e7ff27413..4687922a0 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3103,7 +3103,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ // mipRes = approxSolver->solveMIP(true); // } // d_errorSet.reduceToSignals(); -// //CVC4Message() << "here" << endl; +// //CVC5Message() << "here" << endl; // if(mipRes == ApproximateSimplex::ApproxSat){ // mipSolution = approxSolver->extractMIP(); // d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution); @@ -3121,7 +3121,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ // options::arithStandardCheckVarOrderPivots.set(pass2Limit); // if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = // simplex.findModel(false); } -// //CVC4Message() << "done" << endl; +// //CVC5Message() << "done" << endl; // } // break; // case ApproximateSimplex::ApproxUnsat: @@ -3147,13 +3147,13 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ // }else{ // if(d_qflraStatus == Result::SAT_UNKNOWN){ -// //CVC4Message() << "got sat unknown" << endl; +// //CVC5Message() << "got sat unknown" << endl; // vector<ArithVar> toCut = cutAllBounded(); // if(toCut.size() > 0){ // //branchVector(toCut); // emmittedConflictOrSplit = true; // }else{ -// //CVC4Message() << "splitting" << endl; +// //CVC5Message() << "splitting" << endl; // d_qflraStatus = simplex.findModel(noPivotLimit); // } diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index e2f69f19d..dffe0baf3 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -1,7 +1,7 @@ # kinds [for builtin theory] -*- sh -*- # # This "kinds" file is written in a domain-specific language for -# declaring CVC4 kinds. Comments are marked with #, as this line is. +# declaring cvc5 kinds. Comments are marked with #, as this line is. # # The first non-blank, non-comment line in this file must be a theory # declaration: diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index b7a62be5e..3b9b14fb7 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -74,7 +74,7 @@ class DatatypesRewriter : public TheoryRewriter * Stream := cons( head : Int, tail : Stream ) * The stream 1,0,1,0,1,0... when written in mu-notation is the term: * mu x. cons( 1, mu y. cons( 0, x ) ) - * This is represented in CVC4 by the Node: + * This is represented in cvc5 by the Node: * cons( 1, cons( 0, c[1] ) ) * where c[1] is a uninterpreted constant datatype with Debruijn index 1, * indicating that c[1] is nested underneath 1 level on the path to the diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index a62fd4894..a2306cc6a 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -633,7 +633,7 @@ symbolicProposition symbolicBitVector<isSigned>::operator>( } /*** Type conversion ***/ -// CVC4 nodes make no distinction between signed and unsigned, thus ... +// cvc5 nodes make no distinction between signed and unsigned, thus ... template <bool isSigned> symbolicBitVector<true> symbolicBitVector<isSigned>::toSigned(void) const { diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 4225be84a..1db635cda 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -38,7 +38,7 @@ #endif #ifdef CVC5_SYM_SYMBOLIC_EVAL -// This allows debugging of the CVC4 symbolic back-end. +// This allows debugging of the cvc5 symbolic back-end. // By enabling this and disabling constant folding in the rewriter, // SMT files that have operations on constants will be evaluated // during the encoding step, which means that the expressions @@ -54,7 +54,7 @@ namespace fp { * This is a symfpu symbolic "back-end". It allows the library to be used to * construct bit-vector expressions that compute floating-point operations. * This is effectively the glue between symfpu's notion of "signed bit-vector" - * and CVC4's node. + * and cvc5's node. */ namespace symfpuSymbolic { @@ -103,7 +103,7 @@ typedef traits::bwt bwt; class nodeWrapper : public Node { protected: -/* CVC5_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues. +/* CVC5_SYM_SYMBOLIC_EVAL is for debugging cvc5 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. @@ -255,7 +255,7 @@ class symbolicBitVector : public nodeWrapper symbolicProposition operator>(const symbolicBitVector<isSigned> &op) const; /*** Type conversion ***/ - // CVC4 nodes make no distinction between signed and unsigned, thus these are + // cvc5 nodes make no distinction between signed and unsigned, thus these are // trivial symbolicBitVector<true> toSigned(void) const; symbolicBitVector<false> toUnsigned(void) const; diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h index 1e917c942..c166d0c0a 100644 --- a/src/theory/incomplete_id.h +++ b/src/theory/incomplete_id.h @@ -24,7 +24,7 @@ namespace cvc5 { namespace theory { /** - * Reasons for incompleteness in CVC4. + * Reasons for incompleteness in cvc5. */ enum class IncompleteId { diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index e85917e00..bb099114d 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -22,7 +22,7 @@ * Theory, the Theory should rethrow the same exception (via "throw;" * in the exception block) rather than return, as the Interrupted * instance might contain additional information needed for the - * proper management of CVC4 components. + * proper management of cvc5 components. */ #include "cvc5_private.h" diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index fa06e93a4..9d18d5145 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -30,12 +30,12 @@ namespace cvc5 { /** * A LogicInfo instance describes a collection of theory modules and some * basic configuration about them. Conceptually, it provides a background - * context for all operations in CVC4. Typically, when CVC4's SmtEngine + * context for all operations in cvc5. Typically, when cvc5's SmtEngine * is created, it is issued a setLogic() command indicating features of the * assertions and queries to follow---for example, whether quantifiers are * used, whether integers or reals (or both) will be used, etc. * - * Most places in CVC4 will only ever need to access a const reference to an + * Most places in cvc5 will only ever need to access a const reference to an * instance of this class. Such an instance is generally set by the SmtEngine * when setLogic() is called. However, mutating member functions are also * provided by this class so that it can be used as a more general mechanism diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index c27ff0fb1..baef55679 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -1,8 +1,8 @@ #!/usr/bin/env bash # # mkrewriter -# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010-2013 The CVC4 Project +# Morgan Deters <mdeters@cs.nyu.edu> for cvc5 +# Copyright (c) 2010-2013 The cvc5 Project # # The purpose of this script is to create rewriter_tables.h from a template # and a list of theory kinds. diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index b07b1b46a..4312da406 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -1,8 +1,8 @@ #!/usr/bin/env bash # # mktheorytraits -# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010-2013 The CVC4 Project +# Morgan Deters <mdeters@cs.nyu.edu> for cvc5 +# Copyright (c) 2010-2013 The cvc5 Project # # The purpose of this script is to create theory_traits.h from a template # and a list of theory kinds. diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 8634890b4..684751292 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -31,77 +31,78 @@ namespace inst { class CandidateGenerator; /** InstMatchGenerator class -* -* This is the default generator class for non-simple single triggers, that is, -* triggers composed of a single term with nested term applications. -* For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple -* triggers. -* -* Handling non-simple triggers is done by constructing a linked list of -* InstMatchGenerator classes (see mkInstMatchGenerator), where each -* InstMatchGenerator has a "d_next" pointer. If d_next is NULL, -* then this is the end of the InstMatchGenerator and the last -* InstMatchGenerator is responsible for finalizing the instantiation. -* -* For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list: -* -* [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL -* -* In a call to getNextMatch, -* if we match against a ground term f( b, c ), then the first InstMatchGenerator -* in this list binds y to b, and tells the InstMatchGenerator [ f( x, a ) ] to -* match f-applications in the equivalence class of c. -* -* CVC4 employs techniques that ensure that the number of instantiations -* is worst-case polynomial wrt the number of ground terms. -* Consider the axiom/pattern/context (EX2) : -* -* axiom : forall x1 x2 x3 x4. F[ x1...x4 ] -* -* trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) -* -* ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 ) -* -* If E-matching were applied exhaustively, then x1, x2, x3, x4 would be -* instantiated with all combinations of c_1, ... c_100, giving 100^4 -* instantiations. -* -* Instead, we enforce that at most 1 instantiation is produced for a -* ( pattern, ground term ) pair per round. Meaning, only one instantiation is -* generated when matching P( a, a, a, a ) against the generator -* [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of -* Reynolds, Vampire 2016. -* -* To enforce these policies, we use a flag "d_active_add" which dictates the -* behavior of the last element in the linked list. If d_active_add is -* true -> a call to getNextMatch(...) returns 1 only if adding the -* instantiation via a call to IMGenerator::sendInstantiation(...) -* successfully enqueues a lemma via a call to -* Instantiate::addInstantiation(...). This call may fail e.g. if we -* have already added the instantiation, or the instantiation is -* entailed. -* false -> a call to getNextMatch(...) returns 1 whenever an m is -* constructed, where typically the caller would use m. -* This is important since a return value >0 signals that the current matched -* terms should be flushed. Consider the above example (EX1), where -* [ f(y,f(x,a)) ] is being matched against f(b,c), -* [ f(x,a) ] is being matched against f(d,a) where c=f(d,a) -* A successfully added instantiation { x->d, y->b } here signals we should -* not produce further instantiations that match f(y,f(x,a)) with f(b,c). -* -* A number of special cases of triggers are covered by this generator (see -* implementation of initialize), including : -* Literal triggers, e.g. x >= a, ~x = y -* Selector triggers, e.g. head( x ) -* Triggers with invertible subterms, e.g. f( x+1 ) -* Variable triggers, e.g. x -* -* All triggers above can be in the context of an equality, e.g. -* { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to -* ground terms in the equivalence class of b. -* { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any -* ground terms not in the equivalence class of b. -*/ + * + * This is the default generator class for non-simple single triggers, that is, + * triggers composed of a single term with nested term applications. + * For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple + * triggers. + * + * Handling non-simple triggers is done by constructing a linked list of + * InstMatchGenerator classes (see mkInstMatchGenerator), where each + * InstMatchGenerator has a "d_next" pointer. If d_next is NULL, + * then this is the end of the InstMatchGenerator and the last + * InstMatchGenerator is responsible for finalizing the instantiation. + * + * For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list: + * + * [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL + * + * In a call to getNextMatch, + * if we match against a ground term f( b, c ), then the first + * InstMatchGenerator in this list binds y to b, and tells the + * InstMatchGenerator [ f( x, a ) ] to match f-applications in the equivalence + * class of c. + * + * cvc5 employs techniques that ensure that the number of instantiations + * is worst-case polynomial wrt the number of ground terms. + * Consider the axiom/pattern/context (EX2) : + * + * axiom : forall x1 x2 x3 x4. F[ x1...x4 ] + * + * trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) + * + * ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 ) + * + * If E-matching were applied exhaustively, then x1, x2, x3, x4 would be + * instantiated with all combinations of c_1, ... c_100, giving 100^4 + * instantiations. + * + * Instead, we enforce that at most 1 instantiation is produced for a + * ( pattern, ground term ) pair per round. Meaning, only one instantiation is + * generated when matching P( a, a, a, a ) against the generator + * [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of + * Reynolds, Vampire 2016. + * + * To enforce these policies, we use a flag "d_active_add" which dictates the + * behavior of the last element in the linked list. If d_active_add is + * true -> a call to getNextMatch(...) returns 1 only if adding the + * instantiation via a call to IMGenerator::sendInstantiation(...) + * successfully enqueues a lemma via a call to + * Instantiate::addInstantiation(...). This call may fail e.g. if we + * have already added the instantiation, or the instantiation is + * entailed. + * false -> a call to getNextMatch(...) returns 1 whenever an m is + * constructed, where typically the caller would use m. + * This is important since a return value >0 signals that the current matched + * terms should be flushed. Consider the above example (EX1), where + * [ f(y,f(x,a)) ] is being matched against f(b,c), + * [ f(x,a) ] is being matched against f(d,a) where c=f(d,a) + * A successfully added instantiation { x->d, y->b } here signals we should + * not produce further instantiations that match f(y,f(x,a)) with f(b,c). + * + * A number of special cases of triggers are covered by this generator (see + * implementation of initialize), including : + * Literal triggers, e.g. x >= a, ~x = y + * Selector triggers, e.g. head( x ) + * Triggers with invertible subterms, e.g. f( x+1 ) + * Variable triggers, e.g. x + * + * All triggers above can be in the context of an equality, e.g. + * { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to + * ground terms in the equivalence class of b. + * { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any + * ground terms not in the equivalence class of b. + */ class InstMatchGenerator : public IMGenerator { public: /** destructor */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h index e15d476a3..afe43a604 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -37,7 +37,7 @@ namespace inst { * InstMatchGeneratorMultiLinear at the head and a list of trailing * InstMatchGenerators. * - * CVC4 employs techniques that ensure that the number of instantiations + * cvc5 employs techniques that ensure that the number of instantiations * is worst-case polynomial wrt the number of ground terms, where this class * lifts this policy to multi-triggers. In particular consider * diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index dbfae5382..172e93c12 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -39,66 +39,62 @@ namespace inst { class IMGenerator; class InstMatchGenerator; /** A collection of nodes representing a trigger. -* -* This class encapsulates all implementations of E-matching in CVC4. -* Its primary use is as a utility of the quantifiers module InstantiationEngine -* (see theory/quantifiers/ematching/instantiation_engine.h) which uses Trigger to make -* appropriate calls to Instantiate::addInstantiation(...) -* (see theory/instantiate.h) for the instantiate utility of the quantifiers -* engine (d_quantEngine) associated with this trigger. These calls -* queue instantiation lemmas to the output channel of TheoryQuantifiers during -* a full effort check. -* -* Concretely, a Trigger* t is used in the following way during a full effort -* check. Assume that t is associated with quantified formula q (see field d_f). -* We call : -* -* // setup initial information -* t->resetInstantiationRound(); -* // will produce instantiations based on matching with all terms -* t->reset( Node::null() ); -* // add all instantiations based on E-matching with this trigger and the -* // current context -* t->addInstantiations(); -* -* This will result in (a set of) calls to -* Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn), -* where m1...mn are InstMatch objects. These calls add the corresponding -* instantiation lemma for (q,mi) on the output channel associated with -* d_quantEngine. -* -* The Trigger class is wrapper around an underlying IMGenerator class, which -* implements various forms of E-matching for its set of nodes (d_nodes), which -* is refered to in the literature as a "trigger". A trigger is a set of terms -* whose free variables are the bound variables of a quantified formula q, -* and that is used to guide instantiations for q (for example, see "Efficient -* E-Matching for SMT Solvers" by de Moura et al). -* -* For example of an instantiation lemma produced by E-matching : -* -* quantified formula : forall x. P( x ) -* trigger : P( x ) -* ground context : ~P( a ) -* -* Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a } -* which is used to generate the instantiation lemma : -* (forall x. P( x )) => P( a ) -* -* Terms that are provided as input to a Trigger class via mkTrigger -* should be in "instantiation constant form", see TermUtil::getInstConstantNode. -* Say we have quantified formula q whose AST is the Node -* (FORALL -* (BOUND_VAR_LIST x) -* (NOT (P x)) -* (INST_PATTERN_LIST (INST_PATTERN (P x)))) -* then TermUtil::getInstConstantNode( q, (P x) ) = (P IC) where -* IC = TermUtil::getInstantiationConstant( q, i ). -* Trigger expects as input (P IC) to represent the Trigger (P x). This form -* ensures that references to bound variables are unique to quantified formulas, -* which is required to ensure the correctness of instantiation lemmas we -* generate. -* -*/ + * + * This class encapsulates all implementations of E-matching in cvc5. + * Its primary use is as a utility of the quantifiers module InstantiationEngine + * (see theory/quantifiers/ematching/instantiation_engine.h) which uses Trigger + * to make appropriate calls to Instantiate::addInstantiation(...) (see + * theory/instantiate.h) for the instantiate utility of the quantifiers engine + * (d_quantEngine) associated with this trigger. These calls queue + * instantiation lemmas to the output channel of TheoryQuantifiers during a full + * effort check. + * + * Concretely, a Trigger* t is used in the following way during a full effort + * check. Assume that t is associated with quantified formula q (see field d_f). + * We call : + * + * // setup initial information + * t->resetInstantiationRound(); + * // will produce instantiations based on matching with all terms + * t->reset( Node::null() ); + * // add all instantiations based on E-matching with this trigger and the + * // current context + * t->addInstantiations(); + * + * This will result in (a set of) calls to + * Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn), + * where m1...mn are InstMatch objects. These calls add the corresponding + * instantiation lemma for (q,mi) on the output channel associated with + * d_quantEngine. + * + * The Trigger class is wrapper around an underlying IMGenerator class, which + * implements various forms of E-matching for its set of nodes (d_nodes), which + * is refered to in the literature as a "trigger". A trigger is a set of terms + * whose free variables are the bound variables of a quantified formula q, + * and that is used to guide instantiations for q (for example, see "Efficient + * E-Matching for SMT Solvers" by de Moura et al). + * + * For example of an instantiation lemma produced by E-matching : + * + * quantified formula : forall x. P( x ) + * trigger : P( x ) + * ground context : ~P( a ) + * + * Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a } + * which is used to generate the instantiation lemma : + * (forall x. P( x )) => P( a ) + * + * Terms that are provided as input to a Trigger class via mkTrigger + * should be in "instantiation constant form", see + * TermUtil::getInstConstantNode. Say we have quantified formula q whose AST is + * the Node (FORALL (BOUND_VAR_LIST x) (NOT (P x)) (INST_PATTERN_LIST + * (INST_PATTERN (P x)))) then TermUtil::getInstConstantNode( q, (P x) ) = (P + * IC) where IC = TermUtil::getInstantiationConstant( q, i ). Trigger expects as + * input (P IC) to represent the Trigger (P x). This form ensures that + * references to bound variables are unique to quantified formulas, which is + * required to ensure the correctness of instantiation lemmas we generate. + * + */ class Trigger { friend class IMGenerator; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 4545b2d39..841cd4ab9 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -675,7 +675,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i Node ev = d_quant_models[f].evaluate(fmfmc, inst); if (ev == d_true) { - CVC4Message() << "WARNING: instantiation was true! " << f << " " + CVC5Message() << "WARNING: instantiation was true! " << f << " " << mcond[i] << std::endl; AlwaysAssert(false); } diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 585032dc4..5eba46657 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -104,7 +104,7 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) if( addedLemmas==0 ){ Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl; - //CVC4 will answer SAT or unknown + // cvc5 will answer SAT or unknown if( Trace.isOn("fmf-consistent") ){ Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index f89bdf1f2..1abbd1989 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -173,7 +173,7 @@ void QuantAttributes::computeAttributes( Node q ) { { Node f = qa.d_fundef_f; if( d_fun_defs.find( f )!=d_fun_defs.end() ){ - CVC4Message() << "Cannot define function " << f << " more than once." + CVC5Message() << "Cannot define function " << f << " more than once." << std::endl; AlwaysAssert(false); } diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 7597054d9..3c3dd8d84 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -166,7 +166,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { std::stringstream ss; - ss << "--sygus-rr-query-gen detected unsoundness in CVC4 on input " << qy + ss << "--sygus-rr-query-gen detected unsoundness in cvc5 on input " << qy << "!" << std::endl; ss << "This query has a model : " << std::endl; std::vector<Node> pt; @@ -176,7 +176,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) { ss << " " << d_vars[i] << " -> " << pt[i] << std::endl; } - ss << "but CVC4 answered unsat!" << std::endl; + ss << "but cvc5 answered unsat!" << std::endl; AlwaysAssert(false) << ss.str(); } if (options::sygusQueryGenDumpFiles() diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index 2f21a50e1..431156c03 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -36,7 +36,7 @@ namespace cvc5 { template <typename T> -static CVC4ostream& operator<<(CVC4ostream& out, const std::vector<T>& v) +static CVC5ostream& operator<<(CVC5ostream& out, const std::vector<T>& v) { out << "[ "; std::copy(v.begin(), v.end(), std::ostream_iterator<T>(out, " ")); diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 564779f6a..0f15727e0 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -63,7 +63,7 @@ nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be i # forall y. ( exists x1...xn. P[x1...xn] ^ t[x1...xn] = y ) <=> (member y C) # where y ranges over the element type of the (set) type of the comprehension. # Notice that since all sets must be interpreted as finite, this means that -# CVC4 will not be able to construct a model for any set comprehension such +# cvc5 will not be able to construct a model for any set comprehension such # that there are infinitely many y that satisfy the left hand side of the # equivalence above. The same limitation occurs more generally when combining # finite sets with quantified formulas. diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 76edde5ae..2ca8696b0 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -51,7 +51,7 @@ public: * This class implements inference schemes described in Meng et al. CADE 2017 * for handling quantifier-free constraints in the theory of relations. * - * In CVC4, relations are represented as sets of tuples. The theory of + * In cvc5, relations are represented as sets of tuples. The theory of * relations includes constraints over operators, e.g. TRANSPOSE, JOIN and so * on, which apply to sets of tuples. * diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 4148f51b3..5c4b36043 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -214,7 +214,7 @@ void SubstitutionMap::print(ostream& out) const { } } -void SubstitutionMap::debugPrint() const { print(CVC4Message.getStream()); } +void SubstitutionMap::debugPrint() const { print(CVC5Message.getStream()); } } // namespace theory diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3eacdaa20..e870860c5 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -94,7 +94,7 @@ class PropEngine; * This is essentially an abstraction for a collection of theories. A * TheoryEngine provides services to a PropEngine, making various * T-solvers look like a single unit to the propositional part of - * CVC4. + * cvc5. */ class TheoryEngine { diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 25f87de2c..166df3c80 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1023,7 +1023,7 @@ int SortModel::addSplit(Region* r) } if (ss == b_t) { - CVC4Message() << "Bad split " << s << std::endl; + CVC5Message() << "Bad split " << s << std::endl; AlwaysAssert(false); } } @@ -1420,7 +1420,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ if( !it->second->hasCardinalityAsserted() ){ Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl; - // CVC4Message() << "Error: constraint asserted before cardinality + // CVC5Message() << "Error: constraint asserted before cardinality // for " << it->first << std::endl; Unimplemented(); } } |