Update CVC4 URLs/macros (#6666)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index e8f7737a6ddf4ecca5f4db0d7a9369156736f942..a1421cf12e67f9963f37164af4f353d09dbcde24 100644 (file)
--- 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 be9083960c7af44846ab66ce123ea5a37626624c..2ec190360fd61a18dcef17730d87dc0b46675a6c 100644 (file)
--- 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<Term>& 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 <a href="https://github.com/CVC4/CVC4/issues/1667">#1667</a>).
+   * arrays, the solver doesn't know what to do and aborts (Issue <a
+   * href="https://github.com/cvc5/cvc5/issues/1667">#1667</a>).
    */
   CONST_ARRAY,
   /**

diff --git a/src/api/java/cvc5/Result.java b/src/api/java/cvc5/Result.java
index bd142b98537832faaf9f9b656f49e2b390fd6ff4..4399df1e4f8511b8fb19428eee72c9bc634742b5 100644 (file)
--- 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 80d5bac579e08f959bc370a61fa6a3ba3a4af9ff..61951841b29a6eeb33c1871e92edcdd14a93394c 100644 (file)
--- 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 e9169d9b2ef0312f09c8e052ad1225eb4457b410..4e7bde4b53178ee957a3871aa484b2979689bc1d 100644 (file)
--- 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 80732eab493b9246f48b9437641f521f0ef17eb1..feacc8837015e8c66c3cc820944171b965426e05 100644 (file)
--- 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 fdcfcbe5f28c08ee4f3f0aafd60546c59e24918e..5f5d3a976e2d4b55cfcd0e1ba7e1449b068ebec0 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -126,7 +126,7 @@ typedef NodeTemplate<true> 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<false> TNode;