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/expr | |
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/expr')
-rw-r--r-- | src/expr/attribute.cpp | 2 | ||||
-rw-r--r-- | src/expr/attribute.h | 2 | ||||
-rw-r--r-- | src/expr/dtype.cpp | 4 | ||||
-rw-r--r-- | src/expr/dtype.h | 2 | ||||
-rw-r--r-- | src/expr/dtype_cons.cpp | 4 | ||||
-rw-r--r-- | src/expr/dtype_selector.cpp | 4 | ||||
-rw-r--r-- | src/expr/kind_template.h | 2 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 4 | ||||
-rwxr-xr-x | src/expr/mkexpr | 4 | ||||
-rwxr-xr-x | src/expr/mkkind | 4 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 4 | ||||
-rw-r--r-- | src/expr/node.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 8 | ||||
-rw-r--r-- | src/expr/node_value.h | 4 | ||||
-rw-r--r-- | src/expr/proof_node.h | 4 | ||||
-rw-r--r-- | src/expr/sequence.h | 2 | ||||
-rw-r--r-- | src/expr/type_node.h | 2 |
17 files changed, 30 insertions, 30 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 1cb8adad6..ce617079e 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -36,7 +36,7 @@ bool AttributeManager::inGarbageCollection() const { void AttributeManager::debugHook(int debugFlag) { /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS! * debugHook() is an empty function for the purpose of debugging - * the AttributeManager without recompiling all of CVC4. + * the AttributeManager without recompiling all of cvc5. * Formally this is a nop. */ } diff --git a/src/expr/attribute.h b/src/expr/attribute.h index e42338bbb..b58cd45a9 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -211,7 +211,7 @@ public: /** * debugHook() is an empty function for the purpose of debugging - * the AttributeManager without recompiling all of CVC4. + * the AttributeManager without recompiling all of cvc5. * Formally this is a nop. */ void debugHook(int debugFlag); diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 66331f5c7..07b8aa5f1 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -895,8 +895,8 @@ const std::vector<std::shared_ptr<DTypeConstructor> >& DType::getConstructors() std::ostream& operator<<(std::ostream& os, const DType& dt) { - // can only output datatypes in the CVC4 native language - language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); + // can only output datatypes in the cvc5 native language + language::SetLanguage::Scope ls(os, language::output::LANG_CVC); dt.toStream(os); return os; } diff --git a/src/expr/dtype.h b/src/expr/dtype.h index da16729cc..6fd334e02 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -90,7 +90,7 @@ class DTypeConstructor; * allow the datatype to construct the necessary testers and selectors. * * An additional point to make is that we want to ease the burden on - * both the parser AND the users of the CVC4 API, so this class takes + * both the parser AND the users of the cvc5 API, so this class takes * on the task of generating its own selectors and testers, for * instance. That means that, after reifying the DType with the * NodeManager, the parser needs to go through the (now-resolved) diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 8d6194b06..99e5ad8ac 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -678,8 +678,8 @@ void DTypeConstructor::toStream(std::ostream& out) const std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor) { - // can only output datatypes in the CVC4 native language - language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); + // can only output datatypes in the cvc5 native language + language::SetLanguage::Scope ls(os, language::output::LANG_CVC); ctor.toStream(os); return os; } diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp index d6a3923df..98a07b2c9 100644 --- a/src/expr/dtype_selector.cpp +++ b/src/expr/dtype_selector.cpp @@ -78,8 +78,8 @@ void DTypeSelector::toStream(std::ostream& out) const std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg) { - // can only output datatypes in the CVC4 native language - language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); + // can only output datatypes in the cvc5 native language + language::SetLanguage::Scope ls(os, language::output::LANG_CVC); arg.toStream(os); return os; } diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 5fa1d99ff..6e2362e84 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -36,7 +36,7 @@ enum Kind_t } // namespace kind -// import Kind into the "CVC4" namespace but keep the individual kind +// import Kind into the "cvc5" namespace but keep the individual kind // constants under kind:: typedef ::cvc5::kind::Kind_t Kind; diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 0747b97fa..1271c2e64 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -33,7 +33,7 @@ namespace kind { namespace metakind { /** - * Static, compile-time information about types T representing CVC4 + * Static, compile-time information about types T representing cvc5 * constants: * * typename ConstantMap<T>::OwningTheory @@ -51,7 +51,7 @@ struct ConstantMap; /** * Static, compile-time information about kinds k and what type their - * corresponding CVC4 constants are: + * corresponding cvc5 constants are: * * typename ConstantMapReverse<k>::T * diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 0be51c71c..64a99d406 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -1,8 +1,8 @@ #!/usr/bin/env bash # # mkexpr -# 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 {expr,expr_manager}.{h,cpp} # from template files and a list of theory kinds. Basically it just diff --git a/src/expr/mkkind b/src/expr/mkkind index 53e63af6e..117b3bb9e 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -1,8 +1,8 @@ #!/usr/bin/env bash # # mkkind -# 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 kind.h (and also # type_properties.h) from a template and a list of theory kinds. diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 52fe070e6..a5801b9fe 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -1,8 +1,8 @@ #!/usr/bin/env bash # # mkmetakind -# 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 metakind.h from a template # and a list of theory kinds. diff --git a/src/expr/node.h b/src/expr/node.h index 181fc2e52..9014016b9 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -124,7 +124,7 @@ typedef NodeTemplate<true> Node; * creation. If this is returned as a TNode rather than a Node, the * count drops to zero, marking the expression as eligible for reclamation.) * - * More guidelines on when to use TNodes is available in the CVC4 + * More guidelines on when to use TNodes is available in the cvc5 * Developer's Guide: * http://cvc4.cs.stanford.edu/wiki/Developer%27s_Guide#Dealing_with_expressions_.28Nodes_and_TNodes.29 */ @@ -395,7 +395,7 @@ public: * these functions, as they may only be needed in CNF conversion, * where it's pointless to do a lazy isAtomic determination by * searching through the DAG, and storing it, since the result will - * only be used once. For more details see the 4/27/2010 CVC4 + * only be used once. For more details see the 4/27/2010 cvc5 * developer's meeting notes at: * * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5ca6823d9..528cdcfc7 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -344,7 +344,7 @@ class NodeManager * these functions, as they may only be needed in CNF conversion, * where it's pointless to do a lazy isAtomic determination by * searching through the DAG, and storing it, since the result will - * only be used once. For more details see the 4/27/2010 CVC4 + * only be used once. For more details see the 4/27/2010 cvc5 * developer's meeting notes at: * * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 @@ -364,7 +364,7 @@ class NodeManager * lookup is done on the name. If you mkVar("a", type) and then * mkVar("a", type) again, you have two variables. The NodeManager * version of this is private to avoid internal uses of mkVar() from - * within CVC4. Such uses should employ SkolemManager::mkSkolem() instead. + * within cvc5. Such uses should employ SkolemManager::mkSkolem() instead. */ Node mkVar(const std::string& name, const TypeNode& type); Node* mkVarPtr(const std::string& name, const TypeNode& type); @@ -390,7 +390,7 @@ class NodeManager explicit NodeManager(); ~NodeManager(); - /** The node manager in the current public-facing CVC4 library context */ + /** The node manager in the current public-facing cvc5 library context */ static NodeManager* currentNM() { return s_current; } /** Get this node manager's skolem manager */ SkolemManager* getSkolemManager() { return d_skManager.get(); } @@ -1093,7 +1093,7 @@ class NodeManager * previous thread-global <code>NodeManager</code> when it is * destroyed, effectively maintaining a set of nested * <code>NodeManager</code> scopes. This is especially useful on - * public-interface calls into the CVC4 library, where CVC4's notion + * public-interface calls into the cvc5 library, where cvc5's notion * of the "current" <code>NodeManager</code> should be set to match * the calling context. See, for example, the implementations of * public calls in the <code>SmtEngine</code> class. diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 3aa927bdb..c45fadb5c 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -426,7 +426,7 @@ inline void NodeValue::inc() { ++d_rc; Assert(NodeManager::currentNM() != NULL) << "No current NodeManager on incrementing of NodeValue: " - "maybe a public CVC4 interface function is missing a " + "maybe a public cvc5 interface function is missing a " "NodeManagerScope ?"; NodeManager::currentNM()->markRefCountMaxedOut(this); } @@ -439,7 +439,7 @@ inline void NodeValue::dec() { if(__builtin_expect( ( d_rc == 0 ), false )) { Assert(NodeManager::currentNM() != NULL) << "No current NodeManager on destruction of NodeValue: " - "maybe a public CVC4 interface function is missing a " + "maybe a public cvc5 interface function is missing a " "NodeManagerScope ?"; NodeManager::currentNM()->markForDeletion(this); } diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index 08d2a0245..f8d71f703 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -80,8 +80,8 @@ struct ProofNodeHashFunction * An external proof checker is expected to formalize the ProofNode only in * terms of *witness* forms. * - * However, the rest of CVC4 sees only the *Skolem* form of arguments and - * conclusions in ProofNode, since this is what is used throughout CVC4. + * However, the rest of cvc5 sees only the *Skolem* form of arguments and + * conclusions in ProofNode, since this is what is used throughout cvc5. */ class ProofNode { diff --git a/src/expr/sequence.h b/src/expr/sequence.h index 40cadb858..8bf7abeea 100644 --- a/src/expr/sequence.h +++ b/src/expr/sequence.h @@ -28,7 +28,7 @@ class NodeTemplate; typedef NodeTemplate<true> Node; class TypeNode; -/** The CVC4 sequence class +/** The cvc5 sequence class * * This data structure is the domain of values for the sequence type. */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index d1b5edf22..318d59613 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -420,7 +420,7 @@ public: /** is closed enumerable type * * This returns true if this type has an enumerator that produces constants - * that are fully handled by CVC4's quantifier-free theory solvers. Examples + * that are fully handled by cvc5's quantifier-free theory solvers. Examples * of types that are not closed enumerable are: * (1) uninterpreted sorts, * (2) arrays, |