X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fexpr%2Fnode_manager.h;h=bbb076fbcd0df96a50d7ee691caeb8f1cd9c00c8;hb=f422a12f247b986ae8f6941e768ed75453fd1049;hp=f75ed95592a51ec4e061f3902bae545553ddf643;hpb=004678b6386e66cfa6a079215a3644efca59cdf7;p=cvc5.git diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f75ed9559..bbb076fbc 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,13 +1,13 @@ /********************* */ /*! \file node_manager.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Christopher L. Conway, Morgan Deters - ** Minor contributors (to current version): ACSYS, Tianyi Liang, Tim King + ** Top contributors (to current version): + ** Morgan Deters, Christopher L. Conway, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** 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 ** ** \brief A manager for Nodes ** @@ -25,24 +25,26 @@ #include "expr/expr.h" #include "expr/expr_manager.h" -#ifndef __CVC4__NODE_MANAGER_H -#define __CVC4__NODE_MANAGER_H +#ifndef CVC4__NODE_MANAGER_H +#define CVC4__NODE_MANAGER_H #include #include -#include +#include +#include "base/check.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" -#include "context/context.h" -#include "util/subrange_bound.h" -#include "util/tls.h" #include "options/options.h" namespace CVC4 { class StatisticsRegistry; +class ResourceManager; +class SkolemManager; + +class DType; namespace expr { namespace attr { @@ -58,15 +60,26 @@ namespace expr { * to NodeManager events via NodeManager::subscribeEvents(this). */ class NodeManagerListener { -public: - virtual ~NodeManagerListener() { } - virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { } - virtual void nmNotifyNewSortConstructor(TypeNode tn) { } - virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { } - virtual void nmNotifyNewDatatypes(const std::vector& datatypes) { } - virtual void nmNotifyNewVar(TNode n, uint32_t flags) { } - virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { } -};/* class NodeManagerListener */ + public: + virtual ~NodeManagerListener() {} + virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {} + virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {} + virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, + uint32_t flags) {} + virtual void nmNotifyNewDatatypes(const std::vector& datatypes, + uint32_t flags) + { + } + virtual void nmNotifyNewVar(TNode n, uint32_t flags) {} + virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, + uint32_t flags) {} + /** + * Notify a listener of a Node that's being GCed. If this function stores a + * reference + * to the Node somewhere, very bad things will happen. + */ + virtual void nmNotifyDeleteNode(TNode n) {} +}; /* class NodeManagerListener */ class NodeManager { template friend class CVC4::NodeBuilder; @@ -78,26 +91,25 @@ class NodeManager { 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 ExprManager::mkMutualDatatypeTypes(const std::vector&, const std::set&); - /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } }; - typedef __gnu_cxx::hash_set NodeValuePool; - typedef __gnu_cxx::hash_set ZombieSet; + typedef std::unordered_set NodeValuePool; + typedef std::unordered_set NodeValueIDSet; - static CVC4_THREADLOCAL(NodeManager*) s_current; + static thread_local NodeManager* s_current; - Options* d_options; StatisticsRegistry* d_statisticsRegistry; + /** The skolem manager */ + std::shared_ptr d_skManager; + NodeValuePool d_nodeValuePool; size_t next_id; @@ -113,10 +125,7 @@ class NodeManager { * contexts, like as a key in attribute tables), even though * normally it's an error to have a TNode to a node value with a * reference count of 0. Being "under deletion" also enables - * assertions that inc() is not called on it. (A poorly-behaving - * attribute cleanup function could otherwise create a "Node" that - * points to the node value that is in the process of being deleted, - * springing it back to life.) + * assertions that inc() is not called on it. */ expr::NodeValue* d_nodeUnderDeletion; @@ -133,7 +142,13 @@ class NodeManager { * we might like to delete nodes in least-recently-used order. But * we also need to avoid processing a zombie twice. */ - ZombieSet d_zombies; + NodeValueIDSet d_zombies; + + /** + * NodeValues with maxed out reference counts. These live as long as the + * NodeManager. They have a custom deallocation procedure at the very end. + */ + std::vector d_maxedOut; /** * A set of operator singletons (w.r.t. to this NodeManager @@ -145,15 +160,38 @@ class NodeManager { */ Node d_operators[kind::LAST_KIND]; + /** unique vars per (Kind,Type) */ + std::map< Kind, std::map< TypeNode, Node > > d_unique_vars; + /** * A list of subscribers for NodeManager events. */ std::vector d_listeners; + /** A list of datatypes registered by its corresponding expr manager. + * !!! this member should be deleted when the Expr-layer is deleted. + */ + std::vector > d_registeredDTypes; + /** A list of datatypes owned by this node manager */ + std::vector > d_ownedDTypes; + /** * A map of tuple and record types to their corresponding datatype. */ - std::hash_map d_tupleAndRecordTypes; + class TupleTypeCache { + public: + std::map< TypeNode, TupleTypeCache > d_children; + TypeNode d_data; + TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 ); + }; + class RecTypeCache { + public: + std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children; + TypeNode d_data; + TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 ); + }; + TupleTypeCache d_tt_cache; + RecTypeCache d_rt_cache; /** * Keep a count of all abstract values produced by this NodeManager. @@ -236,7 +274,18 @@ class NodeManager { Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") << std::endl; } - d_zombies.insert(nv);// FIXME multithreading + + // `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. + Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv); + + d_zombies.insert(nv); // FIXME multithreading if(safeToReclaimZombies()) { if(d_zombies.size() > 5000) { @@ -245,6 +294,19 @@ class NodeManager { } } + /** + * Register a NodeValue as having a maxed out reference count. This NodeValue + * will live as long as its containing NodeManager. + */ + inline void markRefCountMaxedOut(expr::NodeValue* nv) { + Assert(nv->HasMaximizedReferenceCount()); + if(Debug.isOn("gc")) { + Debug("gc") << "marking node value " << nv + << " [" << nv->d_id << "]: as maxed out" << std::endl; + } + d_maxedOut.push_back(nv); + } + /** * Reclaim all zombies. */ @@ -255,6 +317,14 @@ class NodeManager { */ bool safeToReclaimZombies() const; + /** + * Returns a reverse topological sort of a list of NodeValues. The NodeValues + * must be valid and have ids. The NodeValues are not modified (including ref + * counts). + */ + static std::vector TopologicalSort( + const std::vector& roots); + /** * This template gives a mechanism to stack-allocate a NodeValue * with enough space for N children (where N is a compile-time @@ -281,13 +351,15 @@ class NodeManager { * only be used once. For more details see the 4/27/2010 CVC4 * developer's meeting notes at: * - * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 + * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 */ // bool containsDecision(TNode); // is "atomic" // bool properlyContainsDecision(TNode); // all children are atomic // undefined private copy constructor (disallow copy) - NodeManager(const NodeManager&) CVC4_UNDEFINED; + NodeManager(const NodeManager&) = delete; + + NodeManager& operator=(const NodeManager&) = delete; void init(); @@ -305,46 +377,70 @@ class NodeManager { 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(context::Context* ctxt, ExprManager* exprManager); - explicit NodeManager(context::Context* ctxt, ExprManager* exprManager, const Options& options); + explicit NodeManager(ExprManager* exprManager); ~NodeManager(); /** The node manager in the current public-facing CVC4 library context */ static NodeManager* currentNM() { return s_current; } - - /** 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 skolem manager */ + SkolemManager* getSkolemManager() { return d_skManager.get(); } /** Get this node manager's statistics registry */ - StatisticsRegistry* getStatisticsRegistry() const throw() { + StatisticsRegistry* getStatisticsRegistry() const + { return d_statisticsRegistry; } /** Subscribe to NodeManager events */ void subscribeEvents(NodeManagerListener* listener) { - Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed"); + Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) + == d_listeners.end()) + << "listener already subscribed"; d_listeners.push_back(listener); } /** Unsubscribe from NodeManager events */ void unsubscribeEvents(NodeManagerListener* listener) { std::vector::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener); - Assert(elt != d_listeners.end(), "listener not subscribed"); + Assert(elt != d_listeners.end()) << "listener not subscribed"; d_listeners.erase(elt); } + /** 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 dt); + /** + * Return the datatype at the given index owned by this class. Type nodes are + * associated with datatypes through the DatatypeIndexConstant class. The + * argument index is intended to be a value taken from that class. + * + * Type nodes must access their DTypes through a level of indirection to + * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which + * 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(size_t index) const; + /** Get a Kind from an operator expression */ static inline Kind operatorToKind(TNode n); + /** Get corresponding application kind for function + * + * Different functional nodes are applied differently, according to their + * type. For example, uninterpreted functions (of FUNCTION_TYPE) are applied + * via APPLY_UF, while constructors (of CONSTRUCTOR_TYPE) via + * APPLY_CONSTRUCTOR. This method provides the correct application according + * to which functional type fun has. + * + * @param fun The functional node + * @return the correct application kind for fun. If fun's type is not function + * like (see TypeNode::isFunctionLike), then UNDEFINED_KIND is returned. + */ + static Kind getKindForFunction(TNode fun); + // general expression-builders /** Create a node with one child. */ @@ -377,6 +473,28 @@ public: template Node* mkNodePtr(Kind kind, const std::vector >& 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 + Node mkAnd(const std::vector >& 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 + Node mkOr(const std::vector >& children); + /** Create a node (with no children) by operator. */ Node mkNode(TNode opNode); Node* mkNodePtr(TNode opNode); @@ -417,18 +535,59 @@ public: Node mkBoundVar(const TypeNode& type); Node* mkBoundVarPtr(const TypeNode& type); + /** 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 children.size() is greater than the max arity for + * kind, then the expression will be broken up into + * suitably-sized chunks, taking advantage of the associativity of + * kind. For example, if kind FOO has max arity + * 2, then calling mkAssociative(FOO,a,b,c) will return + * (FOO (FOO a b) c) or (FOO a (FOO b c)). + * The order of the arguments will be preserved in a left-to-right + * traversal of the resulting tree. + */ + Node mkAssociative(Kind kind, const std::vector& 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& 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& 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& children); + /** * Optional flags used to control behavior of NodeManager::mkSkolem(). * They should be composed with a bitwise OR (e.g., * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT * cannot be composed in such a manner. */ - enum SkolemFlags { - 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 */ - };/* enum SkolemFlags */ + enum SkolemFlags + { + 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_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */ + }; /* enum SkolemFlags */ /** * Create a skolem constant with the given name, type, and comment. @@ -454,9 +613,34 @@ public: /** 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. @@ -660,34 +844,37 @@ public: 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. */ + 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. @@ -696,7 +883,7 @@ public: * @param range the range type * @returns the functional type domain -> range */ - inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range); + TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range); /** * Make a function type with input types from @@ -706,8 +893,8 @@ public: * @param range the range type * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range */ - inline TypeNode mkFunctionType(const std::vector& argTypes, - const TypeNode& range); + TypeNode mkFunctionType(const std::vector& argTypes, + const TypeNode& range); /** * Make a function type with input types from @@ -715,7 +902,7 @@ public: * sorts[sorts.size()-1]. sorts must have * at least 2 elements. */ - inline TypeNode mkFunctionType(const std::vector& sorts); + TypeNode mkFunctionType(const std::vector& sorts); /** * Make a predicate type with input types from @@ -723,7 +910,7 @@ public: * BOOLEAN. sorts must have at least one * element. */ - inline TypeNode mkPredicateType(const std::vector& sorts); + TypeNode mkPredicateType(const std::vector& sorts); /** * Make a tuple type with types from @@ -733,7 +920,7 @@ public: * @param types a vector of types * @returns the tuple type (types[0], ..., types[n]) */ - inline TypeNode mkTupleType(const std::vector& types); + TypeNode mkTupleType(const std::vector& types); /** * Make a record type with the description from rec. @@ -741,7 +928,7 @@ public: * @param rec a description of the record * @returns the record type */ - inline TypeNode mkRecordType(const Record& rec); + TypeNode mkRecordType(const Record& rec); /** * Make a symbolic expression type with types from @@ -753,17 +940,86 @@ public: */ inline TypeNode mkSExprType(const std::vector& types); + /** Make the type of floating-point with exp bit exponent and + sig bit significand */ + TypeNode mkFloatingPointType(unsigned exp, unsigned sig); + TypeNode mkFloatingPointType(FloatingPointSize fs); + /** Make the type of bitvectors of size size */ - 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 arrays with the given parameterization */ + /** Make the type of set with the given parameterization */ inline TypeNode mkSetType(TypeNode elementType); - /** Make a type representing a constructor with the given parameterization */ - TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range); + /** 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); + + /** 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 mkMutualDatatypeTypes( + const std::vector& 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 mkMutualDatatypeTypes( + const std::vector& datatypes, + const std::set& unresolvedTypes, + uint32_t flags = DATATYPE_FLAG_NONE); + + /** + * Make a type representing a constructor with the given argument (subfield) + * types and return type range. + */ + TypeNode mkConstructorType(const std::vector& args, TypeNode range); /** Make a type representing a selector with the given parameterization */ inline TypeNode mkSelectorType(TypeNode domain, TypeNode range); @@ -783,38 +1039,9 @@ public: uint32_t flags = ExprManager::SORT_FLAG_NONE); /** Make a new sort with the given name and arity. */ - TypeNode mkSortConstructor(const std::string& name, size_t arity); - - /** - * Make a predicate subtype type defined by the given LAMBDA - * expression. A TypeCheckingExceptionPrivate can be thrown if - * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at - * proving that the resulting predicate subtype is inhabited. - */ - TypeNode mkPredicateSubtype(Expr lambda) - throw(TypeCheckingExceptionPrivate); - - /** - * Make a predicate subtype type defined by the given LAMBDA - * expression and whose non-emptiness is witnessed by the given - * witness. A TypeCheckingExceptionPrivate can be thrown if lambda - * is not a LAMBDA, or is ill-typed, or if the witness is not a - * witness or ill-typed. - */ - TypeNode mkPredicateSubtype(Expr lambda, Expr witness) - throw(TypeCheckingExceptionPrivate); - - /** - * Make an integer subrange type as defined by the argument. - */ - TypeNode mkSubrangeType(const SubrangeBounds& bounds) - throw(TypeCheckingExceptionPrivate); - - /** - * Given a tuple or record type, get the internal datatype used for - * it. Makes the DatatypeType if necessary. - */ - TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType); + TypeNode mkSortConstructor(const std::string& name, + size_t arity, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** * Get the type for the given node and optionally do type checking. @@ -841,8 +1068,7 @@ public: * @param check whether we should check the type as we compute it * (default: false) */ - TypeNode getType(TNode n, bool check = false) - throw(TypeCheckingExceptionPrivate, AssertionException); + TypeNode getType(TNode n, bool check = false); /** * Convert a node to an expression. Uses the ExprManager @@ -868,7 +1094,7 @@ public: /** * 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. @@ -921,128 +1147,24 @@ public: class NodeManagerScope { /** The old NodeManager, to be restored on destruction. */ NodeManager* d_oldNodeManager; - 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; - 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(BOOLEAN_TYPE)); -} - -/** Get the (singleton) type for integers. */ -inline TypeNode NodeManager::integerType() { - return TypeNode(mkTypeConst(INTEGER_TYPE)); -} - -/** Get the (singleton) type for reals. */ -inline TypeNode NodeManager::realType() { - return TypeNode(mkTypeConst(REAL_TYPE)); -} - -/** Get the (singleton) type for strings. */ -inline TypeNode NodeManager::stringType() { - return TypeNode(mkTypeConst(STRING_TYPE)); -} - -/** Get the (singleton) type for regexps. */ -inline TypeNode NodeManager::regexpType() { - return TypeNode(mkTypeConst(REGEXP_TYPE)); -} - -/** Get the bound var list type. */ -inline TypeNode NodeManager::boundVarListType() { - return TypeNode(mkTypeConst(BOUND_VAR_LIST_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternType() { - return TypeNode(mkTypeConst(INST_PATTERN_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternListType() { - return TypeNode(mkTypeConst(INST_PATTERN_LIST_TYPE)); -} - -/** Get the (singleton) type for builtin operators. */ -inline TypeNode NodeManager::builtinOperatorType() { - return TypeNode(mkTypeConst(BUILTIN_OPERATOR_TYPE)); -} - -/** Make a function type from domain to range. */ -inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { - std::vector sorts; - sorts.push_back(domain); - sorts.push_back(range); - return mkFunctionType(sorts); -} - -inline TypeNode NodeManager::mkFunctionType(const std::vector& argTypes, const TypeNode& range) { - Assert(argTypes.size() >= 1); - std::vector sorts(argTypes); - sorts.push_back(range); - return mkFunctionType(sorts); -} - -inline TypeNode -NodeManager::mkFunctionType(const std::vector& sorts) { - Assert(sorts.size() >= 2); - std::vector sortNodes; - for (unsigned i = 0; i < sorts.size(); ++ i) { - CheckArgument(!sorts[i].isFunctionLike(), sorts, - "cannot create higher-order function types"); - sortNodes.push_back(sorts[i]); - } - return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); -} - -inline TypeNode -NodeManager::mkPredicateType(const std::vector& sorts) { - Assert(sorts.size() >= 1); - std::vector sortNodes; - for (unsigned i = 0; i < sorts.size(); ++ i) { - CheckArgument(!sorts[i].isFunctionLike(), sorts, - "cannot create higher-order function types"); - sortNodes.push_back(sorts[i]); - } - sortNodes.push_back(booleanType()); - return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); -} - -inline TypeNode NodeManager::mkTupleType(const std::vector& types) { - std::vector typeNodes; - for (unsigned i = 0; i < types.size(); ++ i) { - CheckArgument(!types[i].isFunctionLike(), types, - "cannot put function-like types in tuples"); - typeNodes.push_back(types[i]); - } - return mkTypeNode(kind::TUPLE_TYPE, typeNodes); -} - -inline TypeNode NodeManager::mkRecordType(const Record& rec) { - return mkTypeConst(rec); -} - inline TypeNode NodeManager::mkSExprType(const std::vector& types) { std::vector typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { @@ -1051,45 +1173,49 @@ inline TypeNode NodeManager::mkSExprType(const std::vector& types) { return mkTypeNode(kind::SEXPR_TYPE, typeNodes); } -inline TypeNode NodeManager::mkBitVectorType(unsigned size) { - return TypeNode(mkTypeConst(BitVectorSize(size))); -} - inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { CheckArgument(!indexType.isNull(), indexType, "unexpected NULL index type"); CheckArgument(!constituentType.isNull(), constituentType, "unexpected NULL constituent type"); - CheckArgument(!indexType.isFunctionLike(), indexType, - "cannot index arrays by a function-like type"); - CheckArgument(!constituentType.isFunctionLike(), constituentType, - "cannot store function-like types in arrays"); - Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; + CheckArgument(indexType.isFirstClass(), + indexType, + "cannot index arrays by types that are not first-class. Try " + "option --uf-ho."); + CheckArgument(constituentType.isFirstClass(), + constituentType, + "cannot store types that are not first-class in arrays. Try " + "option --uf-ho."); + Debug("arrays") << "making array type " << indexType << " " + << constituentType << std::endl; return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } inline TypeNode NodeManager::mkSetType(TypeNode elementType) { CheckArgument(!elementType.isNull(), elementType, "unexpected NULL element type"); - // TODO: Confirm meaning of isFunctionLike(). --K - CheckArgument(!elementType.isFunctionLike(), elementType, - "cannot store function-like types in sets"); + CheckArgument(elementType.isFirstClass(), + elementType, + "cannot store types that are not first-class in sets. Try " + "option --uf-ho."); Debug("sets") << "making sets type " << elementType << std::endl; return mkTypeNode(kind::SET_TYPE, elementType); } inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { - CheckArgument(!domain.isFunctionLike(), domain, - "cannot create higher-order function types"); - CheckArgument(!range.isFunctionLike(), range, - "cannot create higher-order function types"); + CheckArgument(domain.isDatatype(), domain, + "cannot create non-datatype selector type"); + CheckArgument(range.isFirstClass(), + range, + "cannot have selector fields that are not first-class types. " + "Try option --uf-ho."); return mkTypeNode(kind::SELECTOR_TYPE, domain, range); } inline TypeNode NodeManager::mkTesterType(TypeNode domain) { - CheckArgument(!domain.isFunctionLike(), domain, - "cannot create higher-order function types"); + CheckArgument(domain.isDatatype(), domain, + "cannot create non-datatype tester"); return mkTypeNode(kind::TESTER_TYPE, domain ); } @@ -1103,14 +1229,14 @@ inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { } inline void NodeManager::poolInsert(expr::NodeValue* nv) { - Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), - "NodeValue already in the pool!"); + Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end()) + << "NodeValue already in the pool!"; d_nodeValuePool.insert(nv);// FIXME multithreading } inline void NodeManager::poolRemove(expr::NodeValue* nv) { - Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(), - "NodeValue is not in the pool!"); + Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end()) + << "NodeValue is not in the pool!"; d_nodeValuePool.erase(nv);// FIXME multithreading } @@ -1131,7 +1257,8 @@ inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) { return exprManager->getNodeManager(); } -inline Type NodeManager::toType(TypeNode tn) { +inline Type NodeManager::toType(const TypeNode& tn) +{ return Type(this, new TypeNode(tn)); } @@ -1141,9 +1268,9 @@ inline TypeNode NodeManager::fromType(Type t) { }/* CVC4 namespace */ -#define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/metakind.h" -#undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/node_builder.h" @@ -1156,6 +1283,7 @@ inline bool NodeManager::hasOperator(Kind k) { case kind::metakind::INVALID: case kind::metakind::VARIABLE: + case kind::metakind::NULLARY_OPERATOR: return false; case kind::metakind::OPERATOR: @@ -1165,8 +1293,7 @@ inline bool NodeManager::hasOperator(Kind k) { case kind::metakind::CONSTANT: return false; - default: - Unhandled(mk); + default: Unhandled() << mk; } } @@ -1250,6 +1377,34 @@ inline Node NodeManager::mkNode(Kind kind, return nb.constructNode(); } +template +Node NodeManager::mkAnd(const std::vector >& children) +{ + if (children.empty()) + { + return mkConst(true); + } + else if (children.size() == 1) + { + return children[0]; + } + return mkNode(kind::AND, children); +} + +template +Node NodeManager::mkOr(const std::vector >& children) +{ + if (children.empty()) + { + return mkConst(false); + } + else if (children.size() == 1) + { + return children[0]; + } + return mkNode(kind::OR, children); +} + template inline Node* NodeManager::mkNodePtr(Kind kind, const std::vector >& @@ -1430,6 +1585,9 @@ TypeNode NodeManager::mkTypeConst(const T& val) { template 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::OwningTheory theory_t; NVStorage<1> nvStorage; @@ -1484,4 +1642,4 @@ NodeClass NodeManager::mkConstInternal(const T& val) { }/* CVC4 namespace */ -#endif /* __CVC4__NODE_MANAGER_H */ +#endif /* CVC4__NODE_MANAGER_H */