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
#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"
/* 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))
{
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();
class SygusConstraintCommand;
class SygusInvConstraintCommand;
class SynthFunCommand;
-class Type;
class TypeNode;
class Options;
class QueryCommand;
* @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);
/**
emptybag.h
expr_iomanip.cpp
expr_iomanip.h
- expr_manager_scope.h
kind_map.h
lazy_proof.cpp
lazy_proof.h
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
kind.h
metakind.cpp
metakind.h
- expr.cpp
- expr.h
- expr_manager.cpp
- expr_manager.h
type_checker.cpp
type_properties.h
)
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
kind.h
metakind.cpp
metakind.h
- expr.cpp
- expr.h
- expr_manager.cpp
- expr_manager.h
type_checker.cpp
type_properties.h
)
+++ /dev/null
-/********************* */
-/*! \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 <code>NodeManagerScope</code> with the underlying
- * <code>NodeManager</code> of a given <code>Expr</code> or
- * <code>ExprManager</code>. The <code>NodeManagerScope</code> is
- * destroyed when the <code>ExprManagerScope</code> is destroyed. See
- * <code>NodeManagerScope</code> 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 */
+++ /dev/null
-/********************* */
-/*! \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 <map>
-
-#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<TypeConstant>() \
- : 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<Expr>& 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<Node> nodes;
- vector<Expr>::const_iterator it = children.begin();
- vector<Expr>::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<Expr>& 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<Node> nodes;
- nodes.push_back(child1.getNode());
-
- vector<Expr>::const_iterator it = otherChildren.begin();
- vector<Expr>::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<Expr>& 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<Node> nodes;
- vector<Expr>::const_iterator it = children.begin();
- vector<Expr>::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<Type>& argTypes, Type range) {
- NodeManagerScope nms(d_nodeManager);
- Assert(argTypes.size() >= 1);
- std::vector<TypeNode> 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<Type>& sorts) {
- NodeManagerScope nms(d_nodeManager);
- Assert(sorts.size() >= 2);
- std::vector<TypeNode> 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<Type>& sorts) {
- NodeManagerScope nms(d_nodeManager);
- Assert(sorts.size() >= 1);
- std::vector<TypeNode> 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<Type>& types) {
- NodeManagerScope nms(d_nodeManager);
- std::vector<TypeNode> 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<Expr>& 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<Expr>::const_iterator it = children.begin() ;
- std::vector<Expr>::const_iterator end = children.end() ;
-
- /* The new top-level children and the children of each sub node */
- std::vector<Expr> newChildren;
- std::vector<Node> subChildren;
-
- while( it != end && numChildren > max ) {
- /* Grab the next max children and make a node for them. */
- for( std::vector<Expr>::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<Expr>& 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<Expr>& 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<Expr>& 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<Expr> 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<TypeConstant>());
- } else if(n.getKind() == kind::BITVECTOR_TYPE) {
- return to->mkBitVectorType(n.getConst<BitVectorSize>());
- }
- else if (n.getKind() == kind::FLOATINGPOINT_TYPE)
- {
- return to->mkFloatingPointType(n.getConst<FloatingPointSize>());
- }
- 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 */
+++ /dev/null
-/********************* */
-/*! \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 <vector>
-
-#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<Expr>& 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<Expr>& 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<Expr>& children);
-
- /** Create a constant of type T */
- template <class T>
- Expr mkConst(const T&);
-
- /**
- * Create an Expr by applying an associative operator to the children.
- * If <code>children.size()</code> is greater than the max arity for
- * <code>kind</code>, then the expression will be broken up into
- * suitably-sized chunks, taking advantage of the associativity of
- * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
- * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
- * <code>(FOO (FOO a b) c)</code> or <code>(FOO a (FOO b c))</code>.
- * 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<Expr>& 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<Expr>& 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<Expr>& 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<Expr>& 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<CVC4::Kind>() 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.
- * <code>argTypes</code> must have at least one element.
- */
- FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
-
- /**
- * Make a function type with input types from
- * <code>sorts[0..sorts.size()-2]</code> and result type
- * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
- * at least 2 elements.
- */
- FunctionType mkFunctionType(const std::vector<Type>& sorts);
-
- /**
- * Make a predicate type with input types from
- * <code>sorts</code>. The result with be a function type with range
- * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
- * element.
- */
- FunctionType mkPredicateType(const std::vector<Type>& sorts);
-
- /**
- * Make a symbolic expressiontype with types from
- * <code>types[0..types.size()-1]</code>. <code>types</code> may
- * have any number of elements.
- */
- SExprType mkSExprType(const std::vector<Type>& 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 */
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-#include <iterator>
-#include <utility>
-#include <vector>
-
-#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<Expr>& container)
-{
- container_to_stream(out, container);
- return out;
-}
-
-std::ostream& operator<<(std::ostream& out, const std::set<Expr>& container)
-{
- container_to_stream(out, container);
- return out;
-}
-
-std::ostream& operator<<(
- std::ostream& out,
- const std::unordered_set<Expr, ExprHashFunction>& container)
-{
- container_to_stream(out, container);
- return out;
-}
-
-template <typename V>
-std::ostream& operator<<(std::ostream& out, const std::map<Expr, V>& container)
-{
- container_to_stream(out, container);
- return out;
-}
-
-template <typename V>
-std::ostream& operator<<(
- std::ostream& out,
- const std::unordered_map<Expr, V, ExprHashFunction>& 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<false>, NodeTemplate<true>, 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<Node> 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<Node>::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 Iterator>
-class NodeIteratorAdaptor : public std::iterator<std::input_iterator_tag, Node> {
- 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 <class Iterator>
-static inline NodeIteratorAdaptor<Iterator> mkNodeIteratorAdaptor(Iterator i) {
- return NodeIteratorAdaptor<Iterator>(i);
-}
-
-Expr Expr::substitute(const std::vector<Expr> exes,
- const std::vector<Expr>& 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 Iterator>
-class NodePairIteratorAdaptor : public std::iterator<std::input_iterator_tag, pair<Node, Node> > {
- 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<Node, Node> operator*() { return make_pair(Node::fromExpr((*d_iterator).first), Node::fromExpr((*d_iterator).second)); }
-};/* class NodePairIteratorAdaptor */
-
-template <class Iterator>
-static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterator i) {
- return NodePairIteratorAdaptor<Iterator>(i);
-}
-
-Expr Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> 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<Node::iterator*>(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<Node::iterator*>(d_iterator);
- }
- d_exprManager = it.d_exprManager;
- ExprManagerScope ems(*d_exprManager);
- d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
- return *this;
-}
-Expr::const_iterator::~const_iterator() {
- if(d_iterator != NULL) {
- ExprManagerScope ems(*d_exprManager);
- delete reinterpret_cast<Node::iterator*>(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<Node::iterator*>(d_iterator) ==
- *reinterpret_cast<Node::iterator*>(it.d_iterator);
-}
-Expr::const_iterator& Expr::const_iterator::operator++() {
- Assert(d_iterator != NULL);
- ExprManagerScope ems(*d_exprManager);
- ++*reinterpret_cast<Node::iterator*>(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<Node::iterator*>(d_iterator);
- return it;
-}
-Expr Expr::const_iterator::operator*() const {
- Assert(d_iterator != NULL);
- ExprManagerScope ems(*d_exprManager);
- return (**reinterpret_cast<Node::iterator*>(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<ArrayStoreAll>();
- 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 */
+++ /dev/null
-/********************* */
-/*! \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 <iosfwd>
-#include <iterator>
-#include <string>
-#include <map>
-#include <set>
-#include <unordered_map>
-#include <unordered_set>
-
-#include "base/exception.h"
-#include "options/language.h"
-#include "util/hash.h"
-
-namespace CVC4 {
-
-// The internal expression representation
-template <bool ref_count>
-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<Expr>& 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<Expr>& 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<Expr, ExprHashFunction>& 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 <typename V>
-std::ostream& operator<<(std::ostream& out,
- const std::map<Expr, V>& 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 <typename V>
-std::ostream& operator<<(
- std::ostream& out,
- const std::unordered_map<Expr, V, ExprHashFunction>& 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<true>* 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<true>* 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<Expr> getChildren() const {
- return std::vector<Expr>(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<std::input_iterator_tag, Expr> {
- 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<Expr> exes,
- const std::vector<Expr>& replacements) const;
-
- /**
- * Substitute pairs of (ex,replacement) from the given map.
- */
- Expr substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> 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 <class T>
- 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<true> getNode() const;
-
- /**
- * Returns the actual internal node as a TNode.
- * @return the internal node
- */
- NodeTemplate<false> getTNode() const;
- template <bool ref_count> 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 */
#define CVC4__NODE_H
#include <iostream>
+#include <map>
#include <string>
#include <unordered_map>
#include <unordered_set>
#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"
*/
friend class expr::NodeValue;
- friend class expr::ExportPrivate;
-
/** A convenient null-valued encapsulated pointer */
static NodeTemplate s_null;
*/
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.
// 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
}
}
-template <bool ref_count>
-NodeTemplate<ref_count>::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 <bool ref_count>
NodeTemplate<ref_count>::~NodeTemplate() {
Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
}
}
-template <bool ref_count>
-inline Expr NodeTemplate<ref_count>::toExpr() const {
- assertTNodeNotExpired();
- return NodeManager::currentNM()->toExpr(*this);
-}
-
-// intentionally not defined for TNode
-template <>
-inline Node NodeTemplate<true>::fromExpr(const Expr& e) {
- return NodeManager::fromExpr(e);
-}
-
#ifdef CVC4_DEBUG
/**
* Pretty printer for use within gdb. This is not intended to be used
// attribute that stores the canonical bound variable list for function types
typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> 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)
//#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
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 <unsigned nchild_thresh>
friend class NodeBuilder;
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"
// `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) {
Node* mkVarPtr(const TypeNode& type);
public:
-
- explicit NodeManager(ExprManager* exprManager);
+ explicit NodeManager();
~NodeManager();
/** The node manager in the current public-facing CVC4 library context */
*/
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);
* public-interface calls into the CVC4 library, where CVC4's notion
* of the "current" <code>NodeManager</code> should be set to match
* the calling context. See, for example, the implementations of
- * public calls in the <code>ExprManager</code> and
- * <code>SmtEngine</code> classes.
+ * public calls in the <code>SmtEngine</code> class.
*
* The client must be careful to create and destroy
* <code>NodeManagerScope</code> objects in a well-nested manner (such
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";
}
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
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-#include <sstream>
-#include <string>
-#include <vector>
-
-#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<Type>& types,
- const std::vector<Type>& replacements) const {
- NodeManagerScope nms(d_nodeManager);
-
- vector<TypeNode> typesNodes, replacementsNodes;
-
- for(vector<Type>::const_iterator i = types.begin(),
- iend = types.end();
- i != iend;
- ++i) {
- typesNodes.push_back(*(*i).d_typeNode);
- }
-
- for(vector<Type>::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<Type> FunctionType::getArgTypes() const {
- NodeManagerScope nms(d_nodeManager);
- vector<Type> args;
- vector<TypeNode> argNodes = d_typeNode->getArgTypes();
- vector<TypeNode>::iterator it = argNodes.begin();
- vector<TypeNode>::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<Type> SExprType::getTypes() const {
- NodeManagerScope nms(d_nodeManager);
- vector<Type> types;
- vector<TypeNode> typeNodes = d_typeNode->getSExprTypes();
- vector<TypeNode>::iterator it = typeNodes.begin();
- vector<TypeNode>::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<Type> SortType::getParamTypes() const {
- vector<Type> 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<Type>& params) const {
- NodeManagerScope nms(d_nodeManager);
- vector<TypeNode> paramsNodes;
- for(vector<Type>::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<Type> ConstructorType::getArgTypes() const {
- NodeManagerScope nms(d_nodeManager);
- vector<Type> args;
- vector<TypeNode> argNodes = d_typeNode->getArgTypes();
- vector<TypeNode>::iterator it = argNodes.begin();
- vector<TypeNode>::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<Type> DatatypeType::getParamTypes() const {
- NodeManagerScope nms(d_nodeManager);
- vector<Type> params;
- vector<TypeNode> paramNodes = d_typeNode->getParamTypes();
- vector<TypeNode>::iterator it = paramNodes.begin();
- vector<TypeNode>::iterator it_end = paramNodes.end();
- for(; it != it_end; ++it) {
- params.push_back(makeType(*it));
- }
- return params;
-}
-
-DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const {
- NodeManagerScope nms(d_nodeManager);
- TypeNode cons = d_nodeManager->mkTypeConst( (*d_typeNode)[0].getConst<DatatypeIndexConstant>() );
- vector<TypeNode> paramsNodes;
- paramsNodes.push_back( cons );
- for(vector<Type>::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<Type> DatatypeType::getTupleTypes() const {
- NodeManagerScope nms(d_nodeManager);
- std::vector< TypeNode > vec = d_typeNode->getTupleTypes();
- std::vector< Type > vect;
- for( unsigned i=0; i<vec.size(); i++ ){
- vect.push_back( vec[i].toType() );
- }
- return vect;
-}
-
-DatatypeType SelectorType::getDomain() const {
- return DatatypeType(makeType((*d_typeNode)[0]));
-}
-
-Type SelectorType::getRangeType() const {
- return makeType((*d_typeNode)[1]);
-}
-
-DatatypeType TesterType::getDomain() const {
- return DatatypeType(makeType((*d_typeNode)[0]));
-}
-
-BooleanType TesterType::getRangeType() const {
- return BooleanType(makeType(d_nodeManager->booleanType()));
-}
-
-/* - 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 */
+++ /dev/null
-/********************* */
-/*! \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 <climits>
-#include <string>
-#include <vector>
-
-#include "util/cardinality.h"
-
-namespace CVC4 {
-
-class NodeManager;
-class CVC4_PUBLIC ExprManager;
-class Expr;
-class TypeNode;
-struct CVC4_PUBLIC ExprManagerMapCollection;
-
-class SmtEngine;
-
-template <bool ref_count>
-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<Type>& types,
- const std::vector<Type>& 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<Type> 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<Type> 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<Type> 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<Type>& 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<Type> 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<Type>& params) const;
-
- /** Get the length of a tuple type */
- size_t getTupleLength() const;
-
- /** Get the constituent types of a tuple type */
- std::vector<Type> 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<Type> 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 */
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.
*
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 {
+++ /dev/null
-/********************* */
-/*! \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 <unordered_map>
-
-#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<Expr, Expr, ExprHashFunction> d_variables;
-
- /**
- * A map Type -> Type, intended to be used for a mapping of types
- * between two ExprManagers.
- */
- std::unordered_map<Type, Type, TypeHashFunction> 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<uint64_t, uint64_t> VarMap;
-
-struct CVC4_PUBLIC ExprManagerMapCollection {
- VariableTypeMap d_typeMap;
- VarMap d_to;
- VarMap d_from;
-};/* struct ExprManagerMapCollection */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__VARIABLE_MAP_H */
#include <cvc4/base/configuration.h>
#include <cvc4/base/exception.h>
#include <cvc4/expr/datatype_index.h>
-#include <cvc4/expr/expr.h>
-#include <cvc4/expr/expr_manager.h>
#include <cvc4/options/options.h>
#include <cvc4/parser/parser.h>
#include <cvc4/parser/parser_builder.h>
*/
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
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;
}
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());
}
}
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;
}
}
else
{
- throw TypeCheckingException(
- v.toExpr(),
+ throw TypeCheckingExceptionPrivate(
+ v,
std::string("Cannot translate to Int: ") + v.toString());
}
}
{
// 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());
}
out << "TUPLE";
}
}
- else if (t.toType().isRecord())
+ else if (t.isRecord())
{
const DType& dt = t.getDType();
const DTypeConstructor& recCons = dt[0];
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;
}
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());
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 << ',';
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 << ',';
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 << ',';
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:
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(),
class CnfProof;
-typedef std::unordered_map<prop::SatVariable, Expr> SatVarToExpr;
typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
typedef std::unordered_set<ClauseId> ClauseIdSet;
class CDCLTSatSolverInterface;
class ProofCnfStream;
class PropPfManager;
+class TheoryProxy;
/**
* PropEngine is the abstraction of a Sat Solver, providing methods for
if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores()
|| options::checkUnsatCores())
{
- ProofManager::currentPM()->addCoreAssertion(n.toExpr());
+ ProofManager::currentPM()->addCoreAssertion(n);
}
}
else
ss << "Expected Boolean type\n"
<< "The assertion : " << n << "\n"
<< "Its type : " << type;
- throw TypeCheckingException(n.toExpr(), ss.str());
+ throw TypeCheckingExceptionPrivate(n, ss.str());
}
}
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
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;
{
if (options::checkInterpols())
{
- checkInterpol(interpol.toExpr(), axioms, conj);
+ checkInterpol(interpol, axioms, conj);
}
return true;
}
{
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;
#include "util/result.h"
namespace CVC4 {
+
+class SmtEngine;
+
namespace smt {
/**
<< "definition of function " << func << ", formal\n"
<< " " << *i << "\n"
<< "has kind " << (*i).getKind();
- throw TypeCheckingException(func.toExpr(), ss.str());
+ throw TypeCheckingExceptionPrivate(func, ss.str());
}
}
}
<< "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)) {
<< "Declared type : " << funcType << "\n"
<< "The definition : " << formula << "\n"
<< "Definition type: " << formulaType;
- throw TypeCheckingException(func.toExpr(), ss.str());
+ throw TypeCheckingExceptionPrivate(func, ss.str());
}
}
}
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");
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++)
#include "util/result.h"
namespace CVC4 {
+
+class SmtEngine;
+
namespace theory {
namespace quantifiers {
}
else if (type.isFloatingPoint())
{
- FloatingPointType fp_type = static_cast<FloatingPointType>(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)));
{
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> opLArgs;
- std::vector<Expr> 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());
* 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")
// initialize the arguments
std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>
type_to_init_deq_id;
- std::vector<Type> argTypes =
- static_cast<FunctionType>(f.getType().toType()).getArgTypes();
+ std::vector<TypeNode> 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);
if (!query.isConst() || query.getConst<bool>())
{
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)
{
#ifndef CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
#define CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+#include <climits>
+
#include "theory/sets/normal_form.h"
namespace CVC4 {
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();
}
{
// 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
/** an enumerator for the elements' type */
std::unique_ptr<TypeEnumerator> d_elementEnumerator;
/** The domain */
- std::vector<Expr> d_elementDomain;
+ std::vector<Node> d_elementDomain;
/** Make the current term from d_data */
void mkCurr();
};
<< 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<Node> children;
for (unsigned j = 0; j < numChildren; ++j)
#ifndef CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
#define CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
+#include <climits>
+
namespace CVC4 {
namespace theory {
namespace uf {
#include <string>
#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"
#include <sstream>
#include "api/cvc4cpp.h"
-#include "expr/expr_manager.h"
#include "options/options.h"
#include "options/set_language.h"
#include "parser/parser.h"
#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"
#include <string>
#include <vector>
-#include "expr/expr_manager.h"
#include "expr/node.h"
#include "expr/node_builder.h"
#include "expr/node_manager.h"
#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 {
#include "expr/kind.h"
#include "expr/node_manager.h"
-#include "expr/type.h"
#include "test_node.h"
#include "util/cardinality.h"
#include <sstream>
#include <string>
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
#include "expr/node_manager.h"
#include "expr/type_node.h"
#include "smt/smt_engine.h"
#include <vector>
#include "api/cvc4cpp.h"
-#include "expr/expr_manager.h"
#include "expr/symbol_manager.h"
#include "main/interactive_shell.h"
#include "options/base_options.h"
#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"
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)));
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();
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()));
}
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();
}
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);
}
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);
}
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);
}
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);
}
**/
#include "expr/array_store_all.h"
-#include "expr/expr.h"
-#include "expr/type.h"
#include "test_smt.h"
namespace CVC4 {
#include <sstream>
-#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"
projects / cvc5.git / commitdiff