From: Andres Noetzli Date: Wed, 9 Jun 2021 20:14:38 +0000 (-0700) Subject: Update CVC4 URLs/macros (#6666) X-Git-Tag: cvc5-1.0.0~1614 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=73a3f516e3179141a71d3201e908bebf3061ead0;p=cvc5.git Update CVC4 URLs/macros (#6666) --- diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index e8f7737a6..a1421cf12 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -179,8 +179,8 @@ class CVC5_EXPORT Result bool isNotEntailed() const; /** - * Return true if query was a checkEntailed() () query and cvc5 was not able - * to determine if it is entailed. + * Return true if query was a checkEntailed() query and cvc5 was not able to + * determine if it is entailed. */ bool isEntailmentUnknown() const; @@ -2683,7 +2683,7 @@ class CVC5_EXPORT Statistics /** * Retrieve the statistic with the given name. * Asserts that a statistic with the given name actually exists and throws - * a `CVC4ApiRecoverableException` if it does not. + * a `CVC5ApiRecoverableException` if it does not. * @param name Name of the statistic. * @return The statistic with the given name. */ diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index be9083960..2ec190360 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1850,9 +1850,10 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(const Op& op, const std::vector& children) const` * - * Note: We currently support the creation of constant arrays, but under some + * @note We currently support the creation of constant arrays, but under some * conditions when there is a chain of equalities connecting two constant - * arrays, the solver doesn't know what to do and aborts (Issue #1667). + * arrays, the solver doesn't know what to do and aborts (Issue #1667). */ CONST_ARRAY, /** diff --git a/src/api/java/cvc5/Result.java b/src/api/java/cvc5/Result.java index bd142b985..4399df1e4 100644 --- a/src/api/java/cvc5/Result.java +++ b/src/api/java/cvc5/Result.java @@ -122,7 +122,7 @@ public class Result extends AbstractPointer /** * Return true if query was a checkSat() or checkSatAssuming() query and - * CVC4 was not able to determine (un)satisfiability. + * cvc5 was not able to determine (un)satisfiability. */ public boolean isSatUnknown() { @@ -153,8 +153,8 @@ public class Result extends AbstractPointer private native boolean isNotEntailed(long pointer); /** - * Return true if query was a checkEntailed() () query and CVC4 was not able - * to determine if it is entailed. + * Return true if query was a checkEntailed() query and cvc5 was not able to + * determine if it is entailed. */ public boolean isEntailmentUnknown() { diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 80d5bac57..61951841b 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -99,8 +99,8 @@ std::string Configuration::getVersionExtra() { return CVC5_EXTRAVERSION; } std::string Configuration::copyright() { std::stringstream ss; - ss << "Copyright (c) 2009-2020 by the authors and their institutional\n" - << "affiliations listed at http://cvc4.cs.stanford.edu/authors\n\n"; + ss << "Copyright (c) 2009-2021 by the authors and their institutional\n" + << "affiliations listed at https://cvc5.github.io/people.html\n\n"; if (Configuration::licenseIsGpl()) { ss << "This build of cvc5 uses GPLed libraries, and is thus covered by\n" @@ -185,7 +185,7 @@ std::string Configuration::copyright() { ss << "cvc5 is statically linked against these libraries. To recompile\n" "this version of cvc5 with different versions of these libraries\n" "follow the instructions on " - "https://github.com/CVC4/CVC4/blob/master/INSTALL.md\n\n"; + "https://github.com/cvc5/cvc5/blob/master/INSTALL.md\n\n"; } } diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h index e9169d9b2..4e7bde4b5 100644 --- a/src/decision/decision_engine_old.h +++ b/src/decision/decision_engine_old.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC4__DECISION__DECISION_ENGINE_OLD_H -#define CVC4__DECISION__DECISION_ENGINE_OLD_H +#ifndef CVC5__DECISION__DECISION_ENGINE_OLD_H +#define CVC5__DECISION__DECISION_ENGINE_OLD_H #include "base/output.h" #include "context/cdo.h" @@ -147,4 +147,4 @@ class DecisionEngineOld } // namespace cvc5 -#endif /* CVC4__DECISION__DECISION_ENGINE_H */ +#endif /* CVC5__DECISION__DECISION_ENGINE_H */ diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 80732eab4..feacc8837 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -260,10 +260,9 @@ void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll) // Notice we only want to do this for sygus datatypes that are user-provided. // At the moment, the condition !allow_all implies the grammar is // user-provided and hence may require a default constant. - // TODO (https://github.com/CVC4/cvc4-projects/issues/38): - // In an API for SyGuS, it probably makes more sense for the user to - // explicitly add the "any constant" constructor with a call instead of - // passing a flag. This would make the block of code unnecessary. + // For the SyGuS API, we could consider requiring the user to explicitly add + // the "any constant" constructor with a call instead of passing a flag. This + // would make the block of code unnecessary. if (allowConst && !allowAll) { // if I don't already have a constant (0-ary constructor) diff --git a/src/expr/node.h b/src/expr/node.h index fdcfcbe5f..5f5d3a976 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -126,7 +126,7 @@ typedef NodeTemplate Node; * * More guidelines on when to use TNodes is available in the cvc5 * Developer's Guide: - * https://github.com/CVC4/CVC4/wiki/Developer-Guide#dealing-with-expressions-nodes-and-tnodes + * https://github.com/cvc5/cvc5/wiki/Developer-Guide#dealing-with-expressions-nodes-and-tnodes */ typedef NodeTemplate TNode;