From dc679ed380aabc62aadfbb4033c02c5a27ae903c Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 11 Mar 2021 11:05:58 -0800 Subject: [PATCH] Delete Expr layer. (#6117) --- src/CMakeLists.txt | 4 - src/api/cvc4cpp.cpp | 7 +- src/api/cvc4cpp.h | 2 - src/expr/CMakeLists.txt | 52 - src/expr/expr_manager_scope.h | 69 -- src/expr/expr_manager_template.cpp | 908 ------------------ src/expr/expr_manager_template.h | 463 --------- src/expr/expr_template.cpp | 703 -------------- src/expr/expr_template.h | 622 ------------ src/expr/node.h | 53 +- src/expr/node_manager.cpp | 5 +- src/expr/node_manager.h | 82 +- src/expr/type.cpp | 681 ------------- src/expr/type.h | 695 -------------- src/expr/type_node.h | 21 - src/expr/variable_type_map.h | 63 -- src/include/cvc4.h | 2 - src/preprocessing/passes/bv_to_int.cpp | 4 +- src/preprocessing/passes/int_to_bv.cpp | 15 +- src/preprocessing/passes/real_to_int.cpp | 8 +- src/printer/cvc/cvc_printer.cpp | 20 +- src/printer/smt2/smt2_printer.cpp | 4 +- src/proof/cnf_proof.h | 1 - src/prop/prop_engine.h | 1 + src/smt/assertions.cpp | 4 +- src/smt/expand_definitions.cpp | 6 +- src/smt/interpolation_solver.cpp | 6 +- src/smt/optimization_solver.h | 3 + src/smt/smt_engine.cpp | 6 +- .../datatypes/theory_datatypes_type_rules.h | 2 +- .../quantifiers/cegqi/ceg_dt_instantiator.cpp | 2 +- .../quantifiers/sygus/cegis_core_connective.h | 3 + .../quantifiers/sygus/sygus_grammar_cons.cpp | 7 +- .../quantifiers/sygus/sygus_grammar_norm.cpp | 2 +- .../quantifiers/sygus/sygus_process_conj.cpp | 5 +- .../quantifiers/sygus/synth_conjecture.cpp | 3 +- src/theory/sets/theory_sets_type_rules.h | 2 + src/theory/strings/type_enumerator.cpp | 4 +- src/theory/strings/type_enumerator.h | 2 +- src/theory/uf/equality_engine.cpp | 2 +- src/theory/uf/theory_uf_type_rules.h | 2 + test/api/ouroborous.cpp | 2 - test/api/smt2_compliance.cpp | 1 - test/unit/expr/node_black.cpp | 1 - test/unit/expr/node_traversal_black.cpp | 1 - test/unit/expr/symbol_table_black.cpp | 4 +- test/unit/expr/type_cardinality_black.cpp | 1 - test/unit/expr/type_node_white.cpp | 2 - test/unit/main/interactive_shell_black.cpp | 1 - test/unit/parser/parser_black.cpp | 2 - test/unit/test_node.h | 2 +- test/unit/test_smt.h | 4 +- test/unit/theory/theory_bv_white.cpp | 2 +- .../theory_quantifiers_bv_inverter_white.cpp | 26 +- test/unit/util/array_store_all_white.cpp | 2 - test/unit/util/datatype_black.cpp | 2 - 56 files changed, 85 insertions(+), 4514 deletions(-) delete mode 100644 src/expr/expr_manager_scope.h delete mode 100644 src/expr/expr_manager_template.cpp delete mode 100644 src/expr/expr_manager_template.h delete mode 100644 src/expr/expr_template.cpp delete mode 100644 src/expr/expr_template.h delete mode 100644 src/expr/type.cpp delete mode 100644 src/expr/type.h delete mode 100644 src/expr/variable_type_map.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ad06eb568..7759db20c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1207,12 +1207,8 @@ install(FILES expr/sequence.h expr/symbol_manager.h expr/symbol_table.h - expr/type.h expr/uninterpreted_constant.h - expr/variable_type_map.h - ${CMAKE_CURRENT_BINARY_DIR}/expr/expr.h ${CMAKE_CURRENT_BINARY_DIR}/expr/kind.h - ${CMAKE_CURRENT_BINARY_DIR}/expr/expr_manager.h DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/expr) install(FILES diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ea8165c4a..930ff895c 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -46,7 +46,6 @@ #include "expr/node.h" #include "expr/node_manager.h" #include "expr/sequence.h" -#include "expr/type.h" #include "expr/type_node.h" #include "options/main_options.h" #include "options/options.h" @@ -1024,10 +1023,6 @@ std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e) /* Sort */ /* -------------------------------------------------------------------------- */ -Sort::Sort(const Solver* slv, const CVC4::Type& t) - : d_solver(slv), d_type(new CVC4::TypeNode(TypeNode::fromType(t))) -{ -} Sort::Sort(const Solver* slv, const CVC4::TypeNode& t) : d_solver(slv), d_type(new CVC4::TypeNode(t)) { @@ -3272,7 +3267,7 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const Solver::Solver(Options* opts) { - d_nodeMgr.reset(new NodeManager(nullptr)); + d_nodeMgr.reset(new NodeManager()); d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), opts)); d_smtEngine->setSolver(this); Options& o = d_smtEngine->getOptions(); diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 77a2378de..968ed0522 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -64,7 +64,6 @@ class SmtEngine; class SygusConstraintCommand; class SygusInvConstraintCommand; class SynthFunCommand; -class Type; class TypeNode; class Options; class QueryCommand; @@ -718,7 +717,6 @@ class CVC4_PUBLIC Sort * @param t the internal type that is to be wrapped by this sort * @return the Sort */ - Sort(const Solver* slv, const CVC4::Type& t); Sort(const Solver* slv, const CVC4::TypeNode& t); /** diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 343d55800..3e8717986 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -27,7 +27,6 @@ libcvc4_add_sources( emptybag.h expr_iomanip.cpp expr_iomanip.h - expr_manager_scope.h kind_map.h lazy_proof.cpp lazy_proof.h @@ -94,14 +93,11 @@ libcvc4_add_sources( term_context_stack.h term_conversion_proof_generator.cpp term_conversion_proof_generator.h - type.cpp - type.h type_checker.h type_matcher.cpp type_matcher.h type_node.cpp type_node.h - variable_type_map.h datatype_index.h datatype_index.cpp dtype.h @@ -127,10 +123,6 @@ libcvc4_add_sources(GENERATED kind.h metakind.cpp metakind.h - expr.cpp - expr.h - expr_manager.cpp - expr_manager.h type_checker.cpp type_properties.h ) @@ -193,46 +185,6 @@ add_custom_command( DEPENDS mkmetakind metakind_template.cpp metakind.h ${KINDS_FILES} ) -add_custom_command( - OUTPUT expr.h - COMMAND - ${mkexpr_script} - ${CMAKE_CURRENT_LIST_DIR}/expr_template.h - ${KINDS_FILES} - > ${CMAKE_CURRENT_BINARY_DIR}/expr.h - DEPENDS mkexpr expr_template.h kind.h ${KINDS_FILES} -) - -add_custom_command( - OUTPUT expr.cpp - COMMAND - ${mkexpr_script} - ${CMAKE_CURRENT_LIST_DIR}/expr_template.cpp - ${KINDS_FILES} - > ${CMAKE_CURRENT_BINARY_DIR}/expr.cpp - DEPENDS mkexpr expr_template.cpp expr.h ${KINDS_FILES} -) - -add_custom_command( - OUTPUT expr_manager.h - COMMAND - ${mkexpr_script} - ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.h - ${KINDS_FILES} - > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.h - DEPENDS mkexpr expr_manager_template.h expr.h ${KINDS_FILES} -) - -add_custom_command( - OUTPUT expr_manager.cpp - COMMAND - ${mkexpr_script} - ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.cpp - ${KINDS_FILES} - > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.cpp - DEPENDS mkexpr expr_manager_template.cpp expr_manager.h ${KINDS_FILES} -) - add_custom_command( OUTPUT type_checker.cpp COMMAND @@ -249,10 +201,6 @@ add_custom_target(gen-expr kind.h metakind.cpp metakind.h - expr.cpp - expr.h - expr_manager.cpp - expr_manager.h type_checker.cpp type_properties.h ) diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h deleted file mode 100644 index a737c669b..000000000 --- a/src/expr/expr_manager_scope.h +++ /dev/null @@ -1,69 +0,0 @@ -/********************* */ -/*! \file expr_manager_scope.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__EXPR_MANAGER_SCOPE_H -#define CVC4__EXPR_MANAGER_SCOPE_H - -#include "expr/expr.h" -#include "expr/node_manager.h" -#include "expr/expr_manager.h" - -namespace CVC4 { - -/** - * Creates a NodeManagerScope with the underlying - * NodeManager of a given Expr or - * ExprManager. The NodeManagerScope is - * destroyed when the ExprManagerScope is destroyed. See - * NodeManagerScope for more information. - */ -// NOTE: Here, it seems ExprManagerScope is redundant, since we have -// NodeManagerScope already. However, without this class, we'd need -// Expr to be a friend of ExprManager, because in the implementation -// of Expr functions, it needs to set the current NodeManager -// correctly (and to do that it needs access to -// ExprManager::getNodeManager()). So, we make ExprManagerScope a -// friend of ExprManager's, since its implementation is simple to -// read and understand (and verify that it doesn't do any mischief). -// -// ExprManager::getNodeManager() can't just be made public, since -// ExprManager is exposed to clients of the library and NodeManager is -// not. Similarly, ExprManagerScope shouldn't go in expr_manager.h, -// since that's a public header. -class ExprManagerScope { - NodeManagerScope d_nms; -public: - inline ExprManagerScope(const Expr& e) : - d_nms(e.getExprManager() == NULL - ? NodeManager::currentNM() - : e.getExprManager()->getNodeManager()) { - } - inline ExprManagerScope(const Type& t) : - d_nms(t.getExprManager() == NULL - ? NodeManager::currentNM() - : t.getExprManager()->getNodeManager()) { - } - inline ExprManagerScope(const ExprManager& exprManager) : - d_nms(exprManager.getNodeManager()) { - } -};/* class ExprManagerScope */ - -}/* CVC4 namespace */ - -#endif /* CVC4__EXPR_MANAGER_SCOPE_H */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp deleted file mode 100644 index 414d8a611..000000000 --- a/src/expr/expr_manager_template.cpp +++ /dev/null @@ -1,908 +0,0 @@ -/********************* */ -/*! \file expr_manager_template.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Public-facing expression manager interface, implementation - ** - ** Public-facing expression manager interface, implementation. - **/ - -#include "expr/expr_manager.h" - -#include - -#include "expr/node_manager.h" -#include "expr/variable_type_map.h" -#include "expr/node_manager_attributes.h" -#include "options/options.h" -#include "util/statistics_registry.h" - -${includes} - -#ifdef CVC4_STATISTICS_ON - #define INC_STAT(kind) \ - { \ - if (d_exprStatistics[kind] == NULL) { \ - stringstream statName; \ - statName << "expr::ExprManager::" << kind; \ - d_exprStatistics[kind] = new IntStat(statName.str(), 0); \ - d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatistics[kind]); \ - } \ - ++ *(d_exprStatistics[kind]); \ - } -#define INC_STAT_VAR(type, bound_var) \ - { \ - TypeNode* isv_typeNode = Type::getTypeNode(type); \ - TypeConstant isv_type = isv_typeNode->getKind() == kind::TYPE_CONSTANT \ - ? isv_typeNode->getConst() \ - : LAST_TYPE; \ - if (d_exprStatisticsVars[isv_type] == NULL) \ - { \ - stringstream statName; \ - if (isv_type == LAST_TYPE) \ - { \ - statName << "expr::ExprManager::" \ - << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") \ - << ":Parameterized isv_type"; \ - } \ - else \ - { \ - statName << "expr::ExprManager::" \ - << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" \ - << isv_type; \ - } \ - d_exprStatisticsVars[isv_type] = new IntStat(statName.str(), 0); \ - d_nodeManager->getStatisticsRegistry()->registerStat( \ - d_exprStatisticsVars[isv_type]); \ - } \ - ++*(d_exprStatisticsVars[isv_type]); \ - } -#else - #define INC_STAT(kind) - #define INC_STAT_VAR(type, bound_var) -#endif - -using namespace std; -using namespace CVC4::kind; - -namespace CVC4 { - -ExprManager::ExprManager() : - d_nodeManager(new NodeManager(this)) { -#ifdef CVC4_STATISTICS_ON - for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { - d_exprStatistics[i] = NULL; - } - for (unsigned i = 0; i <= LAST_TYPE; ++ i) { - d_exprStatisticsVars[i] = NULL; - } -#endif -} - -ExprManager::~ExprManager() -{ - NodeManagerScope nms(d_nodeManager); - - try { - -#ifdef CVC4_STATISTICS_ON - for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { - if (d_exprStatistics[i] != NULL) { - d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatistics[i]); - delete d_exprStatistics[i]; - d_exprStatistics[i] = NULL; - } - } - for (unsigned i = 0; i <= LAST_TYPE; ++ i) { - if (d_exprStatisticsVars[i] != NULL) { - d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatisticsVars[i]); - delete d_exprStatisticsVars[i]; - d_exprStatisticsVars[i] = NULL; - } - } -#endif - - delete d_nodeManager; - d_nodeManager = NULL; - } catch(Exception& e) { - Warning() << "CVC4 threw an exception during cleanup." << std::endl - << e << std::endl; - } -} - -BooleanType ExprManager::booleanType() const { - NodeManagerScope nms(d_nodeManager); - return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()))); -} - -StringType ExprManager::stringType() const { - NodeManagerScope nms(d_nodeManager); - return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType()))); -} - -RegExpType ExprManager::regExpType() const { - NodeManagerScope nms(d_nodeManager); - return RegExpType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType()))); -} - -RealType ExprManager::realType() const { - NodeManagerScope nms(d_nodeManager); - return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType()))); -} - -IntegerType ExprManager::integerType() const { - NodeManagerScope nms(d_nodeManager); - return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()))); -} - -RoundingModeType ExprManager::roundingModeType() const { - NodeManagerScope nms(d_nodeManager); - return RoundingModeType(Type(d_nodeManager, new TypeNode(d_nodeManager->roundingModeType()))); -} - - -Expr ExprManager::mkExpr(Kind kind, Expr child1) { - const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - PrettyCheckArgument( - mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { - const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - PrettyCheckArgument( - mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(kind, - child1.getNode(), - child2.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) { - const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - PrettyCheckArgument( - mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(kind, - child1.getNode(), - child2.getNode(), - child3.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, - Expr child4) { - const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = 4 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - PrettyCheckArgument( - mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(kind, - child1.getNode(), - child2.getNode(), - child3.getNode(), - child4.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, - Expr child4, Expr child5) { - const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = 5 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - PrettyCheckArgument( - mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(kind, - child1.getNode(), - child2.getNode(), - child3.getNode(), - child4.getNode(), - child5.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Kind kind, const std::vector& children) -{ - const size_t nchildren = children.size(); - const kind::MetaKind mk = kind::metaKindOf(kind); - PrettyCheckArgument( - mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR, - kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - PrettyCheckArgument( - mk != kind::metakind::PARAMETERIZED || nchildren > 0, - kind, - "Terms with kind %s must have an operator expression as first argument", - kind::kindToString(kind).c_str()); - const size_t n = nchildren - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind), - kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), - maxArity(kind), - n); - - NodeManagerScope nms(d_nodeManager); - - vector nodes; - vector::const_iterator it = children.begin(); - vector::const_iterator it_end = children.end(); - while(it != it_end) { - nodes.push_back(it->getNode()); - ++it; - } - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Kind kind, Expr child1, - const std::vector& otherChildren) { - const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = - otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1; - PrettyCheckArgument( - mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, - "Only operator-style expressions are made with mkExpr(); " - "to make variables and constants, see mkVar(), mkBoundVar(), " - "and mkConst()."); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - - NodeManagerScope nms(d_nodeManager); - - vector nodes; - nodes.push_back(child1.getNode()); - - vector::const_iterator it = otherChildren.begin(); - vector::const_iterator it_end = otherChildren.end(); - while(it != it_end) { - nodes.push_back(it->getNode()); - ++it; - } - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Expr opExpr) { - const Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - PrettyCheckArgument( - opExpr.getKind() == kind::BUILTIN || - kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, - "This Expr constructor is for parameterized kinds only"); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Expr opExpr, Expr child1) { - const unsigned n = 1; - Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - PrettyCheckArgument( - (opExpr.getKind() == kind::BUILTIN || - kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, - "This Expr constructor is for parameterized kinds only"); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) { - const unsigned n = 2; - Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - PrettyCheckArgument( - (opExpr.getKind() == kind::BUILTIN || - kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, - "This Expr constructor is for parameterized kinds only"); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), - child1.getNode(), - child2.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) { - const unsigned n = 3; - Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - PrettyCheckArgument( - (opExpr.getKind() == kind::BUILTIN || - kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, - "This Expr constructor is for parameterized kinds only"); - PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), - child1.getNode(), - child2.getNode(), - child3.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, - Expr child4) { - const unsigned n = 4; - Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - PrettyCheckArgument( - (opExpr.getKind() == kind::BUILTIN || - kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, - "This Expr constructor is for parameterized kinds only"); - - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), - child1.getNode(), - child2.getNode(), - child3.getNode(), - child4.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, - Expr child4, Expr child5) { - const unsigned n = 5; - Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - PrettyCheckArgument( - (opExpr.getKind() == kind::BUILTIN || - kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, - "This Expr constructor is for parameterized kinds only"); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - NodeManagerScope nms(d_nodeManager); - try { - INC_STAT(kind); - return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), - child1.getNode(), - child2.getNode(), - child3.getNode(), - child4.getNode(), - child5.getNode())); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -Expr ExprManager::mkExpr(Expr opExpr, const std::vector& children) { - const unsigned n = children.size(); - Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - PrettyCheckArgument( - (opExpr.getKind() == kind::BUILTIN || - kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, - "This Expr constructor is for parameterized kinds only"); - PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); - - NodeManagerScope nms(d_nodeManager); - - vector nodes; - vector::const_iterator it = children.begin(); - vector::const_iterator it_end = children.end(); - while(it != it_end) { - nodes.push_back(it->getNode()); - ++it; - } - try { - INC_STAT(kind); - return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes)); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - -bool ExprManager::hasOperator(Kind k) { - return NodeManager::hasOperator(k); -} - -Expr ExprManager::operatorOf(Kind k) { - NodeManagerScope nms(d_nodeManager); - - return d_nodeManager->operatorOf(k).toExpr(); -} - -Kind ExprManager::operatorToKind(Expr e) { - NodeManagerScope nms(d_nodeManager); - - return d_nodeManager->operatorToKind( e.getNode() ); -} - -/** Make a function type from domain to range. */ -FunctionType ExprManager::mkFunctionType(Type domain, Type range) { - NodeManagerScope nms(d_nodeManager); - return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode)))); -} - -/** Make a function type with input types from argTypes. */ -FunctionType ExprManager::mkFunctionType(const std::vector& argTypes, Type range) { - NodeManagerScope nms(d_nodeManager); - Assert(argTypes.size() >= 1); - std::vector argTypeNodes; - for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) { - argTypeNodes.push_back(*argTypes[i].d_typeNode); - } - return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode)))); -} - -FunctionType ExprManager::mkFunctionType(const std::vector& sorts) { - NodeManagerScope nms(d_nodeManager); - Assert(sorts.size() >= 2); - std::vector sortNodes; - for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { - sortNodes.push_back(*sorts[i].d_typeNode); - } - return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes)))); -} - -FunctionType ExprManager::mkPredicateType(const std::vector& sorts) { - NodeManagerScope nms(d_nodeManager); - Assert(sorts.size() >= 1); - std::vector sortNodes; - for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { - sortNodes.push_back(*sorts[i].d_typeNode); - } - return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)))); -} - -SExprType ExprManager::mkSExprType(const std::vector& types) { - NodeManagerScope nms(d_nodeManager); - std::vector typeNodes; - for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { - typeNodes.push_back(*types[i].d_typeNode); - } - return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes)))); -} - -FloatingPointType ExprManager::mkFloatingPointType(unsigned exp, unsigned sig) const { - NodeManagerScope nms(d_nodeManager); - return FloatingPointType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFloatingPointType(exp,sig)))); -} - -BitVectorType ExprManager::mkBitVectorType(unsigned size) const { - NodeManagerScope nms(d_nodeManager); - return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)))); -} - -ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { - NodeManagerScope nms(d_nodeManager); - return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)))); -} - -SetType ExprManager::mkSetType(Type elementType) const { - NodeManagerScope nms(d_nodeManager); - return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode)))); -} - -SequenceType ExprManager::mkSequenceType(Type elementType) const -{ - NodeManagerScope nms(d_nodeManager); - return SequenceType(Type( - d_nodeManager, - new TypeNode(d_nodeManager->mkSequenceType(*elementType.d_typeNode)))); -} - -SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const { - NodeManagerScope nms(d_nodeManager); - return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, flags)))); -} - -SortConstructorType ExprManager::mkSortConstructor(const std::string& name, - size_t arity, - uint32_t flags) const -{ - NodeManagerScope nms(d_nodeManager); - return SortConstructorType( - Type(d_nodeManager, - new TypeNode(d_nodeManager->mkSortConstructor(name, arity, flags)))); -} - -/** - * Get the type for the given Expr and optionally do type checking. - * - * Initial type computation will be near-constant time if - * type checking is not requested. Results are memoized, so that - * subsequent calls to getType() without type checking will be - * constant time. - * - * Initial type checking is linear in the size of the expression. - * Again, the results are memoized, so that subsequent calls to - * getType(), with or without type checking, will be constant - * time. - * - * NOTE: A TypeCheckingException can be thrown even when type - * checking is not requested. getType() will always return a - * valid and correct type and, thus, an exception will be thrown - * when no valid or correct type can be computed (e.g., if the - * arguments to a bit-vector operation aren't bit-vectors). When - * type checking is not requested, getType() will do the minimum - * amount of checking required to return a valid result. - * - * @param e the Expr for which we want a type - * @param check whether we should check the type as we compute it - * (default: false) - */ -Type ExprManager::getType(Expr expr, bool check) -{ - NodeManagerScope nms(d_nodeManager); - Type t; - try { - t = Type(d_nodeManager, - new TypeNode(d_nodeManager->getType(expr.getNode(), check))); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } - return t; -} - -Expr ExprManager::mkVar(const std::string& name, Type type) -{ - NodeManagerScope nms(d_nodeManager); - Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode); - Debug("nm") << "set " << name << " on " << *n << std::endl; - INC_STAT_VAR(type, false); - return Expr(this, n); -} - -Expr ExprManager::mkVar(Type type) -{ - NodeManagerScope nms(d_nodeManager); - INC_STAT_VAR(type, false); - return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode)); -} - -Expr ExprManager::mkBoundVar(const std::string& name, Type type) -{ - NodeManagerScope nms(d_nodeManager); - Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode); - Debug("nm") << "set " << name << " on " << *n << std::endl; - INC_STAT_VAR(type, true); - return Expr(this, n); -} - -Expr ExprManager::mkBoundVar(Type type) -{ - NodeManagerScope nms(d_nodeManager); - INC_STAT_VAR(type, true); - return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode)); -} - -Expr ExprManager::mkNullaryOperator(Type type, Kind k){ - NodeManagerScope nms(d_nodeManager); - Node n = d_nodeManager->mkNullaryOperator(*type.d_typeNode, k); - return n.toExpr(); -} - -Expr ExprManager::mkAssociative(Kind kind, - const std::vector& children) { - PrettyCheckArgument( - kind::isAssociative(kind), kind, - "Illegal kind in mkAssociative: %s", - kind::kindToString(kind).c_str()); - - const unsigned int max = maxArity(kind); - unsigned int numChildren = children.size(); - - /* If the number of children is within bounds, then there's nothing to do. */ - if( numChildren <= max ) { - return mkExpr(kind,children); - } - NodeManagerScope nms(d_nodeManager); - const unsigned int min = minArity(kind); - - std::vector::const_iterator it = children.begin() ; - std::vector::const_iterator end = children.end() ; - - /* The new top-level children and the children of each sub node */ - std::vector newChildren; - std::vector subChildren; - - while( it != end && numChildren > max ) { - /* Grab the next max children and make a node for them. */ - for( std::vector::const_iterator next = it + max; - it != next; - ++it, --numChildren ) { - subChildren.push_back(it->getNode()); - } - Node subNode = d_nodeManager->mkNode(kind,subChildren); - newChildren.push_back(subNode.toExpr()); - - subChildren.clear(); - } - - // add the leftover children - if(numChildren > 0) { - for (; it != end; ++it) - { - newChildren.push_back(*it); - } - } - - /* It would be really weird if this happened (it would require - * min > 2, for one thing), but let's make sure. */ - AlwaysAssert(newChildren.size() >= min) - << "Too few new children in mkAssociative"; - - // recurse - return mkAssociative(kind, newChildren); -} - -Expr ExprManager::mkLeftAssociative(Kind kind, - const std::vector& children) -{ - NodeManagerScope nms(d_nodeManager); - Node n = children[0]; - for (unsigned i = 1, size = children.size(); i < size; i++) - { - n = d_nodeManager->mkNode(kind, n, children[i].getNode()); - } - return n.toExpr(); -} - -Expr ExprManager::mkRightAssociative(Kind kind, - const std::vector& children) -{ - NodeManagerScope nms(d_nodeManager); - Node n = children[children.size() - 1]; - for (unsigned i = children.size() - 1; i > 0;) - { - n = d_nodeManager->mkNode(kind, children[--i].getNode(), n); - } - return n.toExpr(); -} - -Expr ExprManager::mkChain(Kind kind, const std::vector& children) -{ - if (children.size() == 2) - { - // if this is the case exactly 1 pair will be generated so the - // AND is not required - return mkExpr(kind, children[0], children[1]); - } - std::vector cchildren; - for (size_t i = 0, nargsmo = children.size() - 1; i < nargsmo; i++) - { - cchildren.push_back(mkExpr(kind, children[i], children[i + 1])); - } - return mkExpr(kind::AND, cchildren); -} - -unsigned ExprManager::minArity(Kind kind) { - return metakind::getMinArityForKind(kind); -} - -unsigned ExprManager::maxArity(Kind kind) { - return metakind::getMaxArityForKind(kind); -} - -bool ExprManager::isNAryKind(Kind fun) -{ - return ExprManager::maxArity(fun) == expr::NodeValue::MAX_CHILDREN; -} - -NodeManager* ExprManager::getNodeManager() const { - return d_nodeManager; -} -Statistics ExprManager::getStatistics() const -{ - return Statistics(*d_nodeManager->getStatisticsRegistry()); -} - -SExpr ExprManager::getStatistic(const std::string& name) const -{ - return d_nodeManager->getStatisticsRegistry()->getStatistic(name); -} - -void ExprManager::safeFlushStatistics(int fd) const { - d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd); -} - -namespace expr { - -Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); - -TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) { - Debug("export") << "type: " << n << " " << n.getId() << std::endl; - if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) { - throw ExportUnsupportedException - ("export of types belonging to theory of DATATYPES kinds unsupported"); - } - if(n.getMetaKind() == kind::metakind::PARAMETERIZED && - n.getKind() != kind::SORT_TYPE) { - throw ExportUnsupportedException - ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); - } - if(n.getKind() == kind::TYPE_CONSTANT) { - return to->mkTypeConst(n.getConst()); - } else if(n.getKind() == kind::BITVECTOR_TYPE) { - return to->mkBitVectorType(n.getConst()); - } - else if (n.getKind() == kind::FLOATINGPOINT_TYPE) - { - return to->mkFloatingPointType(n.getConst()); - } - else if (n.getNumChildren() == 0) - { - std::stringstream msg; - msg << "export of type " << n << " not supported"; - throw ExportUnsupportedException(msg.str().c_str()); - } - Type from_t = from->toType(n); - Type& to_t = vmap.d_typeMap[from_t]; - if(! to_t.isNull()) { - Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl; - return *Type::getTypeNode(to_t); - } - NodeBuilder<> children(to, n.getKind()); - if(n.getKind() == kind::SORT_TYPE) { - Debug("export") << "type: operator: " << n.getOperator() << std::endl; - // make a new sort tag in target node manager - Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG); - children << sortTag; - } - for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { - Debug("export") << "type: child: " << *i << std::endl; - children << exportTypeInternal(*i, from, to, vmap); - } - TypeNode out = children.constructTypeNode();// FIXME thread safety - to_t = to->toType(out); - return out; -}/* exportTypeInternal() */ - -}/* CVC4::expr namespace */ - -Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) { - Assert(t.d_nodeManager != em->d_nodeManager) - << "Can't export a Type to the same ExprManager"; - NodeManagerScope ems(t.d_nodeManager); - return Type(em->d_nodeManager, - new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap))); -} - -${mkConst_implementations} - -}/* CVC4 namespace */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h deleted file mode 100644 index 37c3a7255..000000000 --- a/src/expr/expr_manager_template.h +++ /dev/null @@ -1,463 +0,0 @@ -/********************* */ -/*! \file expr_manager_template.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Public-facing expression manager interface - ** - ** Public-facing expression manager interface. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__EXPR_MANAGER_H -#define CVC4__EXPR_MANAGER_H - -#include - -#include "expr/expr.h" -#include "expr/kind.h" -#include "expr/type.h" -#include "util/statistics.h" - -${includes} - -namespace CVC4 { - -namespace api { -class Solver; -} - -class Expr; -class SmtEngine; -class NodeManager; -class Options; -class IntStat; -struct ExprManagerMapCollection; -class ResourceManager; - -class CVC4_PUBLIC ExprManager { - private: - friend api::Solver; - /** The internal node manager */ - NodeManager* d_nodeManager; - - /** Counts of expressions and variables created of a given kind */ - IntStat* d_exprStatisticsVars[LAST_TYPE + 1]; - IntStat* d_exprStatistics[kind::LAST_KIND]; - - /** - * Returns the internal node manager. This should only be used by - * internal users, i.e. the friend classes. - */ - NodeManager* getNodeManager() const; - - /** - * SmtEngine will use all the internals, so it will grab the - * NodeManager. - */ - friend class SmtEngine; - - /** ExprManagerScope reaches in to get the NodeManager */ - friend class ExprManagerScope; - - /** NodeManager reaches in to get the NodeManager */ - friend class NodeManager; - - // undefined, private copy constructor and assignment op (disallow copy) - ExprManager(const ExprManager&) = delete; - ExprManager& operator=(const ExprManager&) = delete; - /** Creates an expression manager. */ - ExprManager(); - public: - /** - * Destroys the expression manager. No will be deallocated at this point, so - * any expression references that used to be managed by this expression - * manager and are left-over are bad. - */ - ~ExprManager(); - - /** Get the type for booleans */ - BooleanType booleanType() const; - - /** Get the type for strings. */ - StringType stringType() const; - - /** Get the type for regular expressions. */ - RegExpType regExpType() const; - - /** Get the type for reals. */ - RealType realType() const; - - /** Get the type for integers */ - IntegerType integerType() const; - - /** Get the type for rounding modes */ - RoundingModeType roundingModeType() const; - - /** - * Make a unary expression of a given kind (NOT, BVNOT, ...). - * @param kind the kind of expression - * @param child1 kind the kind of expression - * @return the expression - */ - Expr mkExpr(Kind kind, Expr child1); - - /** - * Make a binary expression of a given kind (AND, PLUS, ...). - * @param kind the kind of expression - * @param child1 the first child of the new expression - * @param child2 the second child of the new expression - * @return the expression - */ - Expr mkExpr(Kind kind, Expr child1, Expr child2); - - /** - * Make a 3-ary expression of a given kind (AND, PLUS, ...). - * @param kind the kind of expression - * @param child1 the first child of the new expression - * @param child2 the second child of the new expression - * @param child3 the third child of the new expression - * @return the expression - */ - Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); - - /** - * Make a 4-ary expression of a given kind (AND, PLUS, ...). - * @param kind the kind of expression - * @param child1 the first child of the new expression - * @param child2 the second child of the new expression - * @param child3 the third child of the new expression - * @param child4 the fourth child of the new expression - * @return the expression - */ - Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); - - /** - * Make a 5-ary expression of a given kind (AND, PLUS, ...). - * @param kind the kind of expression - * @param child1 the first child of the new expression - * @param child2 the second child of the new expression - * @param child3 the third child of the new expression - * @param child4 the fourth child of the new expression - * @param child5 the fifth child of the new expression - * @return the expression - */ - Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, - Expr child5); - - /** - * Make an n-ary expression of given kind given a vector of its - * children - * - * @param kind the kind of expression to build - * @param children the subexpressions - * @return the n-ary expression - */ - Expr mkExpr(Kind kind, const std::vector& children); - - /** - * Make an n-ary expression of given kind given a first arg and - * a vector of its remaining children (this can be useful where the - * kind is parameterized operator, so the first arg is really an - * arg to the kind to construct an operator) - * - * @param kind the kind of expression to build - * @param child1 the first subexpression - * @param otherChildren the remaining subexpressions - * @return the n-ary expression - */ - Expr mkExpr(Kind kind, Expr child1, const std::vector& otherChildren); - - /** - * Make a nullary parameterized expression with the given operator. - * - * @param opExpr the operator expression - * @return the nullary expression - */ - Expr mkExpr(Expr opExpr); - - /** - * Make a unary parameterized expression with the given operator. - * - * @param opExpr the operator expression - * @param child1 the subexpression - * @return the unary expression - */ - Expr mkExpr(Expr opExpr, Expr child1); - - /** - * Make a binary parameterized expression with the given operator. - * - * @param opExpr the operator expression - * @param child1 the first subexpression - * @param child2 the second subexpression - * @return the binary expression - */ - Expr mkExpr(Expr opExpr, Expr child1, Expr child2); - - /** - * Make a ternary parameterized expression with the given operator. - * - * @param opExpr the operator expression - * @param child1 the first subexpression - * @param child2 the second subexpression - * @param child3 the third subexpression - * @return the ternary expression - */ - Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3); - - /** - * Make a quaternary parameterized expression with the given operator. - * - * @param opExpr the operator expression - * @param child1 the first subexpression - * @param child2 the second subexpression - * @param child3 the third subexpression - * @param child4 the fourth subexpression - * @return the quaternary expression - */ - Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4); - - /** - * Make a quinary parameterized expression with the given operator. - * - * @param opExpr the operator expression - * @param child1 the first subexpression - * @param child2 the second subexpression - * @param child3 the third subexpression - * @param child4 the fourth subexpression - * @param child5 the fifth subexpression - * @return the quinary expression - */ - Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4, - Expr child5); - - /** - * Make an n-ary expression of given operator to apply and a vector - * of its children - * - * @param opExpr the operator expression - * @param children the subexpressions - * @return the n-ary expression - */ - Expr mkExpr(Expr opExpr, const std::vector& children); - - /** Create a constant of type T */ - template - Expr mkConst(const T&); - - /** - * Create an Expr by applying an associative operator to the children. - * If children.size() is greater than the max arity for - * kind, then the expression will be broken up into - * suitably-sized chunks, taking advantage of the associativity of - * kind. For example, if kind FOO has max arity - * 2, then calling mkAssociative(FOO,a,b,c) will return - * (FOO (FOO a b) c) or (FOO a (FOO b c)). - * The order of the arguments will be preserved in a left-to-right - * traversal of the resulting tree. - */ - Expr mkAssociative(Kind kind, const std::vector& children); - - /** - * Create an Expr by applying an binary left-associative operator to the - * children. For example, mkLeftAssociative( f, { a, b, c } ) returns - * f( f( a, b ), c ). - */ - Expr mkLeftAssociative(Kind kind, const std::vector& children); - /** - * Create an Expr by applying an binary right-associative operator to the - * children. For example, mkRightAssociative( f, { a, b, c } ) returns - * f( a, f( b, c ) ). - */ - Expr mkRightAssociative(Kind kind, const std::vector& children); - - /** make chain - * - * Given a kind k and arguments t_1, ..., t_n, this returns the - * conjunction of: - * (k t_1 t_2) .... (k t_{n-1} t_n) - * It is expected that k is a kind denoting a predicate, and args is a list - * of terms of size >= 2 such that the terms above are well-typed. - */ - Expr mkChain(Kind kind, const std::vector& children); - - /** - * Determine whether Exprs of a particular Kind have operators. - * @returns true if Exprs of Kind k have operators. - */ - static bool hasOperator(Kind k); - - /** - * Get the (singleton) operator of an OPERATOR-kinded kind. The - * returned Expr e will have kind BUILTIN, and calling - * e.getConst() will yield k. - */ - Expr operatorOf(Kind k); - - /** Get a Kind from an operator expression */ - Kind operatorToKind(Expr e); - - /** Make a function type from domain to range. */ - FunctionType mkFunctionType(Type domain, Type range); - - /** - * Make a function type with input types from argTypes. - * argTypes must have at least one element. - */ - FunctionType mkFunctionType(const std::vector& argTypes, Type range); - - /** - * Make a function type with input types from - * sorts[0..sorts.size()-2] and result type - * sorts[sorts.size()-1]. sorts must have - * at least 2 elements. - */ - FunctionType mkFunctionType(const std::vector& sorts); - - /** - * Make a predicate type with input types from - * sorts. The result with be a function type with range - * BOOLEAN. sorts must have at least one - * element. - */ - FunctionType mkPredicateType(const std::vector& sorts); - - /** - * Make a symbolic expressiontype with types from - * types[0..types.size()-1]. types may - * have any number of elements. - */ - SExprType mkSExprType(const std::vector& types); - - /** Make a type representing a floating-point type with the given parameters. */ - FloatingPointType mkFloatingPointType(unsigned exp, unsigned sig) const; - - /** Make a type representing a bit-vector of the given size. */ - BitVectorType mkBitVectorType(unsigned size) const; - - /** Make the type of arrays with the given parameterization. */ - ArrayType mkArrayType(Type indexType, Type constituentType) const; - - /** Make the type of set with the given parameterization. */ - SetType mkSetType(Type elementType) const; - - /** Make the type of sequence with the given parameterization. */ - SequenceType mkSequenceType(Type elementType) const; - - /** Make a new sort with the given name. */ - SortType mkSort(const std::string& name, uint32_t flags) const; - - /** Make a sort constructor from a name and arity. */ - SortConstructorType mkSortConstructor(const std::string& name, - size_t arity, - uint32_t flags) const; - - /** - * Get the type of an expression. - * - * Throws a TypeCheckingException on failures or if a Type cannot be - * computed. - */ - Type getType(Expr e, bool check = false); - - /** - * Create a new, fresh variable. This variable is guaranteed to be - * distinct from every variable thus far in the ExprManager, even - * if it shares a name with another; this is to support any kind of - * scoping policy on top of ExprManager. The SymbolTable class - * can be used to store and lookup symbols by name, if desired. - * - * @param name a name to associate to the fresh new variable - * @param type the type for the new variable - */ - Expr mkVar(const std::string& name, Type type); - - /** - * Create a (nameless) new, fresh variable. This variable is guaranteed - * to be distinct from every variable thus far in the ExprManager. - * - * @param type the type for the new variable - */ - Expr mkVar(Type type); - - /** - * Create a new, fresh variable for use in a binder expression - * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS). It is - * an error for this bound variable to exist outside of a binder, - * and it should also only be used in a single binder expression. - * That is, two distinct FORALL expressions should use entirely - * disjoint sets of bound variables (however, a single FORALL - * expression can be used in multiple places in a formula without - * a problem). This newly-created bound variable is guaranteed to - * be distinct from every variable thus far in the ExprManager, even - * if it shares a name with another; this is to support any kind of - * scoping policy on top of ExprManager. The SymbolTable class - * can be used to store and lookup symbols by name, if desired. - * - * @param name a name to associate to the fresh new bound variable - * @param type the type for the new bound variable - */ - Expr mkBoundVar(const std::string& name, Type type); - - /** - * Create a (nameless) new, fresh variable for use in a binder - * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS). - * It is an error for this bound variable to exist outside of a - * binder, and it should also only be used in a single binder - * expression. That is, two distinct FORALL expressions should use - * entirely disjoint sets of bound variables (however, a single FORALL - * expression can be used in multiple places in a formula without - * a problem). This newly-created bound variable is guaranteed to - * be distinct from every variable thus far in the ExprManager. - * - * @param type the type for the new bound variable - */ - Expr mkBoundVar(Type type); - - /** - * Create unique variable of type - */ - Expr mkNullaryOperator( Type type, Kind k); - - /** Get a reference to the statistics registry for this ExprManager */ - Statistics getStatistics() const; - - /** Get a reference to the statistics registry for this ExprManager */ - SExpr getStatistic(const std::string& name) const; - - /** - * Flushes statistics for this ExprManager to a file descriptor. Safe to use - * in a signal handler. - */ - void safeFlushStatistics(int fd) const; - - /** Export an expr to a different ExprManager */ - //static Expr exportExpr(const Expr& e, ExprManager* em); - /** Export a type to a different ExprManager */ - static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap); - - /** Returns the minimum arity of the given kind. */ - static unsigned minArity(Kind kind); - - /** Returns the maximum arity of the given kind. */ - static unsigned maxArity(Kind kind); - - /** Whether a kind is n-ary. The test is based on n-ary kinds having their - * maximal arity as the maximal possible number of children of a node. - **/ - static bool isNAryKind(Kind fun); -};/* class ExprManager */ - -${mkConst_instantiations} - -}/* CVC4 namespace */ - -#endif /* CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp deleted file mode 100644 index 745588a9a..000000000 --- a/src/expr/expr_template.cpp +++ /dev/null @@ -1,703 +0,0 @@ -/********************* */ -/*! \file expr_template.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Public-facing expression interface, implementation. - ** - ** Public-facing expression interface, implementation. - **/ -#include "expr/expr.h" - -#include -#include -#include -#include - -#include "base/check.h" -#include "expr/expr_manager_scope.h" -#include "expr/node.h" -#include "expr/node_algorithm.h" -#include "expr/node_manager_attributes.h" -#include "expr/variable_type_map.h" - -${includes} - -using namespace CVC4::kind; -using namespace std; - -namespace CVC4 { - -class ExprManager; - -std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) { - return out << e.getMessage() << ": " << e.getExpression(); -} - -std::ostream& operator<<(std::ostream& out, const Expr& e) { - if(e.isNull()) { - return out << "null"; - } else { - ExprManagerScope ems(*e.getExprManager()); - return out << e.getNode(); - } -} - -std::ostream& operator<<(std::ostream& out, const std::vector& container) -{ - container_to_stream(out, container); - return out; -} - -std::ostream& operator<<(std::ostream& out, const std::set& container) -{ - container_to_stream(out, container); - return out; -} - -std::ostream& operator<<( - std::ostream& out, - const std::unordered_set& container) -{ - container_to_stream(out, container); - return out; -} - -template -std::ostream& operator<<(std::ostream& out, const std::map& container) -{ - container_to_stream(out, container); - return out; -} - -template -std::ostream& operator<<( - std::ostream& out, - const std::unordered_map& container) -{ - container_to_stream(out, container); - return out; -} - -TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) - : Exception(t.d_msg), d_expr(new Expr(t.getExpression())) -{ -} - -TypeCheckingException::TypeCheckingException(const Expr& expr, - std::string message) - : Exception(message), d_expr(new Expr(expr)) -{ -} - -TypeCheckingException::TypeCheckingException( - ExprManager* em, const TypeCheckingExceptionPrivate* exc) - : Exception(exc->getMessage()), - d_expr(new Expr(em, new Node(exc->getNode()))) -{ -} - -TypeCheckingException::~TypeCheckingException() { delete d_expr; } - -void TypeCheckingException::toStream(std::ostream& os) const -{ - os << "Error during type checking: " << d_msg << endl - << "The ill-typed expression: " << *d_expr; -} - -Expr TypeCheckingException::getExpression() const { return *d_expr; } - -Expr::Expr() : - d_node(new Node), - d_exprManager(NULL) { - // We do not need to wrap this in an ExprManagerScope as `new Node` is backed - // by NodeValue::null which is a static outside of a NodeManager. -} - -Expr::Expr(ExprManager* em, Node* node) : - d_node(node), - d_exprManager(em) { - // We do not need to wrap this in an ExprManagerScope as this only initializes - // pointers -} - -Expr::Expr(const Expr& e) : - d_node(NULL), - d_exprManager(e.d_exprManager) { - ExprManagerScope ems(*this); - d_node = new Node(*e.d_node); -} - -Expr::~Expr() { - ExprManagerScope ems(*this); - delete d_node; -} - -ExprManager* Expr::getExprManager() const { - return d_exprManager; -} - -namespace expr { - -static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& vmap); - -class ExportPrivate { -private: - typedef std::unordered_map , NodeTemplate, TNodeHashFunction> ExportCache; - ExprManager* d_from; - ExprManager* d_to; - ExprManagerMapCollection& d_vmap; - uint32_t d_flags; - ExportCache d_exportCache; - - public: - ExportPrivate(ExprManager* from, - ExprManager* to, - ExprManagerMapCollection& vmap, - uint32_t flags) - : d_from(from), d_to(to), d_vmap(vmap), d_flags(flags) - { - } - Node exportInternal(TNode n) { - - if(n.isNull()) return Node::null(); - if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) { - throw ExportUnsupportedException - ("export of node belonging to theory of DATATYPES kinds unsupported"); - } - - if(n.getMetaKind() == metakind::CONSTANT) { - if(n.getKind() == kind::EMPTYSET) { - Type type = d_from->exportType( - n.getConst< ::CVC4::EmptySet>().getType().toType(), d_to, d_vmap); - return d_to->mkConst(::CVC4::EmptySet(TypeNode::fromType(type))); - } - return exportConstant(n, NodeManager::fromExprManager(d_to), d_vmap); - } else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){ - Expr from_e(d_from, new Node(n)); - Type type = d_from->exportType(from_e.getType(), d_to, d_vmap); - return d_to->mkNullaryOperator(type, n.getKind()); // FIXME thread safety - } else if(n.getMetaKind() == metakind::VARIABLE) { - Expr from_e(d_from, new Node(n)); - Expr& to_e = d_vmap.d_typeMap[from_e]; - if(! to_e.isNull()) { - Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl; - return to_e.getNode(); - } else { - // construct new variable in other manager: - // to_e is a ref, so this inserts from_e -> to_e - std::string name; - Type type = d_from->exportType(from_e.getType(), d_to, d_vmap); - if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) { - if (n.getKind() == kind::BOUND_VARIABLE) - { - // bound vars are only available at the Node level (not the Expr - // level) - TypeNode typeNode = TypeNode::fromType(type); - NodeManager* to_nm = NodeManager::fromExprManager(d_to); - Node nn = to_nm->mkBoundVar(name, typeNode); // FIXME thread safety - - // Make sure that the correct `NodeManager` is in scope while - // converting the node to an expression. - NodeManagerScope to_nms(to_nm); - to_e = nn.toExpr(); - } else if(n.getKind() == kind::VARIABLE) { - // Temporarily set the node manager to nullptr; this gets around - // a check that mkVar isn't called internally - NodeManagerScope nullScope(nullptr); - to_e = d_to->mkVar(name, - type); // FIXME thread safety - } else if(n.getKind() == kind::SKOLEM) { - // skolems are only available at the Node level (not the Expr level) - TypeNode typeNode = TypeNode::fromType(type); - NodeManager* to_nm = NodeManager::fromExprManager(d_to); - Node nn = - to_nm->mkSkolem(name, - typeNode, - "is a skolem variable imported from another " - "ExprManager"); // FIXME thread safety - - // Make sure that the correct `NodeManager` is in scope while - // converting the node to an expression. - NodeManagerScope to_nms(to_nm); - to_e = nn.toExpr(); - } else { - Unhandled(); - } - - Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl; - } else { - if (n.getKind() == kind::BOUND_VARIABLE) - { - // bound vars are only available at the Node level (not the Expr - // level) - TypeNode typeNode = TypeNode::fromType(type); - NodeManager* to_nm = NodeManager::fromExprManager(d_to); - Node nn = to_nm->mkBoundVar(typeNode); // FIXME thread safety - - // Make sure that the correct `NodeManager` is in scope while - // converting the node to an expression. - NodeManagerScope to_nms(to_nm); - to_e = nn.toExpr(); - } - else - { - // Temporarily set the node manager to nullptr; this gets around - // a check that mkVar isn't called internally - NodeManagerScope nullScope(nullptr); - to_e = d_to->mkVar(type); // FIXME thread safety - } - Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl; - } - uint64_t to_int = (uint64_t)(to_e.getNode().d_nv); - uint64_t from_int = (uint64_t)(from_e.getNode().d_nv); - d_vmap.d_from[to_int] = from_int; - d_vmap.d_to[from_int] = to_int; - d_vmap.d_typeMap[to_e] = from_e; // insert other direction too - - // Make sure that the expressions are associated with the correct - // `ExprManager`s. - Assert(from_e.getExprManager() == d_from); - Assert(to_e.getExprManager() == d_to); - return Node::fromExpr(to_e); - } - } else { - if (d_exportCache.find(n) != d_exportCache.end()) - { - return d_exportCache[n]; - } - - std::vector children; - Debug("export") << "n: " << n << std::endl; - if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { - Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl; - children.reserve(n.getNumChildren() + 1); - children.push_back(exportInternal(n.getOperator())); - } else { - children.reserve(n.getNumChildren()); - } - for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { - Debug("export") << "+ child: " << *i << std::endl; - children.push_back(exportInternal(*i)); - } - if(Debug.isOn("export")) { - Debug("export") << "children for export from " << n << std::endl; - - // `n` belongs to the `from` ExprManager, so begin ExprManagerScope - // after printing `n` - ExprManagerScope ems(*d_to); - for(std::vector::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) { - Debug("export") << " child: " << *i << std::endl; - } - } - - // FIXME thread safety - Node ret = - NodeManager::fromExprManager(d_to)->mkNode(n.getKind(), children); - - d_exportCache[n] = ret; - return ret; - } - }/* exportInternal() */ - -}; - -}/* CVC4::expr namespace */ - -Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, - uint32_t flags /* = 0 */) const { - Assert(d_exprManager != exprManager) - << "No sense in cloning an Expr in the same ExprManager"; - ExprManagerScope ems(*this); - return Expr(exprManager, new Node(expr::ExportPrivate(d_exprManager, exprManager, variableMap, flags).exportInternal(*d_node))); -} - -Expr& Expr::operator=(const Expr& e) { - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!"; - - if(this != &e) { - if(d_exprManager == e.d_exprManager) { - ExprManagerScope ems(*this); - *d_node = *e.d_node; - } else { - // This happens more than you think---every time you set to or - // from the null Expr. It's tricky because each node manager - // must be in play at the right time. - - ExprManagerScope ems1(*this); - *d_node = Node::null(); - - ExprManagerScope ems2(e); - *d_node = *e.d_node; - - d_exprManager = e.d_exprManager; - } - } - return *this; -} - -bool Expr::operator==(const Expr& e) const { - if(d_exprManager != e.d_exprManager) { - return false; - } - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!"; - return *d_node == *e.d_node; -} - -bool Expr::operator!=(const Expr& e) const { - return !(*this == e); -} - -bool Expr::operator<(const Expr& e) const { - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!"; - if(isNull() && !e.isNull()) { - return true; - } - ExprManagerScope ems(*this); - return *d_node < *e.d_node; -} - -bool Expr::operator>(const Expr& e) const { - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!"; - if(isNull() && !e.isNull()) { - return true; - } - ExprManagerScope ems(*this); - return *d_node > *e.d_node; -} - -uint64_t Expr::getId() const -{ - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return d_node->getId(); -} - -Kind Expr::getKind() const { - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return d_node->getKind(); -} - -size_t Expr::getNumChildren() const { - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return d_node->getNumChildren(); -} - -Expr Expr::operator[](unsigned i) const { - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - Assert(i >= 0 && i < d_node->getNumChildren()) << "Child index out of bounds"; - return Expr(d_exprManager, new Node((*d_node)[i])); -} - -bool Expr::hasOperator() const { - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return d_node->hasOperator(); -} - -Expr Expr::getOperator() const { - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - PrettyCheckArgument(d_node->hasOperator(), *this, - "Expr::getOperator() called on an Expr with no operator"); - return Expr(d_exprManager, new Node(d_node->getOperator())); -} - -bool Expr::isParameterized() const -{ - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return d_node->getMetaKind() == kind::metakind::PARAMETERIZED; -} - -Type Expr::getType(bool check) const -{ - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - PrettyCheckArgument(!d_node->isNull(), this, - "Can't get type of null expression!"); - return d_exprManager->getType(*this, check); -} - -Expr Expr::substitute(Expr e, Expr replacement) const { - ExprManagerScope ems(*this); - return Expr(d_exprManager, new Node(d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node)))); -} - -template -class NodeIteratorAdaptor : public std::iterator { - Iterator d_iterator; -public: - NodeIteratorAdaptor(Iterator i) : d_iterator(i) { - } - NodeIteratorAdaptor& operator++() { ++d_iterator; return *this; } - NodeIteratorAdaptor operator++(int) { NodeIteratorAdaptor i(d_iterator); ++d_iterator; return i; } - bool operator==(NodeIteratorAdaptor i) { return d_iterator == i.d_iterator; } - bool operator!=(NodeIteratorAdaptor i) { return !(*this == i); } - Node operator*() { return Node::fromExpr(*d_iterator); } -};/* class NodeIteratorAdaptor */ - -template -static inline NodeIteratorAdaptor mkNodeIteratorAdaptor(Iterator i) { - return NodeIteratorAdaptor(i); -} - -Expr Expr::substitute(const std::vector exes, - const std::vector& replacements) const { - ExprManagerScope ems(*this); - return Expr(d_exprManager, - new Node(d_node->substitute(mkNodeIteratorAdaptor(exes.begin()), - mkNodeIteratorAdaptor(exes.end()), - mkNodeIteratorAdaptor(replacements.begin()), - mkNodeIteratorAdaptor(replacements.end())))); -} - -template -class NodePairIteratorAdaptor : public std::iterator > { - Iterator d_iterator; -public: - NodePairIteratorAdaptor(Iterator i) : d_iterator(i) { - } - NodePairIteratorAdaptor& operator++() { ++d_iterator; return *this; } - NodePairIteratorAdaptor operator++(int) { NodePairIteratorAdaptor i(d_iterator); ++d_iterator; return i; } - bool operator==(NodePairIteratorAdaptor i) { return d_iterator == i.d_iterator; } - bool operator!=(NodePairIteratorAdaptor i) { return !(*this == i); } - pair operator*() { return make_pair(Node::fromExpr((*d_iterator).first), Node::fromExpr((*d_iterator).second)); } -};/* class NodePairIteratorAdaptor */ - -template -static inline NodePairIteratorAdaptor mkNodePairIteratorAdaptor(Iterator i) { - return NodePairIteratorAdaptor(i); -} - -Expr Expr::substitute(const std::unordered_map map) const { - ExprManagerScope ems(*this); - return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end())))); -} - -Expr::const_iterator::const_iterator() - : d_exprManager(nullptr), d_iterator(nullptr) {} - -Expr::const_iterator::const_iterator(ExprManager* em, void* v) - : d_exprManager(em), d_iterator(v) {} - -Expr::const_iterator::const_iterator(const const_iterator& it) - : d_exprManager(nullptr), d_iterator(nullptr) { - if (it.d_iterator != nullptr) { - d_exprManager = it.d_exprManager; - ExprManagerScope ems(*d_exprManager); - d_iterator = - new Node::iterator(*reinterpret_cast(it.d_iterator)); - } -} - -Expr::const_iterator& Expr::const_iterator::operator=(const const_iterator& it) { - if(d_iterator != NULL) { - ExprManagerScope ems(*d_exprManager); - delete reinterpret_cast(d_iterator); - } - d_exprManager = it.d_exprManager; - ExprManagerScope ems(*d_exprManager); - d_iterator = new Node::iterator(*reinterpret_cast(it.d_iterator)); - return *this; -} -Expr::const_iterator::~const_iterator() { - if(d_iterator != NULL) { - ExprManagerScope ems(*d_exprManager); - delete reinterpret_cast(d_iterator); - } -} -bool Expr::const_iterator::operator==(const const_iterator& it) const { - if(d_iterator == NULL || it.d_iterator == NULL) { - return false; - } - return *reinterpret_cast(d_iterator) == - *reinterpret_cast(it.d_iterator); -} -Expr::const_iterator& Expr::const_iterator::operator++() { - Assert(d_iterator != NULL); - ExprManagerScope ems(*d_exprManager); - ++*reinterpret_cast(d_iterator); - return *this; -} -Expr::const_iterator Expr::const_iterator::operator++(int) { - Assert(d_iterator != NULL); - ExprManagerScope ems(*d_exprManager); - const_iterator it = *this; - ++*reinterpret_cast(d_iterator); - return it; -} -Expr Expr::const_iterator::operator*() const { - Assert(d_iterator != NULL); - ExprManagerScope ems(*d_exprManager); - return (**reinterpret_cast(d_iterator)).toExpr(); -} - -Expr::const_iterator Expr::begin() const { - ExprManagerScope ems(*d_exprManager); - return Expr::const_iterator(d_exprManager, new Node::iterator(d_node->begin())); -} - -Expr::const_iterator Expr::end() const { - ExprManagerScope ems(*d_exprManager); - return Expr::const_iterator(d_exprManager, new Node::iterator(d_node->end())); -} - -std::string Expr::toString() const { - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return d_node->toString(); -} - -bool Expr::isNull() const { - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return d_node->isNull(); -} - -bool Expr::isVariable() const { - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return d_node->getMetaKind() == kind::metakind::VARIABLE; -} - -bool Expr::isConst() const { - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return d_node->isConst(); -} - -bool Expr::hasFreeVariable() const -{ - ExprManagerScope ems(*this); - Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; - return expr::hasFreeVar(*d_node); -} - -void Expr::toStream(std::ostream& out, - int depth, - size_t dag, - OutputLanguage language) const -{ - ExprManagerScope ems(*this); - d_node->toStream(out, depth, dag, language); -} - -Node Expr::getNode() const { return *d_node; } -TNode Expr::getTNode() const { return *d_node; } -Expr Expr::notExpr() const { - Assert(d_exprManager != NULL) - << "Don't have an expression manager for this expression!"; - return d_exprManager->mkExpr(NOT, *this); -} - -Expr Expr::andExpr(const Expr& e) const { - Assert(d_exprManager != NULL) - << "Don't have an expression manager for this expression!"; - PrettyCheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); - return d_exprManager->mkExpr(AND, *this, e); -} - -Expr Expr::orExpr(const Expr& e) const { - Assert(d_exprManager != NULL) - << "Don't have an expression manager for this expression!"; - PrettyCheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); - return d_exprManager->mkExpr(OR, *this, e); -} - -Expr Expr::xorExpr(const Expr& e) const { - Assert(d_exprManager != NULL) - << "Don't have an expression manager for this expression!"; - PrettyCheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); - return d_exprManager->mkExpr(XOR, *this, e); -} - -Expr Expr::eqExpr(const Expr& e) const -{ - Assert(d_exprManager != NULL) - << "Don't have an expression manager for this expression!"; - PrettyCheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); - return d_exprManager->mkExpr(EQUAL, *this, e); -} - -Expr Expr::impExpr(const Expr& e) const { - Assert(d_exprManager != NULL) - << "Don't have an expression manager for this expression!"; - PrettyCheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); - return d_exprManager->mkExpr(IMPLIES, *this, e); -} - -Expr Expr::iteExpr(const Expr& then_e, - const Expr& else_e) const { - Assert(d_exprManager != NULL) - << "Don't have an expression manager for this expression!"; - PrettyCheckArgument(d_exprManager == then_e.d_exprManager, then_e, - "Different expression managers!"); - PrettyCheckArgument(d_exprManager == else_e.d_exprManager, else_e, - "Different expression managers!"); - return d_exprManager->mkExpr(ITE, *this, then_e, else_e); -} - -void Expr::printAst(std::ostream & o, int indent) const { - ExprManagerScope ems(*this); - getNode().printAst(o, indent); -} - -void Expr::debugPrint() { -#ifndef CVC4_MUZZLE - printAst(Warning()); - Warning().flush(); -#endif /* ! CVC4_MUZZLE */ -} - -${getConst_implementations} - -namespace expr { - -static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& vmap) { - Assert(n.isConst()); - Debug("export") << "constant: " << n << std::endl; - - if(n.getKind() == kind::STORE_ALL) { - // Special export for ArrayStoreAll. - // - // Ultimately we'll need special cases also for RecordUpdate, - // TupleUpdate, AscriptionType, and other constant-metakinded - // expressions that embed types. For now datatypes aren't supported - // for export so those don't matter. - ExprManager* toEm = to->toExprManager(); - const ArrayStoreAll& asa = n.getConst(); - return to->mkConst(ArrayStoreAll( - TypeNode::fromType(asa.getType().toType().exportTo(toEm, vmap)), - Node::fromExpr(asa.getValue().toExpr().exportTo(toEm, vmap)))); - } - - switch(n.getKind()) { -${exportConstant_cases} - -default: Unhandled() << n.getKind(); - } - -}/* exportConstant() */ - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h deleted file mode 100644 index 2676c12b0..000000000 --- a/src/expr/expr_template.h +++ /dev/null @@ -1,622 +0,0 @@ -/********************* */ -/*! \file expr_template.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Public-facing expression interface. - ** - ** Public-facing expression interface. - **/ - -#include "cvc4_public.h" - -// putting the constant-payload #includes up here allows circularity -// (some of them may require a completely-defined Expr type). This -// way, those #includes can forward-declare some stuff to get Expr's -// getConst<> template instantiations correct, and then #include -// "expr.h" safely, then go on to completely declare their own stuff. -${includes} - -#ifndef CVC4__EXPR_H -#define CVC4__EXPR_H - -#include -#include -#include -#include -#include -#include -#include - -#include "base/exception.h" -#include "options/language.h" -#include "util/hash.h" - -namespace CVC4 { - -// The internal expression representation -template -class NodeTemplate; - -class NodeManager; - -class Expr; -class ExprManager; -class SmtEngine; -class Type; -class TypeCheckingException; -class TypeCheckingExceptionPrivate; - -namespace api { -class Solver; -} - -namespace prop { - class TheoryProxy; -}/* CVC4::prop namespace */ - -struct ExprManagerMapCollection; - -struct ExprHashFunction; - -namespace smt { - class SmtEnginePrivate; -}/* CVC4::smt namespace */ - -namespace expr { - class ExportPrivate; -}/* CVC4::expr namespace */ - -/** - * Exception thrown in the case of type-checking errors. - */ -class CVC4_PUBLIC TypeCheckingException : public Exception { - private: - friend class SmtEngine; - friend class smt::SmtEnginePrivate; - - /** The expression responsible for the error */ - Expr* d_expr; - - protected: - TypeCheckingException() : Exception() {} - TypeCheckingException(ExprManager* em, - const TypeCheckingExceptionPrivate* exc); - - public: - TypeCheckingException(const Expr& expr, std::string message); - - /** Copy constructor */ - TypeCheckingException(const TypeCheckingException& t); - - /** Destructor */ - ~TypeCheckingException() override; - - /** - * Get the Expr that caused the type-checking to fail. - * - * @return the expr - */ - Expr getExpression() const; - - /** - * Returns the message corresponding to the type-checking failure. - * We prefer toStream() to toString() because that keeps the expr-depth - * and expr-language settings present in the stream. - */ - void toStream(std::ostream& out) const override; - - friend class ExprManager; -};/* class TypeCheckingException */ - -/** - * Exception thrown in case of failure to export - */ -class CVC4_PUBLIC ExportUnsupportedException : public Exception { - public: - ExportUnsupportedException() : Exception("export unsupported") {} - ExportUnsupportedException(const char* msg) : Exception(msg) {} -};/* class DatatypeExportUnsupportedException */ - -std::ostream& operator<<(std::ostream& out, - const TypeCheckingException& e) CVC4_PUBLIC; - -/** - * Output operator for expressions - * @param out the stream to output to - * @param e the expression to output - * @return the stream - */ -std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC; - -/** - * Serialize a vector of expressions to given stream. - * - * @param out the output stream to use - * @param container the vector of expressions to output to the stream - * @return the stream - */ -std::ostream& operator<<(std::ostream& out, - const std::vector& container) CVC4_PUBLIC; - -/** - * Serialize a set of expressions to the given stream. - * - * @param out the output stream to use - * @param container the set of expressions to output to the stream - * @return the stream - */ -std::ostream& operator<<(std::ostream& out, - const std::set& container) CVC4_PUBLIC; - -/** - * Serialize an unordered_set of expressions to the given stream. - * - * @param out the output stream to use - * @param container the unordered_set of expressions to output to the stream - * @return the stream - */ -std::ostream& operator<<( - std::ostream& out, - const std::unordered_set& container) CVC4_PUBLIC; - -/** - * Serialize a map of expressions to the given stream. - * - * @param out the output stream to use - * @param container the map of expressions to output to the stream - * @return the stream - */ -template -std::ostream& operator<<(std::ostream& out, - const std::map& container) CVC4_PUBLIC; - -/** - * Serialize an unordered_map of expressions to the given stream. - * - * @param out the output stream to use - * @param container the unordered_map of expressions to output to the stream - * @return the stream - */ -template -std::ostream& operator<<( - std::ostream& out, - const std::unordered_map& container) CVC4_PUBLIC; - -// for hash_maps, hash_sets.. -struct ExprHashFunction { - size_t operator()(CVC4::Expr e) const; -};/* struct ExprHashFunction */ - -/** - * Class encapsulating CVC4 expressions and methods for constructing new - * expressions. - */ -class CVC4_PUBLIC Expr { - friend class ExprManager; - friend class NodeManager; - friend class SmtEngine; - friend class TypeCheckingException; - friend class api::Solver; - friend class expr::ExportPrivate; - friend class prop::TheoryProxy; - friend class smt::SmtEnginePrivate; - friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e); - - /** The internal expression representation */ - NodeTemplate* d_node; - - /** The responsible expression manager */ - ExprManager* d_exprManager; - - /** - * Constructor for internal purposes. - * - * @param em the expression manager that handles this expression - * @param node the actual expression node pointer - */ - Expr(ExprManager* em, NodeTemplate* node); - -public: - - /** Default constructor, makes a null expression. */ - Expr(); - - /** - * Copy constructor, makes a copy of a given expression - * - * @param e the expression to copy - */ - Expr(const Expr& e); - - /** Destructor */ - ~Expr(); - - /** - * Assignment operator, makes a copy of the given expression. If the - * expression managers of the two expressions differ, the expression of - * the given expression will be used. - * - * @param e the expression to assign - * @return the reference to this expression after assignment - */ - Expr& operator=(const Expr& e); - - /** - * Syntactic comparison operator. Returns true if expressions belong to the - * same expression manager and are syntactically identical. - * - * @param e the expression to compare to - * @return true if expressions are syntactically the same, false otherwise - */ - bool operator==(const Expr& e) const; - - /** - * Syntactic disequality operator. - * - * @param e the expression to compare to - * @return true if expressions differ syntactically, false otherwise - */ - bool operator!=(const Expr& e) const; - - /** - * Order comparison operator. The only invariant on the order of expressions - * is that the expressions that were created sooner will be smaller in the - * ordering than all the expressions created later. Null expression is the - * smallest element of the ordering. The behavior of the operator is - * undefined if the expressions come from two different expression managers. - * - * @param e the expression to compare to - * @return true if this expression is smaller than the given one - */ - bool operator<(const Expr& e) const; - - /** - * Order comparison operator. The only invariant on the order of expressions - * is that the expressions that were created sooner will be smaller in the - * ordering than all the expressions created later. Null expression is the - * smallest element of the ordering. The behavior of the operator is - * undefined if the expressions come from two different expression managers. - * - * @param e the expression to compare to - * @return true if this expression is greater than the given one - */ - bool operator>(const Expr& e) const; - - /** - * Order comparison operator. The only invariant on the order of expressions - * is that the expressions that were created sooner will be smaller in the - * ordering than all the expressions created later. Null expression is the - * smallest element of the ordering. The behavior of the operator is - * undefined if the expressions come from two different expression managers. - * - * @param e the expression to compare to - * @return true if this expression is smaller or equal to the given one - */ - bool operator<=(const Expr& e) const { return !(*this > e); } - - /** - * Order comparison operator. The only invariant on the order of expressions - * is that the expressions that were created sooner will be smaller in the - * ordering than all the expressions created later. Null expression is the - * smallest element of the ordering. The behavior of the operator is - * undefined if the expressions come from two different expression managers. - * - * @param e the expression to compare to - * @return true if this expression is greater or equal to the given one - */ - bool operator>=(const Expr& e) const { return !(*this < e); } - - /** - * Get the ID of this expression (used for the comparison operators). - * - * @return an identifier uniquely identifying the value this - * expression holds. - */ - uint64_t getId() const; - - /** - * Returns the kind of the expression (AND, PLUS ...). - * - * @return the kind of the expression - */ - Kind getKind() const; - - /** - * Returns the number of children of this expression. - * - * @return the number of children - */ - size_t getNumChildren() const; - - /** - * Returns the i'th child of this expression. - * - * @param i the index of the child to retrieve - * @return the child - */ - Expr operator[](unsigned i) const; - - /** - * Returns the children of this Expr. - */ - std::vector getChildren() const { - return std::vector(begin(), end()); - } - - /** - * Returns the Boolean negation of this Expr. - */ - Expr notExpr() const; - - /** - * Returns the conjunction of this expression and - * the given expression. - */ - Expr andExpr(const Expr& e) const; - - /** - * Returns the disjunction of this expression and - * the given expression. - */ - Expr orExpr(const Expr& e) const; - - /** - * Returns the exclusive disjunction of this expression and - * the given expression. - */ - Expr xorExpr(const Expr& e) const; - - /** - * Returns the Boolean equivalence of this expression and - * the given expression. - */ - Expr eqExpr(const Expr& e) const; - - /** - * Returns the implication of this expression and - * the given expression. - */ - Expr impExpr(const Expr& e) const; - - /** - * Returns the if-then-else expression with this expression - * as the Boolean condition and the given expressions as - * the "then" and "else" expressions. - */ - Expr iteExpr(const Expr& then_e, const Expr& else_e) const; - - /** - * Iterator type for the children of an Expr. - */ - class const_iterator : public std::iterator { - ExprManager* d_exprManager; - void* d_iterator; - - explicit const_iterator(ExprManager*, void*); - - friend class Expr;// to access void* constructor - - public: - const_iterator(); - const_iterator(const const_iterator& it); - const_iterator& operator=(const const_iterator& it); - ~const_iterator(); - bool operator==(const const_iterator& it) const; - bool operator!=(const const_iterator& it) const { - return !(*this == it); - } - const_iterator& operator++(); - const_iterator operator++(int); - Expr operator*() const; - };/* class Expr::const_iterator */ - - /** - * Returns an iterator to the first child of this Expr. - */ - const_iterator begin() const; - - /** - * Returns an iterator to one-off-the-last child of this Expr. - */ - const_iterator end() const; - - /** - * Check if this is an expression that has an operator. - * - * @return true if this expression has an operator - */ - bool hasOperator() const; - - /** - * Get the operator of this expression. - * - * @throws IllegalArgumentException if it has no operator - * @return the operator of this expression - */ - Expr getOperator() const; - - /** - * Check if this is an expression is parameterized. - * - * @return true if this expression is parameterized. - * - * In detail, an expression that is parameterized is one that has an operator - * that must be provided in addition to its kind to construct it. For example, - * say we want to re-construct an Expr e where its children a1, ..., an are - * replaced by b1 ... bn. Then there are two cases: - * (1) If e is parametric, call: - * ExprManager::mkExpr(e.getKind(), e.getOperator(), b1, ..., bn ) - * (2) If e is not parametric, call: - * ExprManager::mkExpr(e.getKind(), b1, ..., bn ) - */ - bool isParameterized() const; - - /** - * Get the type for this Expr and optionally do type checking. - * - * Initial type computation will be near-constant time if - * type checking is not requested. Results are memoized, so that - * subsequent calls to getType() without type checking will be - * constant time. - * - * Initial type checking is linear in the size of the expression. - * Again, the results are memoized, so that subsequent calls to - * getType(), with or without type checking, will be constant - * time. - * - * NOTE: A TypeCheckingException can be thrown even when type - * checking is not requested. getType() will always return a - * valid and correct type and, thus, an exception will be thrown - * when no valid or correct type can be computed (e.g., if the - * arguments to a bit-vector operation aren't bit-vectors). When - * type checking is not requested, getType() will do the minimum - * amount of checking required to return a valid result. - * - * @param check whether we should check the type as we compute it - * (default: false) - */ - Type getType(bool check = false) const; - - /** - * Substitute "replacement" in for "e". - */ - Expr substitute(Expr e, Expr replacement) const; - - /** - * Substitute "replacements" in for "exes". - */ - Expr substitute(const std::vector exes, - const std::vector& replacements) const; - - /** - * Substitute pairs of (ex,replacement) from the given map. - */ - Expr substitute(const std::unordered_map map) const; - - /** - * Returns the string representation of the expression. - * @return a string representation of the expression - */ - std::string toString() const; - - /** - * Outputs the string representation of the expression to the stream. - * - * @param out the stream to serialize this expression to - * @param toDepth the depth to which to print this expression, or -1 - * to print it fully - * @param dag the dagification threshold to use (0 == off) - * @param language the language in which to output - */ - void toStream(std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const; - - /** - * Check if this is a null expression. - * - * @return true if a null expression - */ - bool isNull() const; - - /** - * Check if this is an expression representing a variable. - * - * @return true if a variable expression - */ - bool isVariable() const; - - /** - * Check if this is an expression representing a constant. - * - * @return true if a constant expression - */ - bool isConst() const; - - /** - * Check if this expression contains a free variable. - * - * @return true if this node contains a free variable. - */ - bool hasFreeVariable() const; - - /* 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 CVC4 - * 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 - - /** Extract a constant of type T */ - template - const T& getConst() const; - - /** - * Returns the expression reponsible for this expression. - */ - ExprManager* getExprManager() const; - - /** - * Maps this Expr into one for a different ExprManager, using - * variableMap for the translation and extending it with any new - * mappings. - */ - Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const; - - /** - * Very basic pretty printer for Expr. - * This is equivalent to calling e.getNode().printAst(...) - * @param out output stream to print to. - * @param indent number of spaces to indent the formula by. - */ - void printAst(std::ostream& out, int indent = 0) const; - -private: - - /** - * Pretty printer for use within gdb - * This is not intended to be used outside of gdb. - * This writes to the ostream Warning() and immediately flushes - * the ostream. - */ - void debugPrint(); - - /** - * Returns the actual internal node. - * @return the internal node - */ - NodeTemplate getNode() const; - - /** - * Returns the actual internal node as a TNode. - * @return the internal node - */ - NodeTemplate getTNode() const; - template friend class NodeTemplate; - -};/* class Expr */ - -${getConst_instantiations} - -inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { - return (size_t) e.getId(); -} - -}/* CVC4 namespace */ - -#endif /* CVC4__EXPR_H */ diff --git a/src/expr/node.h b/src/expr/node.h index 7e6324822..bb8c5618c 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -23,6 +23,7 @@ #define CVC4__NODE_H #include +#include #include #include #include @@ -32,7 +33,6 @@ #include "base/check.h" #include "base/exception.h" #include "base/output.h" -#include "expr/expr.h" #include "expr/expr_iomanip.h" #include "expr/kind.h" #include "expr/metakind.h" @@ -170,8 +170,6 @@ class NodeTemplate { */ friend class expr::NodeValue; - friend class expr::ExportPrivate; - /** A convenient null-valued encapsulated pointer */ static NodeTemplate s_null; @@ -268,14 +266,6 @@ public: */ NodeTemplate(const NodeTemplate& node); - /** - * Allow Exprs to become Nodes. This permits flexible translation of - * Exprs -> Nodes inside the CVC4 library without exposing a toNode() - * function in the public interface, or requiring lots of "friend" - * relationships. - */ - NodeTemplate(const Expr& e); - /** * Assignment operator for nodes, copies the relevant information from node * to this node. @@ -415,23 +405,6 @@ public: // bool containsDecision(); // is "atomic" // bool properlyContainsDecision(); // maybe not atomic but all children are - - /** - * Convert this Node into an Expr using the currently-in-scope - * manager. Essentially this is like an "operator Expr()" but we - * don't want it to compete with implicit conversions between e.g. - * Node and TNode, and we want internal-to-external interface - * (Node -> Expr) points to be explicit. We could write an - * explicit Expr(Node) constructor---but that dirties the public - * interface. - */ - inline Expr toExpr() const; - - /** - * Convert an Expr into a Node. - */ - static inline Node fromExpr(const Expr& e); - /** * Returns true if this node represents a constant * @return true if const @@ -1103,18 +1076,6 @@ NodeTemplate::NodeTemplate(const NodeTemplate& e) { } } -template -NodeTemplate::NodeTemplate(const Expr& e) { - Assert(e.d_node != NULL) << "Expecting a non-NULL expression value!"; - Assert(e.d_node->d_nv != NULL) << "Expecting a non-NULL expression value!"; - d_nv = e.d_node->d_nv; - // shouldn't ever fail - Assert(d_nv->d_rc > 0) << "Node constructed from Expr with rc == 0"; - if(ref_count) { - d_nv->inc(); - } -} - template NodeTemplate::~NodeTemplate() { Assert(d_nv != NULL) << "Expecting a non-NULL expression value!"; @@ -1459,18 +1420,6 @@ NodeTemplate::substitute(Iterator substitutionsBegin, } } -template -inline Expr NodeTemplate::toExpr() const { - assertTNodeNotExpired(); - return NodeManager::currentNM()->toExpr(*this); -} - -// intentionally not defined for TNode -template <> -inline Node NodeTemplate::fromExpr(const Expr& e) { - return NodeManager::fromExpr(e); -} - #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c34aa0a87..2d5ed36fb 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -94,14 +94,13 @@ namespace attr { // attribute that stores the canonical bound variable list for function types typedef expr::Attribute LambdaBoundVarListAttr; -NodeManager::NodeManager(ExprManager* exprManager) +NodeManager::NodeManager() : d_statisticsRegistry(new StatisticsRegistry()), d_skManager(new SkolemManager), d_bvManager(new BoundVarManager), next_id(0), d_attrManager(new expr::attr::AttributeManager()), - d_exprManager(exprManager), - d_nodeUnderDeletion(NULL), + d_nodeUnderDeletion(nullptr), d_inReclaimZombies(false), d_abstractValueCount(0), d_skolemCounter(0) diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d113c1458..348200b6e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -22,8 +22,6 @@ //#include "expr/attribute.h" #include "expr/node.h" #include "expr/type_node.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" #ifndef CVC4__NODE_MANAGER_H #define CVC4__NODE_MANAGER_H @@ -90,9 +88,6 @@ class NodeManager friend class api::Solver; friend class expr::NodeValue; friend class expr::TypeChecker; - // friends so they can access mkVar() here, which is private - friend Expr ExprManager::mkVar(const std::string&, Type); - friend Expr ExprManager::mkVar(Type); template friend class NodeBuilder; @@ -134,9 +129,6 @@ class NodeManager expr::attr::AttributeManager* d_attrManager; - /** The associated ExprManager */ - ExprManager* d_exprManager; - /** * The node value we're currently freeing. This unique node value * is permitted to have outstanding TNodes to it (in "soft" @@ -292,14 +284,10 @@ class NodeManager // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies` // already contains a node value with the same id as `nv`, but the pointers // are different, then the wrong `NodeManager` was in scope for one of the - // two nodes when it reached refcount zero. This can happen for example if - // you create a node with a `NodeManager` n1 and then call `Node::toExpr()` - // on that node while a different `NodeManager` n2 is in scope. When that - // `Expr` is deleted and the node reaches refcount zero in the `Expr`'s - // destructor, then `markForDeletion()` will be called on n2. + // two nodes when it reached refcount zero. Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv); - d_zombies.insert(nv); // FIXME multithreading + d_zombies.insert(nv); if(safeToReclaimZombies()) { if(d_zombies.size() > 5000) { @@ -392,8 +380,7 @@ class NodeManager Node* mkVarPtr(const TypeNode& type); public: - - explicit NodeManager(ExprManager* exprManager); + explicit NodeManager(); ~NodeManager(); /** The node manager in the current public-facing CVC4 library context */ @@ -1103,37 +1090,6 @@ class NodeManager */ TypeNode getType(TNode n, bool check = false); - /** - * Convert a node to an expression. Uses the ExprManager - * associated to this NodeManager. - */ - inline Expr toExpr(TNode n); - - /** - * Convert an expression to a node. - */ - static inline Node fromExpr(const Expr& e); - - /** - * Convert a node manager to an expression manager. - */ - inline ExprManager* toExprManager(); - - /** - * Convert an expression manager to a node manager. - */ - static inline NodeManager* fromExprManager(ExprManager* exprManager); - - /** - * Convert a type node to a type. - */ - inline Type toType(const TypeNode& tn); - - /** - * Convert a type to a type node. - */ - static inline TypeNode fromType(Type t); - /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/ void reclaimZombiesUntil(uint32_t k); @@ -1165,8 +1121,7 @@ class NodeManager * public-interface calls into the CVC4 library, where CVC4's notion * of the "current" NodeManager should be set to match * the calling context. See, for example, the implementations of - * public calls in the ExprManager and - * SmtEngine classes. + * public calls in the SmtEngine class. * * The client must be careful to create and destroy * NodeManagerScope objects in a well-nested manner (such @@ -1183,10 +1138,6 @@ class NodeManagerScope { public: NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) { - // There are corner cases where nm can be NULL and it's ok. - // For example, if you write { Expr e; }, then when the null - // Expr is destructed, there's no active node manager. - // Assert(nm != NULL); NodeManager::s_current = nm; Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } @@ -1274,31 +1225,6 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) { d_nodeValuePool.erase(nv);// FIXME multithreading } -inline Expr NodeManager::toExpr(TNode n) { - return Expr(d_exprManager, new Node(n)); -} - -inline Node NodeManager::fromExpr(const Expr& e) { - return e.getNode(); -} - -inline ExprManager* NodeManager::toExprManager() { - return d_exprManager; -} - -inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) { - return exprManager->getNodeManager(); -} - -inline Type NodeManager::toType(const TypeNode& tn) -{ - return Type(this, new TypeNode(tn)); -} - -inline TypeNode NodeManager::fromType(Type t) { - return *Type::getTypeNode(t); -} - }/* CVC4 namespace */ #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP diff --git a/src/expr/type.cpp b/src/expr/type.cpp deleted file mode 100644 index baf3ddf8c..000000000 --- a/src/expr/type.cpp +++ /dev/null @@ -1,681 +0,0 @@ -/********************* */ -/*! \file type.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of expression types - ** - ** Implementation of expression types. - **/ -#include "expr/type.h" - -#include -#include -#include -#include - -#include "base/exception.h" -#include "expr/node_manager.h" -#include "expr/node_manager_attributes.h" -#include "expr/type_node.h" - -using namespace std; - -namespace CVC4 { - -ostream& operator<<(ostream& out, const Type& t) { - NodeManagerScope nms(t.d_nodeManager); - return out << *Type::getTypeNode(t); -} - -Type Type::makeType(const TypeNode& typeNode) const { - return Type(d_nodeManager, new TypeNode(typeNode)); -} - -Type::Type(NodeManager* nm, TypeNode* node) - : d_typeNode(node), d_nodeManager(nm) { - // This does not require a NodeManagerScope as this is restricted to be an - // internal only pointer initialization call. -} - -Type::Type() : d_typeNode(new TypeNode), d_nodeManager(NULL) { - // This does not require a NodeManagerScope as `new TypeNode` is backed by a - // static expr::NodeValue::null(). -} - -Type::Type(const Type& t) : d_typeNode(NULL), d_nodeManager(t.d_nodeManager) { - NodeManagerScope nms(d_nodeManager); - d_typeNode = new TypeNode(*t.d_typeNode); -} - -Type::~Type() { - NodeManagerScope nms(d_nodeManager); - delete d_typeNode; -} - -bool Type::isNull() const { - return d_typeNode->isNull(); -} - -Cardinality Type::getCardinality() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getCardinality(); -} - -bool Type::isFinite() const -{ - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isFinite(); -} - -bool Type::isInterpretedFinite() const -{ - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isInterpretedFinite(); -} - -bool Type::isWellFounded() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isWellFounded(); -} - -bool Type::isFirstClass() const -{ - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isFirstClass(); -} - -bool Type::isFunctionLike() const -{ - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isFunctionLike(); -} - -Expr Type::mkGroundTerm() const { - NodeManagerScope nms(d_nodeManager); - Expr ret = d_typeNode->mkGroundTerm().toExpr(); - if (ret.isNull()) - { - IllegalArgument(this, "Cannot construct ground term!"); - } - return ret; -} - -Expr Type::mkGroundValue() const -{ - NodeManagerScope nms(d_nodeManager); - return d_typeNode->mkGroundValue().toExpr(); -} - -bool Type::isSubtypeOf(Type t) const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isSubtypeOf(*t.d_typeNode); -} - -bool Type::isComparableTo(Type t) const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isComparableTo(*t.d_typeNode); -} - -Type Type::getBaseType() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getBaseType().toType(); -} - -Type& Type::operator=(const Type& t) { - PrettyCheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!"); - PrettyCheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!"); - - if(this != &t) { - if(d_nodeManager == t.d_nodeManager) { - NodeManagerScope nms(d_nodeManager); - *d_typeNode = *t.d_typeNode; - } else { - // This happens more than you think---every time you set to or - // from the null Type. It's tricky because each node manager - // must be in play at the right time. - - NodeManagerScope nms1(d_nodeManager); - *d_typeNode = TypeNode::null(); - - NodeManagerScope nms2(t.d_nodeManager); - *d_typeNode = *t.d_typeNode; - - d_nodeManager = t.d_nodeManager; - } - } - return *this; -} - -bool Type::operator==(const Type& t) const { - NodeManagerScope nms(d_nodeManager); - return *d_typeNode == *t.d_typeNode; -} - -bool Type::operator!=(const Type& t) const { - NodeManagerScope nms(d_nodeManager); - return *d_typeNode != *t.d_typeNode; -} - -bool Type::operator<(const Type& t) const { - NodeManagerScope nms(d_nodeManager); - return *d_typeNode < *t.d_typeNode; -} - -bool Type::operator<=(const Type& t) const { - NodeManagerScope nms(d_nodeManager); - return *d_typeNode <= *t.d_typeNode; -} - -bool Type::operator>(const Type& t) const { - NodeManagerScope nms(d_nodeManager); - return *d_typeNode > *t.d_typeNode; -} - -bool Type::operator>=(const Type& t) const { - NodeManagerScope nms(d_nodeManager); - return *d_typeNode >= *t.d_typeNode; -} - -Type Type::substitute(const Type& type, const Type& replacement) const { - NodeManagerScope nms(d_nodeManager); - return makeType(d_typeNode->substitute(*type.d_typeNode, - *replacement.d_typeNode)); -} - -Type Type::substitute(const std::vector& types, - const std::vector& replacements) const { - NodeManagerScope nms(d_nodeManager); - - vector typesNodes, replacementsNodes; - - for(vector::const_iterator i = types.begin(), - iend = types.end(); - i != iend; - ++i) { - typesNodes.push_back(*(*i).d_typeNode); - } - - for(vector::const_iterator i = replacements.begin(), - iend = replacements.end(); - i != iend; - ++i) { - replacementsNodes.push_back(*(*i).d_typeNode); - } - - return makeType(d_typeNode->substitute(typesNodes.begin(), - typesNodes.end(), - replacementsNodes.begin(), - replacementsNodes.end())); -} - -ExprManager* Type::getExprManager() const { - return d_nodeManager->toExprManager(); -} - -Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const { - return ExprManager::exportType(*this, exprManager, vmap); -} - -void Type::toStream(std::ostream& out) const { - NodeManagerScope nms(d_nodeManager); - out << *d_typeNode; - return; -} - -string Type::toString() const { - NodeManagerScope nms(d_nodeManager); - stringstream ss; - ss << *d_typeNode; - return ss.str(); -} - -/** Is this the Boolean type? */ -bool Type::isBoolean() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isBoolean(); -} - -/** Is this the integer type? */ -bool Type::isInteger() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isInteger(); -} - -/** Is this the real type? */ -bool Type::isReal() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isReal(); -} - -/** Is this the string type? */ -bool Type::isString() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isString(); -} - -/** Is this the regexp type? */ -bool Type::isRegExp() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isRegExp(); -} - -/** Is this the rounding mode type? */ -bool Type::isRoundingMode() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isRoundingMode(); -} - -/** Is this the bit-vector type? */ -bool Type::isBitVector() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isBitVector(); -} - -/** Is this the floating-point type? */ -bool Type::isFloatingPoint() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isFloatingPoint(); -} - -/** Is this a datatype type? */ -bool Type::isDatatype() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isDatatype(); -} - -/** Is this the Constructor type? */ -bool Type::isConstructor() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isConstructor(); -} - -/** Is this the Selector type? */ -bool Type::isSelector() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isSelector(); -} - -/** Is this the Tester type? */ -bool Type::isTester() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isTester(); -} - -/** Is this a function type? */ -bool Type::isFunction() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isFunction(); -} - -/** - * Is this a predicate type? NOTE: all predicate types are also - * function types. - */ -bool Type::isPredicate() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isPredicate(); -} - -/** Is this a tuple type? */ -bool Type::isTuple() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isTuple(); -} - -/** Is this a record type? */ -bool Type::isRecord() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isRecord(); -} - -/** Is this a symbolic expression type? */ -bool Type::isSExpr() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isSExpr(); -} - -/** Is this an array type? */ -bool Type::isArray() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isArray(); -} - -/** Is this a Set type? */ -bool Type::isSet() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isSet(); -} - -bool Type::isSequence() const -{ - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isSequence(); -} - -/** Is this a sort kind */ -bool Type::isSort() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isSort(); -} - -/** Cast to a sort type */ -bool Type::isSortConstructor() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isSortConstructor(); -} - -size_t FunctionType::getArity() const { - return d_typeNode->getNumChildren() - 1; -} - -vector FunctionType::getArgTypes() const { - NodeManagerScope nms(d_nodeManager); - vector args; - vector argNodes = d_typeNode->getArgTypes(); - vector::iterator it = argNodes.begin(); - vector::iterator it_end = argNodes.end(); - for(; it != it_end; ++ it) { - args.push_back(makeType(*it)); - } - return args; -} - -Type FunctionType::getRangeType() const { - NodeManagerScope nms(d_nodeManager); - PrettyCheckArgument(isNull() || isFunction(), this); - return makeType(d_typeNode->getRangeType()); -} - -vector SExprType::getTypes() const { - NodeManagerScope nms(d_nodeManager); - vector types; - vector typeNodes = d_typeNode->getSExprTypes(); - vector::iterator it = typeNodes.begin(); - vector::iterator it_end = typeNodes.end(); - for(; it != it_end; ++ it) { - types.push_back(makeType(*it)); - } - return types; -} - -string SortType::getName() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getAttribute(expr::VarNameAttr()); -} - -bool SortType::isParameterized() const { - return false; -} - -/** Get the parameter types */ -std::vector SortType::getParamTypes() const { - vector params; - return params; -} - -string SortConstructorType::getName() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getAttribute(expr::VarNameAttr()); -} - -size_t SortConstructorType::getArity() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getAttribute(expr::SortArityAttr()); -} - -SortType SortConstructorType::instantiate(const std::vector& params) const { - NodeManagerScope nms(d_nodeManager); - vector paramsNodes; - for(vector::const_iterator i = params.begin(), - iend = params.end(); - i != iend; - ++i) { - paramsNodes.push_back(*getTypeNode(*i)); - } - return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes))); -} - -BooleanType::BooleanType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isBoolean(), this); -} - -IntegerType::IntegerType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isInteger(), this); -} - -RealType::RealType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isReal(), this); -} - -StringType::StringType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isString(), this); -} - -RegExpType::RegExpType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isRegExp(), this); -} - -RoundingModeType::RoundingModeType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isRoundingMode(), this); -} - -BitVectorType::BitVectorType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isBitVector(), this); -} - -FloatingPointType::FloatingPointType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isFloatingPoint(), this); -} - -DatatypeType::DatatypeType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isDatatype(), this); -} - -ConstructorType::ConstructorType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isConstructor(), this); -} - -SelectorType::SelectorType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isSelector(), this); -} - -TesterType::TesterType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isTester(), this); -} - -FunctionType::FunctionType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isFunction(), this); -} - -SExprType::SExprType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isSExpr(), this); -} - -ArrayType::ArrayType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isArray(), this); -} - -SetType::SetType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isSet(), this); -} - -SequenceType::SequenceType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isSequence(), this); -} - -SortType::SortType(const Type& t) : Type(t) -{ - PrettyCheckArgument(isNull() || isSort(), this); -} - -SortConstructorType::SortConstructorType(const Type& t) - : Type(t) { - PrettyCheckArgument(isNull() || isSortConstructor(), this); -} - -unsigned BitVectorType::getSize() const { - return d_typeNode->getBitVectorSize(); -} - -unsigned FloatingPointType::getExponentSize() const { - return d_typeNode->getFloatingPointExponentSize(); -} - -unsigned FloatingPointType::getSignificandSize() const { - return d_typeNode->getFloatingPointSignificandSize(); -} - -Type ArrayType::getIndexType() const { - return makeType(d_typeNode->getArrayIndexType()); -} - -Type ArrayType::getConstituentType() const { - return makeType(d_typeNode->getArrayConstituentType()); -} - -Type SetType::getElementType() const { - return makeType(d_typeNode->getSetElementType()); -} - -Type SequenceType::getElementType() const -{ - return makeType(d_typeNode->getSequenceElementType()); -} - -DatatypeType ConstructorType::getRangeType() const { - return DatatypeType(makeType(d_typeNode->getConstructorRangeType())); -} - -size_t ConstructorType::getArity() const { - return d_typeNode->getNumChildren() - 1; -} - -std::vector ConstructorType::getArgTypes() const { - NodeManagerScope nms(d_nodeManager); - vector args; - vector argNodes = d_typeNode->getArgTypes(); - vector::iterator it = argNodes.begin(); - vector::iterator it_end = argNodes.end(); - for(; it != it_end; ++ it) { - args.push_back(makeType(*it)); - } - return args; -} - -bool DatatypeType::isParametric() const { - return d_typeNode->isParametricDatatype(); -} - -bool DatatypeType::isInstantiated() const { - return d_typeNode->isInstantiatedDatatype(); -} - -bool DatatypeType::isParameterInstantiated(unsigned n) const { - return d_typeNode->isParameterInstantiatedDatatype(n); -} - -size_t DatatypeType::getArity() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getNumChildren() - 1; -} - -std::vector DatatypeType::getParamTypes() const { - NodeManagerScope nms(d_nodeManager); - vector params; - vector paramNodes = d_typeNode->getParamTypes(); - vector::iterator it = paramNodes.begin(); - vector::iterator it_end = paramNodes.end(); - for(; it != it_end; ++it) { - params.push_back(makeType(*it)); - } - return params; -} - -DatatypeType DatatypeType::instantiate(const std::vector& params) const { - NodeManagerScope nms(d_nodeManager); - TypeNode cons = d_nodeManager->mkTypeConst( (*d_typeNode)[0].getConst() ); - vector paramsNodes; - paramsNodes.push_back( cons ); - for(vector::const_iterator i = params.begin(), - iend = params.end(); - i != iend; - ++i) { - paramsNodes.push_back(*getTypeNode(*i)); - } - return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes))); -} - -/** Get the length of a tuple type */ -size_t DatatypeType::getTupleLength() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getTupleLength(); -} - -/** Get the constituent types of a tuple type */ -std::vector DatatypeType::getTupleTypes() const { - NodeManagerScope nms(d_nodeManager); - std::vector< TypeNode > vec = d_typeNode->getTupleTypes(); - std::vector< Type > vect; - for( unsigned i=0; ibooleanType())); -} - -/* - not in release 1.0 -Expr PredicateSubtype::getPredicate() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getSubtypePredicate().toExpr(); -} - -Type PredicateSubtype::getParentType() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getSubtypeParentType().toType(); -} -*/ - -size_t TypeHashFunction::operator()(const Type& t) const { - return TypeNodeHashFunction()(NodeManager::fromType(t)); -} - -}/* CVC4 namespace */ diff --git a/src/expr/type.h b/src/expr/type.h deleted file mode 100644 index 8f8ccc1bf..000000000 --- a/src/expr/type.h +++ /dev/null @@ -1,695 +0,0 @@ -/********************* */ -/*! \file type.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Interface for expression types. - ** - ** Interface for expression types - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__TYPE_H -#define CVC4__TYPE_H - -#include -#include -#include - -#include "util/cardinality.h" - -namespace CVC4 { - -class NodeManager; -class CVC4_PUBLIC ExprManager; -class Expr; -class TypeNode; -struct CVC4_PUBLIC ExprManagerMapCollection; - -class SmtEngine; - -template -class NodeTemplate; - -class BooleanType; -class IntegerType; -class RealType; -class StringType; -class RegExpType; -class RoundingModeType; -class BitVectorType; -class ArrayType; -class SetType; -class DatatypeType; -class ConstructorType; -class SelectorType; -class TesterType; -class FunctionType; -class SExprType; -class SortType; -class SortConstructorType; -class Type; - -/** Hash function for Types */ -struct CVC4_PUBLIC TypeHashFunction { - /** Return a hash code for type t */ - size_t operator()(const CVC4::Type& t) const; -};/* struct TypeHashFunction */ - -/** - * Output operator for types - * @param out the stream to output to - * @param t the type to output - * @return the stream - */ -std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC; - -namespace expr { - TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap); -}/* CVC4::expr namespace */ - -/** - * Class encapsulating CVC4 expression types. - */ -class CVC4_PUBLIC Type { - - friend class SmtEngine; - friend class ExprManager; - friend class NodeManager; - friend class TypeNode; - friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t); - friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap); - -protected: - - /** The internal expression representation */ - TypeNode* d_typeNode; - - /** The responsible expression manager */ - NodeManager* d_nodeManager; - - /** - * Construct a new type given the typeNode, for internal use only. - * @param typeNode the TypeNode to use - * @return the Type corresponding to the TypeNode - */ - Type makeType(const TypeNode& typeNode) const; - - /** - * Constructor for internal purposes. - * @param em the expression manager that handles this expression - * @param typeNode the actual TypeNode pointer for this type - */ - Type(NodeManager* em, TypeNode* typeNode); - - /** Accessor for derived classes */ - static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; } - public: - /** Force a virtual destructor for safety. */ - virtual ~Type(); - - /** Default constructor */ - Type(); - - /** - * Copy constructor. - * @param t the type to make a copy of - */ - Type(const Type& t); - - /** - * Check whether this is a null type - * @return true if type is null - */ - bool isNull() const; - - /** - * Return the cardinality of this type. - */ - Cardinality getCardinality() const; - - /** - * Is this type finite? This assumes uninterpreted sorts have infinite - * cardinality. - */ - bool isFinite() const; - - /** - * Is this type interpreted as being finite. - * If finite model finding is enabled, this assumes all uninterpreted sorts - * are interpreted as finite. - */ - bool isInterpretedFinite() const; - - /** - * Is this a well-founded type? - */ - bool isWellFounded() const; - - /** - * Is this a first-class type? - * - * First-class types are types for which: - * (1) we handle equalities between terms of that type, and - * (2) they are allowed to be parameters of parametric types (e.g. index or - * element types of arrays). - * - * Examples of types that are not first-class include constructor types, - * selector types, tester types, regular expressions and SExprs. - */ - bool isFirstClass() const; - - /** - * Is this a function-LIKE type? - * - * Anything function-like except arrays (e.g., datatype selectors) is - * considered a function here. Function-like terms can not be the argument - * or return value for any term that is function-like. - * This is mainly to avoid higher order. - * - * Note that arrays are explicitly not considered function-like here. - * - * @return true if this is a function-like type - */ - bool isFunctionLike() const; - - /** - * Construct and return a ground term for this Type. Throws an - * exception if this type is not well-founded. - */ - Expr mkGroundTerm() const; - - /** - * Construct and return a ground value for this Type. Throws an - * exception if this type is not well-founded. - * - * This is the same as mkGroundTerm, but constructs a constant value instead - * of a canonical ground term. These two notions typically coincide. However, - * for uninterpreted sorts, they do not: mkGroundTerm returns a fresh variable - * whereas mkValue returns an uninterpreted constant. The motivation for - * mkGroundTerm is that unintepreted constants should never appear in lemmas. - * The motivation for mkGroundValue is for e.g. type enumeration and model - * construction. - */ - Expr mkGroundValue() const; - - /** - * Is this type a subtype of the given type? - */ - bool isSubtypeOf(Type t) const; - - /** - * Is this type comparable to the given type (i.e., do they share - * a common ancestor in the subtype tree)? - */ - bool isComparableTo(Type t) const; - - /** - * Get the most general base type of this type. - */ - Type getBaseType() const; - - /** - * Substitution of Types. - */ - Type substitute(const Type& type, const Type& replacement) const; - - /** - * Simultaneous substitution of Types. - */ - Type substitute(const std::vector& types, - const std::vector& replacements) const; - - /** - * Get this type's ExprManager. - */ - ExprManager* getExprManager() const; - - /** - * Exports this type into a different ExprManager. - */ - Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const; - - /** - * Assignment operator. - * @param t the type to assign to this type - * @return this type after assignment. - */ - Type& operator=(const Type& t); - - /** - * Comparison for structural equality. - * @param t the type to compare to - * @returns true if the types are equal - */ - bool operator==(const Type& t) const; - - /** - * Comparison for structural disequality. - * @param t the type to compare to - * @returns true if the types are not equal - */ - bool operator!=(const Type& t) const; - - /** - * An ordering on Types so they can be stored in maps, etc. - */ - bool operator<(const Type& t) const; - - /** - * An ordering on Types so they can be stored in maps, etc. - */ - bool operator<=(const Type& t) const; - - /** - * An ordering on Types so they can be stored in maps, etc. - */ - bool operator>(const Type& t) const; - - /** - * An ordering on Types so they can be stored in maps, etc. - */ - bool operator>=(const Type& t) const; - - /** - * Is this the Boolean type? - * @return true if the type is a Boolean type - */ - bool isBoolean() const; - - /** - * Is this the integer type? - * @return true if the type is a integer type - */ - bool isInteger() const; - - /** - * Is this the real type? - * @return true if the type is a real type - */ - bool isReal() const; - - /** - * Is this the string type? - * @return true if the type is the string type - */ - bool isString() const; - - /** - * Is this the regexp type? - * @return true if the type is the regexp type - */ - bool isRegExp() const; - - /** - * Is this the rounding mode type? - * @return true if the type is the rounding mode type - */ - bool isRoundingMode() const; - - /** - * Is this the bit-vector type? - * @return true if the type is a bit-vector type - */ - bool isBitVector() const; - - /** - * Is this the floating-point type? - * @return true if the type is a floating-point type - */ - bool isFloatingPoint() const; - - /** - * Is this a function type? - * @return true if the type is a function type - */ - bool isFunction() const; - - /** - * Is this a predicate type, i.e. if it's a function type mapping to Boolean. - * All predicate types are also function types. - * @return true if the type is a predicate type - */ - bool isPredicate() const; - - /** - * Is this a tuple type? - * @return true if the type is a tuple type - */ - bool isTuple() const; - - /** - * Is this a record type? - * @return true if the type is a record type - */ - bool isRecord() const; - - /** - * Is this a symbolic expression type? - * @return true if the type is a symbolic expression type - */ - bool isSExpr() const; - - /** - * Is this an array type? - * @return true if the type is a array type - */ - bool isArray() const; - - /** - * Is this a Set type? - * @return true if the type is a Set type - */ - bool isSet() const; - - /** - * Is this a Sequence type? - * @return true if the type is a Sequence type - */ - bool isSequence() const; - - /** - * Is this a datatype type? - * @return true if the type is a datatype type - */ - bool isDatatype() const; - - /** - * Is this a constructor type? - * @return true if the type is a constructor type - */ - bool isConstructor() const; - - /** - * Is this a selector type? - * @return true if the type is a selector type - */ - bool isSelector() const; - - /** - * Is this a tester type? - * @return true if the type is a tester type - */ - bool isTester() const; - - /** - * Is this a sort kind? - * @return true if this is a sort kind - */ - bool isSort() const; - - /** - * Is this a sort constructor kind? - * @return true if this is a sort constructor kind - */ - bool isSortConstructor() const; - - /** - * Is this a predicate subtype? - * @return true if this is a predicate subtype - */ - // not in release 1.0 - //bool isPredicateSubtype() const; - - /** - * Is this an integer subrange type? - * @return true if this is an integer subrange type - */ - //bool isSubrange() const; - - /** - * Outputs a string representation of this type to the stream. - * @param out the stream to output to - */ - void toStream(std::ostream& out) const; - - /** - * Constructs a string representation of this type. - */ - std::string toString() const; -};/* class Type */ - -/** Singleton class encapsulating the Boolean type. */ -class CVC4_PUBLIC BooleanType : public Type { - public: - /** Construct from the base type */ - BooleanType(const Type& type = Type()); -};/* class BooleanType */ - -/** Singleton class encapsulating the integer type. */ -class CVC4_PUBLIC IntegerType : public Type { - public: - /** Construct from the base type */ - IntegerType(const Type& type = Type()); -};/* class IntegerType */ - -/** Singleton class encapsulating the real type. */ -class CVC4_PUBLIC RealType : public Type { - public: - /** Construct from the base type */ - RealType(const Type& type = Type()); -};/* class RealType */ - -/** Singleton class encapsulating the string type. */ -class CVC4_PUBLIC StringType : public Type { - public: - /** Construct from the base type */ - StringType(const Type& type); -};/* class StringType */ - -/** Singleton class encapsulating the string type. */ -class CVC4_PUBLIC RegExpType : public Type { - public: - /** Construct from the base type */ - RegExpType(const Type& type); -};/* class RegExpType */ - -/** Singleton class encapsulating the rounding mode type. */ -class CVC4_PUBLIC RoundingModeType : public Type { - public: - /** Construct from the base type */ - RoundingModeType(const Type& type = Type()); -};/* class RoundingModeType */ - -/** Class encapsulating a function type. */ -class CVC4_PUBLIC FunctionType : public Type { - public: - /** Construct from the base type */ - FunctionType(const Type& type = Type()); - - /** Get the arity of the function type */ - size_t getArity() const; - - /** Get the argument types */ - std::vector getArgTypes() const; - - /** Get the range type (i.e., the type of the result). */ - Type getRangeType() const; -};/* class FunctionType */ - -/** Class encapsulating a sexpr type. */ -class CVC4_PUBLIC SExprType : public Type { - public: - /** Construct from the base type */ - SExprType(const Type& type = Type()); - - /** Get the constituent types */ - std::vector getTypes() const; -};/* class SExprType */ - -/** Class encapsulating an array type. */ -class CVC4_PUBLIC ArrayType : public Type { - public: - /** Construct from the base type */ - ArrayType(const Type& type = Type()); - - /** Get the index type */ - Type getIndexType() const; - - /** Get the constituent type */ - Type getConstituentType() const; -};/* class ArrayType */ - -/** Class encapsulating a set type. */ -class CVC4_PUBLIC SetType : public Type { - public: - /** Construct from the base type */ - SetType(const Type& type = Type()); - - /** Get the element type */ - Type getElementType() const; -}; /* class SetType */ - -/** Class encapsulating a sequence type. */ -class CVC4_PUBLIC SequenceType : public Type -{ - public: - /** Construct from the base type */ - SequenceType(const Type& type = Type()); - - /** Get the element type */ - Type getElementType() const; -}; /* class SetType */ - -/** Class encapsulating a user-defined sort. */ -class CVC4_PUBLIC SortType : public Type { - public: - /** Construct from the base type */ - SortType(const Type& type = Type()); - - /** Get the name of the sort */ - std::string getName() const; - - /** Is this type parameterized? */ - bool isParameterized() const; - - /** Get the parameter types */ - std::vector getParamTypes() const; - -};/* class SortType */ - -/** Class encapsulating a user-defined sort constructor. */ -class CVC4_PUBLIC SortConstructorType : public Type { - public: - /** Construct from the base type */ - SortConstructorType(const Type& type = Type()); - - /** Get the name of the sort constructor */ - std::string getName() const; - - /** Get the arity of the sort constructor */ - size_t getArity() const; - - /** Instantiate a sort using this sort constructor */ - SortType instantiate(const std::vector& params) const; - -};/* class SortConstructorType */ - -/** Class encapsulating the bit-vector type. */ -class CVC4_PUBLIC BitVectorType : public Type { - public: - /** Construct from the base type */ - BitVectorType(const Type& type = Type()); - - /** - * Returns the size of the bit-vector type. - * @return the width of the bit-vector type (> 0) - */ - unsigned getSize() const; - -};/* class BitVectorType */ - -/** Class encapsulating the floating point type. */ -class CVC4_PUBLIC FloatingPointType : public Type { - public: - /** Construct from the base type */ - FloatingPointType(const Type& type = Type()); - - /** - * Returns the size of the floating-point exponent type. - * @return the width of the floating-point exponent type (> 0) - */ - unsigned getExponentSize() const; - - /** - * Returns the size of the floating-point significand type. - * @return the width of the floating-point significand type (> 0) - */ - unsigned getSignificandSize() const; - -};/* class FloatingPointType */ - -/** Class encapsulating the datatype type */ -class CVC4_PUBLIC DatatypeType : public Type { - public: - /** Construct from the base type */ - DatatypeType(const Type& type = Type()); - - /** Is this datatype parametric? */ - bool isParametric() const; - /** - * Has this datatype been fully instantiated ? - * - * @return true if this datatype is not parametric or, if it is, it - * has been fully instantiated - */ - bool isInstantiated() const; - - /** Has this datatype been instantiated for parameter `n` ? */ - bool isParameterInstantiated(unsigned n) const; - - /** Get the parameter types */ - std::vector getParamTypes() const; - - /** Get the arity of the datatype constructor */ - size_t getArity() const; - - /** Instantiate a datatype using this datatype constructor */ - DatatypeType instantiate(const std::vector& params) const; - - /** Get the length of a tuple type */ - size_t getTupleLength() const; - - /** Get the constituent types of a tuple type */ - std::vector getTupleTypes() const; - -};/* class DatatypeType */ - -/** Class encapsulating the constructor type. */ -class CVC4_PUBLIC ConstructorType : public Type { - public: - /** Construct from the base type */ - ConstructorType(const Type& type = Type()); - - /** Get the range type */ - DatatypeType getRangeType() const; - - /** Get the argument types */ - std::vector getArgTypes() const; - - /** Get the number of constructor arguments */ - size_t getArity() const; - -};/* class ConstructorType */ - -/** Class encapsulating the Selector type. */ -class CVC4_PUBLIC SelectorType : public Type { - public: - /** Construct from the base type */ - SelectorType(const Type& type = Type()); - - /** Get the domain type for this selector (the datatype type) */ - DatatypeType getDomain() const; - - /** Get the range type for this selector (the field type) */ - Type getRangeType() const; - -};/* class SelectorType */ - -/** Class encapsulating the Tester type. */ -class CVC4_PUBLIC TesterType : public Type { - public: - /** Construct from the base type */ - TesterType(const Type& type = Type()); - - /** Get the type that this tester tests (the datatype type) */ - DatatypeType getDomain() const; - - /** - * Get the range type for this tester (included for sake of - * interface completeness), but doesn't give useful information). - */ - BooleanType getRangeType() const; - -};/* class TesterType */ - -}/* CVC4 namespace */ - -#endif /* CVC4__TYPE_H */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 63c26f5e9..15cfeede6 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -403,17 +403,6 @@ public: return d_nv == &expr::NodeValue::null(); } - /** - * Convert this TypeNode into a Type using the currently-in-scope - * manager. - */ - inline Type toType() const; - - /** - * Convert a Type into a TypeNode. - */ - inline static TypeNode fromType(const Type& t); - /** * Returns the cardinality of this type. * @@ -772,16 +761,6 @@ typedef TypeNode::HashFunction TypeNodeHashFunction; namespace CVC4 { -inline Type TypeNode::toType() const -{ - return NodeManager::currentNM()->toType(*this); -} - -inline TypeNode TypeNode::fromType(const Type& t) { - NodeManagerScope scope(t.d_nodeManager); - return NodeManager::fromType(t); -} - inline TypeNode TypeNode::substitute(const TypeNode& type, const TypeNode& replacement) const { diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h deleted file mode 100644 index afccac13f..000000000 --- a/src/expr/variable_type_map.h +++ /dev/null @@ -1,63 +0,0 @@ -/********************* */ -/*! \file variable_type_map.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__VARIABLE_TYPE_MAP_H -#define CVC4__VARIABLE_TYPE_MAP_H - -#include - -#include "expr/expr.h" - -namespace CVC4 { - -class Expr; -struct ExprHashFunction; -class Type; -struct TypeHashFunction; - -class CVC4_PUBLIC VariableTypeMap { - /** - * A map Expr -> Expr, intended to be used for a mapping of variables - * between two ExprManagers. - */ - std::unordered_map d_variables; - - /** - * A map Type -> Type, intended to be used for a mapping of types - * between two ExprManagers. - */ - std::unordered_map d_types; - -public: - Expr& operator[](Expr e) { return d_variables[e]; } - Type& operator[](Type t) { return d_types[t]; } - -};/* class VariableTypeMap */ - -typedef std::unordered_map VarMap; - -struct CVC4_PUBLIC ExprManagerMapCollection { - VariableTypeMap d_typeMap; - VarMap d_to; - VarMap d_from; -};/* struct ExprManagerMapCollection */ - -}/* CVC4 namespace */ - -#endif /* CVC4__VARIABLE_MAP_H */ diff --git a/src/include/cvc4.h b/src/include/cvc4.h index 48db2b689..f35b1c5e6 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -21,8 +21,6 @@ #include #include #include -#include -#include #include #include #include diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 6174d381d..f5e81bb9c 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -646,8 +646,8 @@ Node BVToInt::translateWithChildren(Node original, */ if (childrenTypesChanged(original) && options::ufHo()) { - throw TypeCheckingException( - original.toExpr(), + throw TypeCheckingExceptionPrivate( + original, string("Cannot translate to Int: ") + original.toString()); } // Insert the translated application term to the cache diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 152c096e0..e857b7b61 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -163,9 +163,9 @@ Node intToBV(TNode n, NodeMap& cache) case kind::ITE: break; default: if (childrenTypesChanged(current, cache)) { - throw TypeCheckingException( - current.toExpr(), - string("Cannot translate to BV: ") + current.toString()); + throw TypeCheckingExceptionPrivate( + current, + string("Cannot translate to BV: ") + current.toString()); } break; } @@ -225,8 +225,8 @@ Node intToBV(TNode n, NodeMap& cache) BitVector bv(size, constant.getNumerator()); if (bv.toSignedInteger() != constant.getNumerator()) { - throw TypeCheckingException( - current.toExpr(), + throw TypeCheckingExceptionPrivate( + current, string("Not enough bits for constant in intToBV: ") + current.toString()); } @@ -239,9 +239,8 @@ Node intToBV(TNode n, NodeMap& cache) } else { - throw TypeCheckingException( - current.toExpr(), - string("Cannot translate to BV: ") + current.toString()); + throw TypeCheckingExceptionPrivate( + current, string("Cannot translate to BV: ") + current.toString()); } cache[current] = result; } diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index c37ac9c20..9c58250e3 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -116,8 +116,8 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va } else { - throw TypeCheckingException( - v.toExpr(), + throw TypeCheckingExceptionPrivate( + v, std::string("Cannot translate to Int: ") + v.toString()); } } @@ -171,8 +171,8 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va { // cannot change the type of quantified variables, since this leads // to incompleteness. - throw TypeCheckingException( - n.toExpr(), + throw TypeCheckingExceptionPrivate( + n, std::string("Cannot translate bound variable to Int: ") + n.toString()); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 715f74c43..280dc7047 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -401,7 +401,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, out << "TUPLE"; } } - else if (t.toType().isRecord()) + else if (t.isRecord()) { const DType& dt = t.getDType(); const DTypeConstructor& recCons = dt[0]; @@ -448,11 +448,11 @@ void CvcPrinter::toStreamNode(std::ostream& out, int sindex; if (n.getKind() == kind::APPLY_SELECTOR) { - sindex = DType::indexOf(opn.toExpr()); + sindex = DType::indexOf(opn); } else { - sindex = dt[0].getSelectorIndexInternal(opn.toExpr()); + sindex = dt[0].getSelectorIndexInternal(opn); } Assert(sindex >= 0); out << sindex; @@ -468,7 +468,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, } break; case kind::APPLY_TESTER: { - Assert(!n.getType().isTuple() && !n.getType().toType().isRecord()); + Assert(!n.getType().isTuple() && !n.getType().isRecord()); op << "is_"; unsigned cindex = DType::indexOf(n.getOperator()); const DType& dt = DType::datatypeOf(n.getOperator()); @@ -733,14 +733,14 @@ void CvcPrinter::toStreamNode(std::ostream& out, unsigned child = 0; while (child < numc) { out << "BVPLUS("; - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[child], depth, false, lbind); out << ','; ++child; } out << "BVPLUS("; - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[child], depth, false, lbind); out << ','; @@ -756,7 +756,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, case kind::BITVECTOR_SUB: out << "BVSUB("; Assert(n.getType().isBitVector()); - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[0], depth, false, lbind); out << ','; @@ -770,14 +770,14 @@ void CvcPrinter::toStreamNode(std::ostream& out, unsigned child = 0; while (child < numc) { out << "BVMULT("; - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[child], depth, false, lbind); out << ','; ++child; } out << "BVMULT("; - out << BitVectorType(n.getType().toType()).getSize(); + out << n.getType().getBitVectorSize(); out << ','; toStreamNode(out, n[child], depth, false, lbind); out << ','; @@ -813,7 +813,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, case kind::BITVECTOR_SIGN_EXTEND: out << "SX("; toStreamNode(out, n[0], depth, false, lbind); - out << ", " << BitVectorType(n.getType().toType()).getSize() << ')'; + out << ", " << n.getType().getBitVectorSize() << ')'; return; break; case kind::BITVECTOR_ROTATE_LEFT: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f21683525..7a27794e6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -995,8 +995,8 @@ void Smt2Printer::toStream(std::ostream& out, if(toDepth != 0) { if (n.getKind() == kind::APPLY_TESTER) { - unsigned cindex = DType::indexOf(n.getOperator().toExpr()); - const DType& dt = DType::datatypeOf(n.getOperator().toExpr()); + unsigned cindex = DType::indexOf(n.getOperator()); + const DType& dt = DType::datatypeOf(n.getOperator()); out << "(_ is "; toStream(out, dt[cindex].getConstructor(), diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 3ebdad4db..abea75d50 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -35,7 +35,6 @@ namespace prop { class CnfProof; -typedef std::unordered_map SatVarToExpr; typedef std::unordered_map NodeToNode; typedef std::unordered_set ClauseIdSet; diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 17d2f4d2f..decf83634 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -41,6 +41,7 @@ class CnfStream; class CDCLTSatSolverInterface; class ProofCnfStream; class PropPfManager; +class TheoryProxy; /** * PropEngine is the abstraction of a Sat Solver, providing methods for diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 5fcb57beb..38a424731 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -183,7 +183,7 @@ void Assertions::addFormula( if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores()) { - ProofManager::currentPM()->addCoreAssertion(n.toExpr()); + ProofManager::currentPM()->addCoreAssertion(n); } } else @@ -228,7 +228,7 @@ void Assertions::ensureBoolean(const Node& n) ss << "Expected Boolean type\n" << "The assertion : " << n << "\n" << "Its type : " << type; - throw TypeCheckingException(n.toExpr(), ss.str()); + throw TypeCheckingExceptionPrivate(n, ss.str()); } } diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 20c5d3e17..62779dbba 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -143,7 +143,7 @@ TrustNode ExpandDefs::expandDefinitions( else { // We always check if this operator corresponds to a defined function. - doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr()); + doExpand = d_smt.isDefinedFunction(n.getOperator()); } } // the premise of the proof of expansion (if we are expanding a definition @@ -171,8 +171,8 @@ TrustNode ExpandDefs::expandDefinitions( SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func); if (i == dfuns->end()) { - throw TypeCheckingException( - n.toExpr(), + throw TypeCheckingExceptionPrivate( + n, std::string("Undefined function: `") + func.toString() + "'"); } DefinedFunction def = (*i).second; diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 8df36a9fe..616014992 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -57,7 +57,7 @@ bool InterpolationSolver::getInterpol(const Node& conj, { if (options::checkInterpols()) { - checkInterpol(interpol.toExpr(), axioms, conj); + checkInterpol(interpol, axioms, conj); } return true; } @@ -83,8 +83,8 @@ void InterpolationSolver::checkInterpol(Node interpol, { if (j == 1) { - Trace("check-interpol") << "SmtEngine::checkInterpol: conjecture is " - << conj.toExpr() << std::endl; + Trace("check-interpol") + << "SmtEngine::checkInterpol: conjecture is " << conj << std::endl; } Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j << ": make new SMT engine" << std::endl; diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index fafd733d6..f69bd1502 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -23,6 +23,9 @@ #include "util/result.h" namespace CVC4 { + +class SmtEngine; + namespace smt { /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d89b30c87..94e53a093 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -607,7 +607,7 @@ void SmtEngine::debugCheckFormals(const std::vector& formals, Node func) << "definition of function " << func << ", formal\n" << " " << *i << "\n" << "has kind " << (*i).getKind(); - throw TypeCheckingException(func.toExpr(), ss.str()); + throw TypeCheckingExceptionPrivate(func, ss.str()); } } } @@ -632,7 +632,7 @@ void SmtEngine::debugCheckFunctionBody(Node formula, << "Declared type : " << rangeType << "\n" << "The body : " << formula << "\n" << "Body type : " << formulaType; - throw TypeCheckingException(func.toExpr(), ss.str()); + throw TypeCheckingExceptionPrivate(func, ss.str()); } } else { if(! formulaType.isComparableTo(funcType)) { @@ -642,7 +642,7 @@ void SmtEngine::debugCheckFunctionBody(Node formula, << "Declared type : " << funcType << "\n" << "The definition : " << formula << "\n" << "Definition type: " << formulaType; - throw TypeCheckingException(func.toExpr(), ss.str()); + throw TypeCheckingExceptionPrivate(func, ss.str()); } } } diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index d0e28b221..58bc2f09f 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -277,7 +277,7 @@ struct RecordUpdateTypeRule { TypeNode recordType = n[0].getType(check); TypeNode newValue = n[1].getType(check); if (check) { - if (!recordType.toType().isRecord()) + if (!recordType.isRecord()) { throw TypeCheckingExceptionPrivate( n, "Record-update expression formed over non-record"); diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index 13904eecd..c9bc63308 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -147,7 +147,7 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb) else { NodeManager* nm = NodeManager::currentNM(); - unsigned cindex = DType::indexOf(a.getOperator().toExpr()); + unsigned cindex = DType::indexOf(a.getOperator()); TypeNode tn = a.getType(); const DType& dt = tn.getDType(); for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++) diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index c559f4c75..d20755e47 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -26,6 +26,9 @@ #include "util/result.h" namespace CVC4 { + +class SmtEngine; + namespace theory { namespace quantifiers { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 49c0f5f47..1e58a1f24 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -428,9 +428,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, } else if (type.isFloatingPoint()) { - FloatingPointType fp_type = static_cast(type.toType()); - FloatingPointSize fp_size(FloatingPointType(fp_type).getExponentSize(), - FloatingPointType(fp_type).getSignificandSize()); + FloatingPointSize fp_size(type.getFloatingPointExponentSize(), + type.getFloatingPointSignificandSize()); ops.push_back(nm->mkConst(FloatingPoint::makeNaN(fp_size))); ops.push_back(nm->mkConst(FloatingPoint::makeInf(fp_size, true))); ops.push_back(nm->mkConst(FloatingPoint::makeInf(fp_size, false))); @@ -524,10 +523,8 @@ Node CegGrammarConstructor::createLambdaWithZeroArg( { NodeManager* nm = NodeManager::currentNM(); std::vector opLArgs; - std::vector opLArgsExpr; // get the builtin type opLArgs.push_back(nm->mkBoundVar(bArgType)); - opLArgsExpr.push_back(opLArgs.back().toExpr()); // build zarg Node zarg; Assert(bArgType.isReal() || bArgType.isBitVector()); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 6dda91fe7..c72ad20d9 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -111,7 +111,7 @@ void SygusGrammarNorm::TypeObject::initializeDatatype( * Int, etc) */ TypeNode sygusType = dt.getSygusType(); d_sdt.initializeDatatype(sygusType, - sygus_norm->d_sygus_vars.toExpr(), + sygus_norm->d_sygus_vars, dt.getSygusAllowConst(), dt.getSygusAllowAll()); Trace("sygus-grammar-normalize") diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index 04ce91fa9..66e322efe 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -36,11 +36,10 @@ void SynthConjectureProcessFun::init(Node f) // initialize the arguments std::unordered_map type_to_init_deq_id; - std::vector argTypes = - static_cast(f.getType().toType()).getArgTypes(); + std::vector argTypes = f.getType().getArgTypes(); for (unsigned j = 0; j < argTypes.size(); j++) { - TypeNode atn = TypeNode::fromType(argTypes[j]); + TypeNode atn = argTypes[j]; std::stringstream ss; ss << "a" << j; Node k = NodeManager::currentNM()->mkBoundVar(ss.str(), atn); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index dc864fbd8..3a9864ea9 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -576,8 +576,7 @@ bool SynthConjecture::doCheck(std::vector& lems) if (!query.isConst() || query.getConst()) { Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; - Result r = - checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs); + Result r = checkWithSubsolver(query, d_ce_sk_vars, d_ce_sk_var_mvs); Trace("sygus-engine") << " ...got " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::SAT) { diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index ec9c8fa20..9f7875e18 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -19,6 +19,8 @@ #ifndef CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H #define CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H +#include + #include "theory/sets/normal_form.h" namespace CVC4 { diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index 61bef82f1..5def8ec4b 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -177,7 +177,7 @@ SeqEnumLen::SeqEnumLen(TypeNode tn, d_elementEnumerator.reset( new TypeEnumerator(d_type.getSequenceElementType(), tep)); // ensure non-empty element domain - d_elementDomain.push_back((**d_elementEnumerator).toExpr()); + d_elementDomain.push_back((**d_elementEnumerator)); ++(*d_elementEnumerator); mkCurr(); } @@ -195,7 +195,7 @@ bool SeqEnumLen::increment() { // yet to establish domain Assert(d_elementEnumerator != nullptr); - d_elementDomain.push_back((**d_elementEnumerator).toExpr()); + d_elementDomain.push_back((**d_elementEnumerator)); ++(*d_elementEnumerator); } // the current cardinality is the domain size of the element diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index 425bb453b..02d3e7f41 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -159,7 +159,7 @@ class SeqEnumLen : public SEnumLen /** an enumerator for the elements' type */ std::unique_ptr d_elementEnumerator; /** The domain */ - std::vector d_elementDomain; + std::vector d_elementDomain; /** Make the current term from d_data */ void mkCurr(); }; diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 3eb0ed629..1c5419977 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1076,7 +1076,7 @@ void EqualityEngine::buildEqConclusion(EqualityNodeId id1, << id2 << "} " << d_nodes[id2] << "\n"; // if has at least as many children as the minimal // number of children of the n-ary kind, build the node - if (numChildren >= ExprManager::minArity(k1)) + if (numChildren >= kind::metakind::getMaxArityForKind(k1)) { std::vector children; for (unsigned j = 0; j < numChildren; ++j) diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 926c0b0f9..aad1ad63d 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -19,6 +19,8 @@ #ifndef CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H #define CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H +#include + namespace CVC4 { namespace theory { namespace uf { diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index 442a57e34..7b42d6a76 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -29,8 +29,6 @@ #include #include "api/cvc4cpp.h" -#include "expr/expr.h" -#include "expr/expr_iomanip.h" #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index c008018b2..223028d4c 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -19,7 +19,6 @@ #include #include "api/cvc4cpp.h" -#include "expr/expr_manager.h" #include "options/options.h" #include "options/set_language.h" #include "parser/parser.h" diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp index b536fb932..3c1651155 100644 --- a/test/unit/expr/node_black.cpp +++ b/test/unit/expr/node_black.cpp @@ -22,7 +22,6 @@ #include "api/cvc4cpp.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" -#include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" diff --git a/test/unit/expr/node_traversal_black.cpp b/test/unit/expr/node_traversal_black.cpp index 1c18abdb5..e443ff685 100644 --- a/test/unit/expr/node_traversal_black.cpp +++ b/test/unit/expr/node_traversal_black.cpp @@ -19,7 +19,6 @@ #include #include -#include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" diff --git a/test/unit/expr/symbol_table_black.cpp b/test/unit/expr/symbol_table_black.cpp index 68b822bac..10fb52f6d 100644 --- a/test/unit/expr/symbol_table_black.cpp +++ b/test/unit/expr/symbol_table_black.cpp @@ -20,10 +20,8 @@ #include "base/check.h" #include "base/exception.h" #include "context/context.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" +#include "expr/kind.h" #include "expr/symbol_table.h" -#include "expr/type.h" #include "test_api.h" namespace CVC4 { diff --git a/test/unit/expr/type_cardinality_black.cpp b/test/unit/expr/type_cardinality_black.cpp index 08e863bc4..58024fa53 100644 --- a/test/unit/expr/type_cardinality_black.cpp +++ b/test/unit/expr/type_cardinality_black.cpp @@ -18,7 +18,6 @@ #include "expr/kind.h" #include "expr/node_manager.h" -#include "expr/type.h" #include "test_node.h" #include "util/cardinality.h" diff --git a/test/unit/expr/type_node_white.cpp b/test/unit/expr/type_node_white.cpp index 4412ec95a..f364e40fc 100644 --- a/test/unit/expr/type_node_white.cpp +++ b/test/unit/expr/type_node_white.cpp @@ -18,8 +18,6 @@ #include #include -#include "expr/expr.h" -#include "expr/expr_manager.h" #include "expr/node_manager.h" #include "expr/type_node.h" #include "smt/smt_engine.h" diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index b35f07f18..c600e3477 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -18,7 +18,6 @@ #include #include "api/cvc4cpp.h" -#include "expr/expr_manager.h" #include "expr/symbol_manager.h" #include "main/interactive_shell.h" #include "options/base_options.h" diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index ece6168e9..87556d53d 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -19,8 +19,6 @@ #include "api/cvc4cpp.h" #include "base/output.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" #include "expr/symbol_manager.h" #include "options/base_options.h" #include "options/language.h" diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 978914d3e..cf343f006 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -28,7 +28,7 @@ class TestNode : public TestInternal protected: void SetUp() override { - d_nodeManager.reset(new NodeManager(nullptr)); + d_nodeManager.reset(new NodeManager()); d_scope.reset(new NodeManagerScope(d_nodeManager.get())); d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType())); d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2))); diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 718a9d2b6..e55c00e65 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -41,7 +41,7 @@ class TestSmt : public TestInternal protected: void SetUp() override { - d_nodeManager.reset(new NodeManager(nullptr)); + d_nodeManager.reset(new NodeManager()); d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); d_smtEngine->finishInit(); @@ -57,7 +57,7 @@ class TestSmtNoFinishInit : public TestInternal protected: void SetUp() override { - d_nodeManager.reset(new NodeManager(nullptr)); + d_nodeManager.reset(new NodeManager()); d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); } diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 6952fb320..1447670f3 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -86,7 +86,7 @@ TEST_F(TestTheoryWhiteBv, mkUmulo) kind::DISTINCT, mkExtract(mul, 2 * w - 1, w), mkZero(w)); Node rhs = mkUmulo(x, y); Node eq = d_nodeManager->mkNode(kind::DISTINCT, lhs, rhs); - d_smtEngine->assertFormula(eq.toExpr()); + d_smtEngine->assertFormula(eq); Result res = d_smtEngine->checkSat(); ASSERT_EQ(res.isSat(), Result::UNSAT); d_smtEngine->pop(); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 54b4ce55b..7b6a73d2c 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -88,7 +88,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit } Node body = d_nodeManager->mkNode(k, x, d_t); Node scr = d_nodeManager->mkNode(EXISTS, d_bvarlist, body); - Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr(); + Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); Result res = d_smtEngine->checkSat(a); ASSERT_EQ(res.d_sat, Result::UNSAT); } @@ -117,14 +117,14 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit litk, d_nodeManager->mkNode(k, d_s, d_x), d_t); Node scr = d_nodeManager->mkNode(EXISTS, d_bvarlist, pol ? body : body.notNode()); - Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr(); + Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); Result res = d_smtEngine->checkSat(a); if (res.d_sat == Result::SAT) { std::cout << std::endl; - std::cout << "s " << d_smtEngine->getValue(d_s.toExpr()) << std::endl; - std::cout << "t " << d_smtEngine->getValue(d_t.toExpr()) << std::endl; - std::cout << "x " << d_smtEngine->getValue(d_x.toExpr()) << std::endl; + std::cout << "s " << d_smtEngine->getValue(d_s) << std::endl; + std::cout << "t " << d_smtEngine->getValue(d_t) << std::endl; + std::cout << "x " << d_smtEngine->getValue(d_x) << std::endl; } ASSERT_EQ(res.d_sat, Result::UNSAT); } @@ -173,17 +173,17 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit Node bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {x}); Node scr = d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode()); - Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr(); + Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); Result res = d_smtEngine->checkSat(a); if (res.d_sat == Result::SAT) { std::cout << std::endl; if (!s1.isNull()) - std::cout << "s1 " << d_smtEngine->getValue(s1.toExpr()) << std::endl; + std::cout << "s1 " << d_smtEngine->getValue(s1) << std::endl; if (!s2.isNull()) - std::cout << "s2 " << d_smtEngine->getValue(s2.toExpr()) << std::endl; - std::cout << "t " << d_smtEngine->getValue(t.toExpr()) << std::endl; - std::cout << "x " << d_smtEngine->getValue(x.toExpr()) << std::endl; + std::cout << "s2 " << d_smtEngine->getValue(s2) << std::endl; + std::cout << "t " << d_smtEngine->getValue(t) << std::endl; + std::cout << "x " << d_smtEngine->getValue(x) << std::endl; } ASSERT_TRUE(res.d_sat == Result::UNSAT); } @@ -213,13 +213,13 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit Node bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {x}); Node scr = d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode()); - Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr(); + Node a = d_nodeManager->mkNode(DISTINCT, scl, scr); Result res = d_smtEngine->checkSat(a); if (res.d_sat == Result::SAT) { std::cout << std::endl; - std::cout << "t " << d_smtEngine->getValue(t.toExpr()) << std::endl; - std::cout << "x " << d_smtEngine->getValue(x.toExpr()) << std::endl; + std::cout << "t " << d_smtEngine->getValue(t) << std::endl; + std::cout << "x " << d_smtEngine->getValue(x) << std::endl; } ASSERT_TRUE(res.d_sat == Result::UNSAT); } diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 693bc0423..540fca6f2 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -15,8 +15,6 @@ **/ #include "expr/array_store_all.h" -#include "expr/expr.h" -#include "expr/type.h" #include "test_smt.h" namespace CVC4 { diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 18dc479be..ef24d870d 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -16,10 +16,8 @@ #include -#include "api/cvc4cpp.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" -#include "expr/expr.h" #include "expr/type_node.h" #include "test_smt.h" -- 2.30.2