diff options
| -rw-r--r-- | src/expr/CMakeLists.txt | 13 | ||||
| -rwxr-xr-x | src/expr/mkmetakind | 21 | ||||
| -rw-r--r-- | src/expr/node_manager_template.cpp | 6 | ||||
| -rw-r--r-- | src/expr/node_manager_template.h (renamed from src/expr/node_manager.h) | 4 | ||||
| -rw-r--r-- | src/theory/arith/kinds | 6 | ||||
| -rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 2 |
6 files changed, 39 insertions, 13 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 9a89dfbe6..e00e938e0 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -47,7 +47,6 @@ libcvc5_add_sources( node_builder.h node_converter.cpp node_converter.h - node_manager.h node_manager_attributes.h node_self_iterator.h node_trie.cpp @@ -104,6 +103,7 @@ libcvc5_add_sources(GENERATED metakind.cpp metakind.h node_manager.cpp + node_manager.h type_checker.cpp type_properties.cpp type_properties.h @@ -178,6 +178,16 @@ add_custom_command( ) add_custom_command( + OUTPUT node_manager.h + COMMAND + ${mkmetakind_script} + ${CMAKE_CURRENT_LIST_DIR}/node_manager_template.h + ${KINDS_FILES} + > ${CMAKE_CURRENT_BINARY_DIR}/node_manager.h + DEPENDS mkmetakind node_manager_template.h ${KINDS_FILES} +) + +add_custom_command( OUTPUT node_manager.cpp COMMAND ${mkmetakind_script} @@ -204,6 +214,7 @@ add_custom_target(gen-expr metakind.cpp metakind.h node_manager.cpp + node_manager.h type_checker.cpp type_properties.cpp type_properties.h diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index d5f6d9b1a..3ee7dc59b 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -54,6 +54,7 @@ metakind_ubchildren= metakind_lbchildren= metakind_operatorKinds= metakind_mkConst= +metakind_mkConstDelete= seen_theory=false seen_theory_builtin=false @@ -295,8 +296,23 @@ TypeNode NodeManager::mkTypeConst<${class}>(const ${class}& val) } " metakind_mkConst="${metakind_mkConst} -template -Node NodeManager::mkConst(Kind k, const ${class}& val); +template<> +Node NodeManager::mkConst(Kind k, const ${class}& val) +{ + return mkConstInternal<Node, ${class}>(k, val); +} +" + elif [[ "${payload_seen}" != true ]]; then + metakind_mkConstDelete="${metakind_mkConstDelete} +template<> +Node NodeManager::mkConst<${class}>(const ${class}& val) = delete; +" + metakind_mkConst="${metakind_mkConst} +template<> +Node NodeManager::mkConst(Kind k, const ${class}& val) +{ + return mkConstInternal<Node, ${class}>(k, val); +} " fi @@ -442,6 +458,7 @@ for var in \ metakind_lbchildren \ metakind_operatorKinds \ metakind_mkConst \ + metakind_mkConstDelete \ template \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 4f235a53a..944d7fe66 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -1158,12 +1158,6 @@ TNode NodeManager::operatorOf(Kind k) return d_operators[k]; } -template <class T> -Node NodeManager::mkConst(Kind k, const T& val) -{ - return mkConstInternal<Node, T>(k, val); -} - template <class NodeClass, class T> NodeClass NodeManager::mkConstInternal(Kind k, const T& val) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager_template.h index b2682661e..073077344 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager_template.h @@ -1206,6 +1206,10 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, return NodeBuilder(this, kind).append(children).constructTypeNode(); } +// clang-format off +${metakind_mkConstDelete} +// clang-format off + } // namespace cvc5 #endif /* CVC5__NODE_MANAGER_H */ diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index f577b4109..e496cf335 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -54,13 +54,13 @@ constant DIVISIBLE_OP \ sort REAL_TYPE \ Cardinality::REALS \ well-founded \ - "NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))" \ + "NodeManager::currentNM()->mkConstReal(Rational(0))" \ "expr/node_manager.h" \ "real type" sort INTEGER_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))" \ + "NodeManager::currentNM()->mkConstInt(Rational(0))" \ "expr/node_manager.h" \ "integer type" @@ -73,7 +73,7 @@ constant CONST_RATIONAL \ constant CONST_INTEGER \ class \ - Rational \ + Rational+ \ ::cvc5::RationalHashFunction \ "util/rational.h" \ "a multiple-precision integer constant; payload is an instance of the cvc5::Rational class" diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 1ccb67490..634f27294 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -2089,7 +2089,7 @@ Node SequencesRewriter::rewriteUpdate(Node node) NodeManager* nm = NodeManager::currentNM(); Node idx = nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, s), - nm->mkNode(PLUS, i, nm->mkConst(Rational(1)))); + nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1)))); Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s, idx, x)); return returnRewrite(node, ret, Rewrite::UPD_REV); } |