/*! \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-2016 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
**
#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 <vector>
#include <string>
-#include <ext/hash_set>
+#include <unordered_set>
-#include "base/tls.h"
+#include "base/check.h"
#include "expr/kind.h"
#include "expr/metakind.h"
#include "expr/node_value.h"
-#include "util/subrange_bound.h"
#include "options/options.h"
namespace CVC4 {
class StatisticsRegistry;
class ResourceManager;
+class SkolemManager;
+
+class DType;
namespace expr {
namespace attr {
* 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<DatatypeType>& datatypes) { }
- 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
+ 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<TypeNode>& 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 */
+ virtual void nmNotifyDeleteNode(TNode n) {}
+}; /* class NodeManagerListener */
class NodeManager {
template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
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(const std::vector<Datatype>&, const std::set<Type>&);
-
/** Predicate for use with STL algorithms */
struct NodeValueReferenceCountNonZero {
bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
};
- typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValuePoolHashFunction,
- expr::NodeValuePoolEq> NodeValuePool;
- typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValueIDHashFunction,
- expr::NodeValueEq> ZombieSet;
+ typedef std::unordered_set<expr::NodeValue*,
+ expr::NodeValuePoolHashFunction,
+ expr::NodeValuePoolEq> NodeValuePool;
+ typedef std::unordered_set<expr::NodeValue*,
+ expr::NodeValueIDHashFunction,
+ expr::NodeValueIDEquality> NodeValueIDSet;
- static CVC4_THREADLOCAL(NodeManager*) s_current;
+ static thread_local NodeManager* s_current;
- Options* d_options;
StatisticsRegistry* d_statisticsRegistry;
- ResourceManager* d_resourceManager;
-
- /**
- * 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;
+ /** The skolem manager */
+ std::shared_ptr<SkolemManager> d_skManager;
NodeValuePool d_nodeValuePool;
* 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;
* 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<expr::NodeValue*> d_maxedOut;
/**
* A set of operator singletons (w.r.t. to this NodeManager
* plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
*/
Node d_operators[kind::LAST_KIND];
-
- /** sep nil per type */
- std::map< TypeNode, Node > d_sep_nils;
+
+ /** unique vars per (Kind,Type) */
+ std::map< Kind, std::map< TypeNode, Node > > d_unique_vars;
/**
* A list of subscribers for NodeManager events.
*/
std::vector<NodeManagerListener*> 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<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.
*/
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) {
}
}
+ /**
+ * 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.
*/
*/
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<expr::NodeValue*> TopologicalSort(
+ const std::vector<expr::NodeValue*>& roots);
+
/**
* This template gives a mechanism to stack-allocate a NodeValue
* with enough space for N children (where N is a compile-time
* 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&) CVC4_UNDEFINED;
+ NodeManager& operator=(const NodeManager&) = delete;
void init();
/** 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() throw() { return d_resourceManager; }
+ /** 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<NodeManagerListener*>::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<DType> 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. */
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);
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 <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_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.
/** Create a instantiation constant with the given type. */
Node mkInstConstant(const TypeNode& type);
-
- /** Create nil reference for separation logic with the given type (unique per type). */
- Node mkSepNil(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.
* @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
* @param range the range type
* @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
*/
- inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
- const TypeNode& range);
+ TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
+ const TypeNode& range);
/**
* Make a function type with input types from
* <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
* at least 2 elements.
*/
- inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
+ TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
/**
* Make a predicate type with input types from
* <code>BOOLEAN</code>. <code>sorts</code> must have at least one
* element.
*/
- inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
+ TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
/**
* Make a tuple type with types from
/** 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 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<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.
+ */
+ TypeNode mkConstructorType(const std::vector<TypeNode>& args, TypeNode range);
/** Make a type representing a selector with the given parameterization */
inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
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);
+ 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.
* @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
/**
* 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));
-}
-
-/** Make a function type from domain to range. */
-inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
- std::vector<TypeNode> sorts;
- sorts.push_back(domain);
- sorts.push_back(range);
- return mkFunctionType(sorts);
-}
-
-inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
- Assert(argTypes.size() >= 1);
- std::vector<TypeNode> sorts(argTypes);
- sorts.push_back(range);
- return mkFunctionType(sorts);
-}
-
-inline TypeNode
-NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
- Assert(sorts.size() >= 2);
- std::vector<TypeNode> 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<TypeNode>& sorts) {
- Assert(sorts.size() >= 1);
- std::vector<TypeNode> 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::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,
"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");
+ 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 );
}
}
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
}
return exprManager->getNodeManager();
}
-inline Type NodeManager::toType(TypeNode tn) {
+inline Type NodeManager::toType(const TypeNode& tn)
+{
return Type(this, new TypeNode(tn));
}
}/* 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"
case kind::metakind::INVALID:
case kind::metakind::VARIABLE:
+ case kind::metakind::NULLARY_OPERATOR:
return false;
case kind::metakind::OPERATOR:
case kind::metakind::CONSTANT:
return false;
- default:
- Unhandled(mk);
+ default: Unhandled() << mk;
}
}
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;
}/* CVC4 namespace */
-#endif /* __CVC4__NODE_MANAGER_H */
+#endif /* CVC4__NODE_MANAGER_H */
projects / cvc5.git / blobdiff