/*! \file node_manager.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic
+ ** Morgan Deters, Christopher L. Conway, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 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
**
virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {}
virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort,
uint32_t flags) {}
- virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes,
+ virtual void nmNotifyNewDatatypes(const std::vector<TypeNode>& datatypes,
uint32_t flags)
{
}
friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags);
friend Expr ExprManager::mkVar(Type, uint32_t flags);
- // friend so it can access NodeManager's d_listeners and notify clients
- friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
- std::vector<Datatype>&, std::set<Type>&, uint32_t);
-
/** Predicate for use with STL algorithms */
struct NodeValueReferenceCountNonZero {
bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
static thread_local NodeManager* s_current;
- Options* d_options;
StatisticsRegistry* d_statisticsRegistry;
- ResourceManager* d_resourceManager;
-
/** The skolem manager */
std::shared_ptr<SkolemManager> d_skManager;
- /**
- * A list of registrations on d_options to that call into d_resourceManager.
- * These must be garbage collected before d_options and d_resourceManager.
- */
- ListenerRegistrationList* d_registrations;
-
NodeValuePool d_nodeValuePool;
size_t next_id;
*/
std::vector<NodeManagerListener*> d_listeners;
- /** A list of datatypes owned by this node manager. */
- std::vector<std::shared_ptr<DType> > d_ownedDTypes;
+ /** A list of datatypes registered by its corresponding expr manager.
+ * !!! this member should be deleted when the Expr-layer is deleted.
+ */
+ std::vector<std::shared_ptr<DType> > d_registeredDTypes;
+ /** A list of datatypes owned by this node manager */
+ std::vector<std::unique_ptr<DType> > d_ownedDTypes;
/**
* A map of tuple and record types to their corresponding datatype.
/** Create a variable with the given type. */
Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
-public:
+
+ public:
explicit NodeManager(ExprManager* exprManager);
- explicit NodeManager(ExprManager* exprManager, const Options& options);
~NodeManager();
/** The node manager in the current public-facing CVC4 library context */
static NodeManager* currentNM() { return s_current; }
- /** The resource manager associated with the current node manager */
- static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; }
-
- /** Get this node manager's options (const version) */
- const Options& getOptions() const {
- return *d_options;
- }
-
- /** Get this node manager's options (non-const version) */
- Options& getOptions() {
- return *d_options;
- }
-
- /** Get this node manager's resource manager */
- ResourceManager* getResourceManager() { return d_resourceManager; }
/** Get this node manager's skolem manager */
SkolemManager* getSkolemManager() { return d_skManager.get(); }
Assert(elt != d_listeners.end()) << "listener not subscribed";
d_listeners.erase(elt);
}
-
- /** register datatype */
+
+ /** register that datatype dt was constructed by the expression manager
+ * !!! this interface should be deleted when the Expr-layer is deleted.
+ */
size_t registerDatatype(std::shared_ptr<DType> dt);
/**
* Return the datatype at the given index owned by this class. Type nodes are
* would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant
* which is used as an index to retrieve the DType via this call.
*/
- const DType& getDTypeForIndex(unsigned index) const;
+ const DType& getDTypeForIndex(size_t index) const;
/** Get a Kind from an operator expression */
static inline Kind operatorToKind(TNode n);
template <bool ref_count>
Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
+ /**
+ * Create an AND node with arbitrary number of children. This returns the
+ * true node if children is empty, or the single node in children if
+ * it contains only one node.
+ *
+ * We define construction of AND as a special case here since it is widely
+ * used for e.g. constructing explanations.
+ */
+ template <bool ref_count>
+ Node mkAnd(const std::vector<NodeTemplate<ref_count> >& children);
+
+ /**
+ * Create an OR node with arbitrary number of children. This returns the
+ * false node if children is empty, or the single node in children if
+ * it contains only one node.
+ *
+ * We define construction of OR as a special case here since it is widely
+ * used for e.g. constructing explanations or lemmas.
+ */
+ template <bool ref_count>
+ Node mkOr(const std::vector<NodeTemplate<ref_count> >& children);
+
/** Create a node (with no children) by operator. */
Node mkNode(TNode opNode);
Node* mkNodePtr(TNode opNode);
/** get the canonical bound variable list for function type tn */
Node getBoundVarListForFunctionType( TypeNode tn );
+ /**
+ * Create an Node 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.
+ */
+ Node mkAssociative(Kind kind, const std::vector<Node>& children);
+
+ /**
+ * Create an Node by applying an binary left-associative operator to the
+ * children. For example, mkLeftAssociative( f, { a, b, c } ) returns
+ * f( f( a, b ), c ).
+ */
+ Node mkLeftAssociative(Kind kind, const std::vector<Node>& children);
+ /**
+ * Create an Node by applying an binary right-associative operator to the
+ * children. For example, mkRightAssociative( f, { a, b, c } ) returns
+ * f( a, f( b, c ) ).
+ */
+ Node mkRightAssociative(Kind kind, const std::vector<Node>& 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.
+ */
+ Node mkChain(Kind kind, const std::vector<Node>& children);
+
/**
* Optional flags used to control behavior of NodeManager::mkSkolem().
* They should be composed with a bitwise OR (e.g.,
SKOLEM_DEFAULT = 0, /**< default behavior */
SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */
- SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */
- };
+ SKOLEM_IS_GLOBAL = 4, /**< global vars appear in models even after a pop */
+ SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
+ }; /* enum SkolemFlags */
+
/**
* Create a skolem constant with the given name, type, and comment.
*
/** Create a instantiation constant with the given type. */
Node mkInstConstant(const TypeNode& type);
-
+
/** Create a boolean term variable. */
Node mkBooleanTermVariable();
/** Make a new abstract value with the given type. */
Node mkAbstractValue(const TypeNode& type);
-
+
/** make unique (per Type,Kind) variable. */
Node mkNullaryOperator(const TypeNode& type, Kind k);
+ /**
+ * Create a singleton set from the given element n.
+ * @param t the element type of the returned set.
+ * Note that the type of n needs to be a subtype of t.
+ * @param n the single element in the singleton.
+ * @return a singleton set constructed from the element n.
+ */
+ Node mkSingleton(const TypeNode& t, const TNode n);
+
+ /**
+ * Create a bag from the given element n along with its multiplicity m.
+ * @param t the element type of the returned bag.
+ * Note that the type of n needs to be a subtype of t.
+ * @param n the element that is used to to construct the bag
+ * @param m the multiplicity of the element n
+ * @return a bag that contains m occurrences of n.
+ */
+ Node mkBag(const TypeNode& t, const TNode n, const TNode m);
+
/**
* Create a constant of type T. It will have the appropriate
* CONST_* kind defined for T.
const typename AttrKind::value_type& value);
/** Get the (singleton) type for Booleans. */
- inline TypeNode booleanType();
+ TypeNode booleanType();
/** Get the (singleton) type for integers. */
- inline TypeNode integerType();
+ TypeNode integerType();
/** Get the (singleton) type for reals. */
- inline TypeNode realType();
+ TypeNode realType();
/** Get the (singleton) type for strings. */
- inline TypeNode stringType();
+ TypeNode stringType();
/** Get the (singleton) type for RegExp. */
- inline TypeNode regExpType();
+ TypeNode regExpType();
/** Get the (singleton) type for rounding modes. */
- inline TypeNode roundingModeType();
+ TypeNode roundingModeType();
/** Get the bound var list type. */
- inline TypeNode boundVarListType();
+ TypeNode boundVarListType();
/** Get the instantiation pattern type. */
- inline TypeNode instPatternType();
+ TypeNode instPatternType();
/** Get the instantiation pattern type. */
- inline TypeNode instPatternListType();
+ TypeNode instPatternListType();
/**
* Get the (singleton) type for builtin operators (that is, the type
* of the Node returned from Node::getOperator() when the operator
* is built-in, like EQUAL). */
- inline TypeNode builtinOperatorType();
+ TypeNode builtinOperatorType();
/**
* Make a function type from domain to range.
/** Make the type of floating-point with <code>exp</code> bit exponent and
<code>sig</code> bit significand */
- inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
- inline TypeNode mkFloatingPointType(FloatingPointSize fs);
+ TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
+ TypeNode mkFloatingPointType(FloatingPointSize fs);
/** Make the type of bitvectors of size <code>size</code> */
- inline TypeNode mkBitVectorType(unsigned size);
+ TypeNode mkBitVectorType(unsigned size);
/** Make the type of arrays with the given parameterization */
inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
/** Make the type of set with the given parameterization */
inline TypeNode mkSetType(TypeNode elementType);
+ /** Make the type of bags with the given parameterization */
+ TypeNode mkBagType(TypeNode elementType);
+
/** Make the type of sequences with the given parameterization */
TypeNode mkSequenceType(TypeNode elementType);
- /** Make a type representing a constructor with the given parameterization */
- TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
+ /** Bits for use in mkDatatypeType() flags.
+ *
+ * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed
+ * out as a definition, for example, in models or during dumping.
+ */
+ enum
+ {
+ DATATYPE_FLAG_NONE = 0,
+ DATATYPE_FLAG_PLACEHOLDER = 1
+ }; /* enum */
+
+ /** Make a type representing the given datatype. */
+ TypeNode mkDatatypeType(DType& datatype, uint32_t flags = DATATYPE_FLAG_NONE);
+
+ /**
+ * Make a set of types representing the given datatypes, which may be
+ * mutually recursive.
+ */
+ std::vector<TypeNode> mkMutualDatatypeTypes(
+ const std::vector<DType>& datatypes, uint32_t flags = DATATYPE_FLAG_NONE);
+
+ /**
+ * Make a set of types representing the given datatypes, which may
+ * be mutually recursive. unresolvedTypes is a set of SortTypes
+ * that were used as placeholders in the Datatypes for the Datatypes
+ * of the same name. This is just a more complicated version of the
+ * above mkMutualDatatypeTypes() function, but is required to handle
+ * complex types.
+ *
+ * For example, unresolvedTypes might contain the single sort "list"
+ * (with that name reported from SortType::getName()). The
+ * datatypes list might have the single datatype
+ *
+ * DATATYPE
+ * list = cons(car:ARRAY INT OF list, cdr:list) | nil;
+ * END;
+ *
+ * To represent the Type of the array, the user had to create a
+ * placeholder type (an uninterpreted sort) to stand for "list" in
+ * the type of "car". It is this placeholder sort that should be
+ * passed in unresolvedTypes. If the datatype was of the simpler
+ * form:
+ *
+ * DATATYPE
+ * list = cons(car:list, cdr:list) | nil;
+ * END;
+ *
+ * then no complicated Type needs to be created, and the above,
+ * simpler form of mkMutualDatatypeTypes() is enough.
+ */
+ std::vector<TypeNode> mkMutualDatatypeTypes(
+ const std::vector<DType>& datatypes,
+ const std::set<TypeNode>& unresolvedTypes,
+ uint32_t flags = DATATYPE_FLAG_NONE);
+
/**
* Make a type representing a constructor with the given argument (subfield)
* types and return type range.
/**
* Convert a type node to a type.
*/
- inline Type toType(TypeNode tn);
+ inline Type toType(const TypeNode& tn);
/**
* Convert a type to a type node.
class NodeManagerScope {
/** The old NodeManager, to be restored on destruction. */
NodeManager* d_oldNodeManager;
- Options::OptionsScope d_optionsScope;
public:
-
- NodeManagerScope(NodeManager* nm)
- : d_oldNodeManager(NodeManager::s_current)
- , d_optionsScope(nm ? nm->d_options : NULL) {
- // 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;
- //Options::s_current = nm ? nm->d_options : NULL;
- Debug("current") << "node manager scope: "
- << NodeManager::s_current << "\n";
+ 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";
}
~NodeManagerScope() {
NodeManager::s_current = d_oldNodeManager;
- //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
Debug("current") << "node manager scope: "
<< "returning to " << NodeManager::s_current << "\n";
}
};/* class NodeManagerScope */
-/** Get the (singleton) type for booleans. */
-inline TypeNode NodeManager::booleanType() {
- return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
-}
-
-/** Get the (singleton) type for integers. */
-inline TypeNode NodeManager::integerType() {
- return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
-}
-
-/** Get the (singleton) type for reals. */
-inline TypeNode NodeManager::realType() {
- return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
-}
-
-/** Get the (singleton) type for strings. */
-inline TypeNode NodeManager::stringType() {
- return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
-}
-
-/** Get the (singleton) type for regexps. */
-inline TypeNode NodeManager::regExpType() {
- return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
-}
-
-/** Get the (singleton) type for rounding modes. */
-inline TypeNode NodeManager::roundingModeType() {
- return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE));
-}
-
-/** Get the bound var list type. */
-inline TypeNode NodeManager::boundVarListType() {
- return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternType() {
- return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternListType() {
- return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
-}
-
-/** Get the (singleton) type for builtin operators. */
-inline TypeNode NodeManager::builtinOperatorType() {
- return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
-}
-
inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
std::vector<TypeNode> typeNodes;
for (unsigned i = 0; i < types.size(); ++ i) {
return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
}
-inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
- return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
-}
-
-inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) {
- return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig)));
-}
-
-inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) {
- return TypeNode(mkTypeConst<FloatingPointSize>(fs));
-}
-
inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
TypeNode constituentType) {
CheckArgument(!indexType.isNull(), indexType,
return exprManager->getNodeManager();
}
-inline Type NodeManager::toType(TypeNode tn) {
+inline Type NodeManager::toType(const TypeNode& tn)
+{
return Type(this, new TypeNode(tn));
}
return nb.constructNode();
}
+template <bool ref_count>
+Node NodeManager::mkAnd(const std::vector<NodeTemplate<ref_count> >& children)
+{
+ if (children.empty())
+ {
+ return mkConst(true);
+ }
+ else if (children.size() == 1)
+ {
+ return children[0];
+ }
+ return mkNode(kind::AND, children);
+}
+
+template <bool ref_count>
+Node NodeManager::mkOr(const std::vector<NodeTemplate<ref_count> >& children)
+{
+ if (children.empty())
+ {
+ return mkConst(false);
+ }
+ else if (children.size() == 1)
+ {
+ return children[0];
+ }
+ return mkNode(kind::OR, children);
+}
+
template <bool ref_count>
inline Node* NodeManager::mkNodePtr(Kind kind,
const std::vector<NodeTemplate<ref_count> >&
template <class NodeClass, class T>
NodeClass NodeManager::mkConstInternal(const T& val) {
+ // This method indirectly calls `NodeValue::inc()`, which relies on having
+ // the correct `NodeManager` in scope.
+ NodeManagerScope nms(this);
// typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
NVStorage<1> nvStorage;
projects / cvc5.git / blobdiff