diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-04-21 10:21:34 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-21 10:21:34 -0700 |
commit | ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch) | |
tree | a7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /src/expr | |
parent | 86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (diff) |
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/CMakeLists.txt | 4 | ||||
-rw-r--r-- | src/expr/node.h | 16 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 16 | ||||
-rw-r--r-- | src/expr/node_value.h | 2 | ||||
-rw-r--r-- | src/expr/symbol_manager.h | 4 | ||||
-rw-r--r-- | src/expr/symbol_table.h | 6 | ||||
-rw-r--r-- | src/expr/type_node.h | 2 |
8 files changed, 12 insertions, 42 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 17bd49ea7..28cf23f57 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -13,7 +13,7 @@ # The build system configuration. ## -libcvc4_add_sources( +libcvc5_add_sources( array_store_all.cpp array_store_all.h ascription_type.cpp @@ -124,7 +124,7 @@ libcvc4_add_sources( uninterpreted_constant.h ) -libcvc4_add_sources(GENERATED +libcvc5_add_sources(GENERATED kind.cpp kind.h metakind.cpp diff --git a/src/expr/node.h b/src/expr/node.h index 9014016b9..5480b38ae 100644 --- 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: - * http://cvc4.cs.stanford.edu/wiki/Developer%27s_Guide#Dealing_with_expressions_.28Nodes_and_TNodes.29 + * https://github.com/CVC4/CVC4/wiki/Developer-Guide#dealing-with-expressions-nodes-and-tnodes */ typedef NodeTemplate<false> TNode; @@ -389,20 +389,6 @@ public: return NodeTemplate(d_nv->getChild(i)); } - /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance).. - * - * It has been decided for now to hold off on implementations of - * 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 cvc5 - * developer's meeting notes at: - * - * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 - */ - // bool containsDecision(); // is "atomic" - // bool properlyContainsDecision(); // maybe not atomic but all children are - /** * Returns true if this node represents a constant * @return true if const diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 42be16742..70f221091 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -708,7 +708,7 @@ TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vecto if( index==types.size() ){ if( d_data.isNull() ){ std::stringstream sst; - sst << "__cvc4_tuple"; + sst << "__cvc5_tuple"; for (unsigned i = 0; i < types.size(); ++ i) { sst << "_" << types[i]; } @@ -738,7 +738,7 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor { if( d_data.isNull() ){ std::stringstream sst; - sst << "__cvc4_record"; + sst << "__cvc5_record"; for (const std::pair<std::string, TypeNode>& i : rec) { sst << "_" << i.first << "_" << i.second; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 528cdcfc7..6cda50075 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -338,20 +338,6 @@ class NodeManager expr::NodeValue* child[N]; };/* struct NodeManager::NVStorage<N> */ - /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance).. - * - * It has been decided for now to hold off on implementations of - * 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 cvc5 - * developer's meeting notes at: - * - * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 - */ - // bool containsDecision(TNode); // is "atomic" - // bool properlyContainsDecision(TNode); // all children are atomic - // undefined private copy constructor (disallow copy) NodeManager(const NodeManager&) = delete; @@ -1079,7 +1065,7 @@ class NodeManager /** * This function gives developers a hook into the NodeManager. - * This can be changed in node_manager.cpp without recompiling most of cvc4. + * This can be changed in node_manager.cpp without recompiling most of cvc5. * * debugHook is a debugging only function, and should not be present in * any published code! diff --git a/src/expr/node_value.h b/src/expr/node_value.h index c45fadb5c..5f5ac7d86 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -330,7 +330,7 @@ class NodeValue /** The ID (0 is reserved for the null value) */ uint64_t d_id : NBITS_ID; - /** The expression's reference count. @see cvc4::Node. */ + /** The expression's reference count. */ uint32_t d_rc : NBITS_REFCOUNT; /** Kind of the expression */ diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 53057d0b1..6cd0a1467 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -23,7 +23,7 @@ #include <string> #include "api/cpp/cvc5.h" -#include "cvc4_export.h" +#include "cvc5_export.h" #include "expr/symbol_table.h" namespace cvc5 { @@ -36,7 +36,7 @@ namespace cvc5 { * Like SymbolTable, this class currently lives in src/expr/ since it uses * context-dependent data structures. */ -class CVC4_EXPORT SymbolManager +class CVC5_EXPORT SymbolManager { public: SymbolManager(api::Solver* s); diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index cd80c0eba..ddf26f9da 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -23,7 +23,7 @@ #include <vector> #include "base/exception.h" -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { @@ -33,7 +33,7 @@ class Sort; class Term; } // namespace api -class CVC4_EXPORT ScopeException : public Exception +class CVC5_EXPORT ScopeException : public Exception { }; @@ -42,7 +42,7 @@ class CVC4_EXPORT ScopeException : public Exception * nested scoping rules for declarations, with separate bindings for expressions * and types. */ -class CVC4_EXPORT SymbolTable +class CVC5_EXPORT SymbolTable { public: /** Create a symbol table. */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 318d59613..32a1befbd 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -695,8 +695,6 @@ public: * Returns the leastUpperBound in the extended type lattice of the two types. * If this is \top, i.e. there is no inhabited type that contains both, * a TypeNode such that isNull() is true is returned. - * - * For more information see: http://cvc4.cs.nyu.edu/wiki/Cvc4_Type_Lattice */ static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1); |