cardinality CONSTRUCTOR_TYPE \
"::CVC4::theory::datatypes::ConstructorProperties::computeCardinality(%TYPE%)" \
"theory/datatypes/theory_datatypes_type_rules.h"
-well-founded CONSTRUCTOR_TYPE \
- "::CVC4::theory::datatypes::ConstructorProperties::isWellFounded(%TYPE%)" \
- "::CVC4::theory::datatypes::ConstructorProperties::mkGroundTerm(%TYPE%)" \
- "theory/datatypes/theory_datatypes_type_rules.h"
# selector type has domain type and a range type
operator SELECTOR_TYPE 2 "selector"
}
return c;
}
-
- inline static bool isWellFounded(TypeNode type) {
- // Constructors aren't exactly functions, they're like
- // parameterized ground terms. So the wellfoundedness is more
- // like that of a tuple than that of a function.
- AssertArgument(type.isConstructor(), type);
- for(unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) {
- if(!type[i].isWellFounded()) {
- return false;
- }
- }
- return true;
- }
-
- inline static Node mkGroundTerm(TypeNode type) {
- AssertArgument(type.isConstructor(), type);
-
- // is this already in the cache ?
- Node groundTerm = type.getAttribute(GroundTermAttr());
- if(!groundTerm.isNull()) {
- return groundTerm;
- }
-
- // This is a bit tricky; Constructors have a unique index within
- // their datatype, but Constructor *types* do not; multiple
- // Constructors within the same Datatype could share the same
- // type. So we scan through the datatype to find one that
- // matches.
- //const Datatype& dt = type[type.getNumChildren() - 1].getConst<Datatype>();
- const Datatype& dt = DatatypeType(type[type.getNumChildren() - 1].toType()).getDatatype();
- for(Datatype::const_iterator i = dt.begin(),
- i_end = dt.end();
- i != i_end;
- ++i) {
- if(TypeNode::fromType((*i).getConstructor().getType()) == type) {
- groundTerm = Node::fromExpr((*i).mkGroundTerm( type.toType() ));
- type.setAttribute(GroundTermAttr(), groundTerm);
- return groundTerm;
- }
- }
-
- InternalError("couldn't find a matching constructor?!");
- }
};/* struct ConstructorProperties */
struct TupleTypeRule {
channel.h \
language.cpp \
ntuple.h \
- recursion_breaker.h \
subrange_bound.h \
dump.h \
dump.cpp \
cardinality.cpp \
cache.h \
utility.h \
- trans_closure.h \
- trans_closure.cpp \
boolean_simplification.h \
boolean_simplification.cpp \
ite_removal.h \
#include "expr/node_manager.h"
#include "expr/node.h"
#include "expr/attribute.h"
-#include "util/recursion_breaker.h"
#include "util/matcher.h"
#include "util/cvc4_assert.h"
struct DatatypeIndexTag {};
struct DatatypeConsIndexTag {};
struct DatatypeFiniteTag {};
- struct DatatypeWellFoundedTag {};
struct DatatypeFiniteComputedTag {};
- struct DatatypeWellFoundedComputedTag {};
- struct DatatypeGroundTermTag {};
}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr;
typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
-typedef expr::Attribute<expr::attr::DatatypeWellFoundedTag, bool> DatatypeWellFoundedAttr;
typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
-typedef expr::Attribute<expr::attr::DatatypeWellFoundedComputedTag, bool> DatatypeWellFoundedComputedAttr;
-typedef expr::Attribute<expr::attr::DatatypeGroundTermTag, Node> DatatypeGroundTermAttr;
const Datatype& Datatype::datatypeOf(Expr item) {
ExprManagerScope ems(item);
CheckArgument(isResolved(), this, "this datatype is not yet resolved");
ExprManagerScope ems(d_self);
- TypeNode self = TypeNode::fromType(d_self);
// is this already in the cache ?
- Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr();
- if(!groundTerm.isNull()) {
- Debug("datatypes") << "\nin cache: " << d_self << " => " << groundTerm << std::endl;
+ std::map< Type, Expr >::iterator it = d_ground_term.find( t );
+ if( it != d_ground_term.end() ){
+ Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl;
+ return it->second;
} else {
std::vector< Type > processing;
- groundTerm = computeGroundTerm( t, processing );
- if(!groundTerm.isNull() && !isParametric() ) {
+ Expr groundTerm = computeGroundTerm( t, processing );
+ if(!groundTerm.isNull() ) {
// we found a ground-term-constructing constructor!
- self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
}
- }
- if( groundTerm.isNull() ){
- if( !d_isCo ){
- // if we get all the way here, we aren't well-founded
- CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!");
+ d_ground_term[t] = groundTerm;
+ if( groundTerm.isNull() ){
+ if( !d_isCo ){
+ // if we get all the way here, we aren't well-founded
+ CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!");
+ }else{
+ return groundTerm;
+ }
}else{
return groundTerm;
}
- }else{
- return groundTerm;
}
}
return true;
}
-bool DatatypeConstructor::isWellFounded() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-
- // we're using some internals, so we have to set up this library context
- ExprManagerScope ems(d_constructor);
- std::vector< Type > processing;
- return computeWellFounded( processing );
-}
-
-Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-
- // we're using some internals, so we have to set up this library context
- ExprManagerScope ems(d_constructor);
-
- TNode self = Node::fromExpr(d_constructor);
-
- // is this already in the cache ?
- Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr();
- if(!groundTerm.isNull()) {
- return groundTerm;
- }
-
- RecursionBreaker<const DatatypeConstructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
- if(breaker.isRecursion()) {
- // Recursive path, we should skip and go to the next constructor;
- // see lengthy comments in Datatype::mkGroundTerm().
- return Expr();
- }
-
- std::vector<Expr> groundTerms;
- groundTerms.push_back(getConstructor());
-
- // for each selector, get a ground term
- CheckArgument( t.isDatatype(), t );
- std::vector< Type > instTypes;
- std::vector< Type > paramTypes;
- if( DatatypeType(t).isParametric() ){
- paramTypes = DatatypeType(t).getDatatype().getParameters();
- instTypes = DatatypeType(t).getParamTypes();
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type selType = SelectorType((*i).getSelector().getType()).getRangeType();
- if( DatatypeType(t).isParametric() ){
- selType = selType.substitute( paramTypes, instTypes );
- }
- groundTerms.push_back(selType.mkGroundTerm());
- }
-
- groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
- if( groundTerm.getType()!=t ){
- Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
- //type is ambiguous, must apply type ascription
- Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
- groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
- getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
- groundTerms[0]);
- groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
- }
- self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
- return groundTerm;
-}
-
Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
*/
bool isFinite() const throw(IllegalArgumentException);
- /**
- * Return true iff this constructor is well-founded (there exist
- * ground terms). The constructor must be resolved or an
- * exception is thrown.
- */
- bool isWellFounded() const throw(IllegalArgumentException);
-
- /**
- * Construct and return a ground term of this constructor. The
- * constructor must be both resolved and well-founded, or else an
- * exception is thrown.
- */
- Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
-
/**
* Returns true iff this Datatype constructor has already been
* resolved.
// is this well-founded
mutable int d_well_founded;
// ground term for this datatype
- mutable Expr d_ground_term;
+ mutable std::map< Type, Expr > d_ground_term;
/**
* Datatypes refer to themselves, recursively, and we have a
+++ /dev/null
-/********************* */
-/*! \file recursion_breaker.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A utility class to help with detecting recursion in a
- ** computation
- **
- ** A utility class to help with detecting recursion in a computation.
- ** A breadcrumb trail is left, and a function can query the breaker
- ** to see if recursion has occurred. For example:
- **
- ** @code
- ** int foo(int x) {
- ** RecursionBreaker<int> breaker("foo", x);
- ** if(breaker.isRecursion()) {
- ** ++d_count;
- ** return 0;
- ** }
- ** int xfactor = x * x;
- ** if(x > 0) {
- ** xfactor = -xfactor;
- ** }
- ** int y = foo(11 * x + xfactor);
- ** int z = y < 0 ? y : x * y;
- ** cout << "x == " << x << ", y == " << y << " ==> " << z << endl;
- ** return z;
- ** }
- ** @endcode
- **
- ** Recursion occurs after a while in this example, and the recursion
- ** is broken by the RecursionBreaker.
- **
- ** RecursionBreaker is really just a thread-local set of "what has
- ** been seen." The above example is trivial, easily fixed by
- ** allocating such a set at the base of the recursion, and passing a
- ** reference to it to each invocation. But other cases of
- ** nontrivial, mutual recursion exist that aren't so easily broken,
- ** and that's what the RecursionBreaker is for. See
- ** Datatype::getCardinality(), for example. A Datatype's cardinality
- ** depends on the cardinalities of the types it references---but
- ** these, in turn can reference the original datatype in a cyclic
- ** fashion. Where that happens, we need to break the recursion.
- **
- ** Several RecursionBreakers can be used at once; each is identified
- ** by the string tag in its constructor. If a single function is
- ** involved in the detection of recursion, a good choice is to use
- ** __FUNCTION__:
- **
- ** RecursionBreaker<Foo*>(__FUNCTION__, this) breaker;
- **
- ** Of course, if you're using GNU, you might prefer
- ** __PRETTY_FUNCTION__, since it's robust to overloading, namespaces,
- ** and containing classes. But neither is a good choice if two
- ** functions need to access the same RecursionBreaker mechanism.
- **
- ** For non-primitive datatypes, it might be a good idea to use a
- ** pointer type to instantiate RecursionBreaker<>, for example with
- ** RecursionBreaker<Foo*>.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__RECURSION_BREAKER_H
-#define __CVC4__RECURSION_BREAKER_H
-
-#include <string>
-#include <map>
-#include <ext/hash_set>
-#include "util/hash.h"
-#include "util/tls.h"
-#include "util/cvc4_assert.h"
-
-namespace CVC4 {
-
-template <class T, class Hasher = std::hash<T> >
-class RecursionBreaker {
- typedef std::hash_set<T, Hasher> Set;
- typedef std::map<std::string, Set> Map;
- static CVC4_THREADLOCAL(Map*) s_maps;
-
- std::string d_tag;
- const T d_item;
- bool d_firstToTag;
- bool d_recursion;
-
-public:
- /** Mark that item has been seen for tag. */
- RecursionBreaker(std::string tag, const T& item) :
- d_tag(tag),
- d_item(item) {
- if(s_maps == NULL) {
- s_maps = new Map();
- }
- d_firstToTag = s_maps->find(tag) == s_maps->end();
- Set& set = (*s_maps)[tag];
- d_recursion = (set.find(item) != set.end());
- Assert(!d_recursion || !d_firstToTag);
- if(!d_recursion) {
- set.insert(item);
- }
- }
-
- /** Clean up the seen trail. */
- ~RecursionBreaker() {
- Assert(s_maps->find(d_tag) != s_maps->end());
- if(!d_recursion) {
- (*s_maps)[d_tag].erase(d_item);
- }
- if(d_firstToTag) {
- Assert((*s_maps)[d_tag].empty());
- s_maps->erase(d_tag);
- Assert(s_maps->find(d_tag) == s_maps->end());
- }
- }
-
- /** Return true iff recursion has been detected. */
- bool isRecursion() const throw() {
- return d_recursion;
- }
-
-};/* class RecursionBreaker<T> */
-
-template <class T, class Hasher>
-CVC4_THREADLOCAL(typename RecursionBreaker<T, Hasher>::Map*) RecursionBreaker<T, Hasher>::s_maps;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__RECURSION_BREAKER_H */
+++ /dev/null
-/********************* */
-/*! \file trans_closure.cpp
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief The transitive closure module implementation
- **
- ** Implementation file for TransitiveClosure class.
- **/
-
-
-#include "util/trans_closure.h"
-#include "util/cvc4_assert.h"
-
-
-using namespace std;
-
-
-namespace CVC4 {
-
-
-TransitiveClosure::~TransitiveClosure() {
- unsigned i;
- for (i = 0; i < adjMatrix.size(); ++i) {
- if (adjMatrix[i]) {
- adjMatrix[i]->deleteSelf();
- }
- }
-}
-
-
-bool TransitiveClosure::addEdge(unsigned i, unsigned j)
-{
- Debug("trans-closure") << "Add edge " << i << " -> " << j << std::endl;
- // Check for loops
- Assert(i != j, "Cannot add self-loop");
- if (adjIndex.get() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) {
- return true;
- }
-
- // Grow matrix if necessary
- unsigned maxSize = ((i > j) ? i : j) + 1;
- while (maxSize > adjIndex.get()) {
- if( maxSize > adjMatrix.size() ){
- adjMatrix.push_back(NULL);
- }else if( adjMatrix[adjIndex.get()]!=NULL ){
- adjMatrix[adjIndex.get()]->clear();
- }
- adjIndex.set( adjIndex.get() + 1 );
- }
-
- // Add edge from i to j and everything j can reach
- if (adjMatrix[i] == NULL) {
- adjMatrix[i] = new (true) CDBV(d_context);
- }
- adjMatrix[i]->write(j);
- if (adjMatrix[j] != NULL) {
- adjMatrix[i]->merge(adjMatrix[j]);
- }
-
- // Add edges from everything that can reach i to j and everything that j can reach
- unsigned k;
- for (k = 0; k < adjIndex.get(); ++k) {
- if (adjMatrix[k] != NULL && adjMatrix[k]->read(i)) {
- adjMatrix[k]->write(j);
- if (adjMatrix[j] != NULL) {
- adjMatrix[k]->merge(adjMatrix[j]);
- }
- }
- }
-
- return false;
-}
-
-bool TransitiveClosure::isConnected(unsigned i, unsigned j)
-{
- if( i>=adjIndex.get() || j>adjIndex.get() ){//adjMatrix.size() ){
- return false;
- }else{
- return adjMatrix[i] != NULL && adjMatrix[i]->read(j);
- }
-}
-
-void TransitiveClosure::debugPrintMatrix()
-{
- unsigned i,j;
- for (i = 0; i < adjIndex.get(); ++i) {
- for (j = 0; j < adjIndex.get(); ++j) {
- if (adjMatrix[i] != NULL && adjMatrix[i]->read(j)) {
- Debug("trans-closure") << "1 ";
- }
- else Debug("trans-closure") << "0 ";
- }
- Debug("trans-closure") << endl;
- }
-}
-
-unsigned TransitiveClosureNode::getId( Node i ){
- context::CDHashMap< Node, unsigned, NodeHashFunction >::iterator it = nodeMap.find( i );
- if( it==nodeMap.end() ){
- unsigned c = d_counter.get();
- nodeMap[i] = c;
- d_counter.set( c + 1 );
- return c;
- }
- return (*it).second;
-}
-
-void TransitiveClosureNode::debugPrint(){
- for( int i=0; i<(int)currEdges.size(); i++ ){
- Debug("trans-closure") << "currEdges[ " << i << " ] = "
- << currEdges[i].first << " -> " << currEdges[i].second;
- int id1 = getId( currEdges[i].first );
- int id2 = getId( currEdges[i].second );
- Debug("trans-closure") << " { " << id1 << " -> " << id2 << " } ";
- Debug("trans-closure") << std::endl;
- }
- debugPrintMatrix();
-}
-
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file trans_closure.h
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief The transitive closure module
- **
- ** The transitive closure module.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__UTIL__TRANSITIVE_CLOSURE_H
-#define __CVC4__UTIL__TRANSITIVE_CLOSURE_H
-
-#include "context/context.h"
-#include "expr/node.h"
-#include <map>
-
-#include "context/cdlist.h"
-#include "context/cdhashmap.h"
-#include "context/cdo.h"
-
-namespace CVC4 {
-
-/*
- * Implements context-dependent variable-sized boolean vector
- */
-class CDBV :public context::ContextObj {
- uint64_t d_data;
- CDBV* d_next;
-
- CDBV(const CDBV& cdbv) : ContextObj(cdbv), d_data(cdbv.d_data), d_next(cdbv.d_next) {}
-
- /**
- * operator= for CDBV is private to ensure CDBV object is not copied.
- */
- CDBV& operator=(const CDBV& cdbv);
-
-protected:
- context::ContextObj* save(context::ContextMemoryManager* pCMM) {
- return new(pCMM) CDBV(*this);
- }
-
- void restore(context::ContextObj* pContextObj) {
- d_data = ((CDBV*) pContextObj)->d_data;
- }
-
- uint64_t data() { return d_data; }
-
- CDBV* next() { return d_next; }
-
-public:
- CDBV(context::Context* context) :
- ContextObj(context), d_data(0), d_next(NULL)
- {}
-
- ~CDBV() {
- if (d_next != NULL) {
- d_next->deleteSelf();
- }
- destroy();
- }
- void clear() { d_data = 0; if( d_next ) d_next->clear(); }
- bool read(unsigned index) {
- if (index < 64) return (d_data & (uint64_t(1) << index)) != 0;
- else if (d_next == NULL) return false;
- else return d_next->read(index - 64);
- }
-
- void write(unsigned index) {
- if (index < 64) {
- uint64_t mask = uint64_t(1) << index;
- if ((d_data & mask) != 0) return;
- makeCurrent();
- d_data = d_data | mask;
- }
- else if (d_next != NULL) {
- d_next->write(index - 64);
- }
- else {
- makeCurrent();
- d_next = new(true) CDBV(getContext());
- d_next->write(index - 64);
- }
- }
-
- void merge(CDBV* pcdbv) {
- d_data = d_data | pcdbv->data();
- if (d_next != NULL && pcdbv->next() != NULL) {
- d_next->merge(pcdbv->next());
- }
- }
-
-};
-
-
-/**
- * Transitive closure module for CVC4.
- *
- */
-class TransitiveClosure {
- context::Context* d_context;
- std::vector<CDBV* > adjMatrix;
- context::CDO<unsigned> adjIndex;
-
-public:
- TransitiveClosure(context::Context* context) : d_context(context), adjIndex(context,0) {}
- virtual ~TransitiveClosure();
-
- /* Add an edge from node i to node j. Return false if successful, true if this edge would create a cycle */
- bool addEdge(unsigned i, unsigned j);
- /** whether node i is connected to node j */
- bool isConnected(unsigned i, unsigned j);
- void debugPrintMatrix();
-};
-
-/**
- * Transitive closure module for nodes in CVC4.
- *
- */
-class TransitiveClosureNode : public TransitiveClosure{
- context::CDO< unsigned > d_counter;
- context::CDHashMap< Node, unsigned, NodeHashFunction > nodeMap;
- //for debugging
- context::CDList< std::pair< Node, Node > > currEdges;
-public:
- TransitiveClosureNode(context::Context* context) :
- TransitiveClosure(context), d_counter( context, 0 ), nodeMap( context ), currEdges(context) {}
- ~TransitiveClosureNode(){}
-
- /** get id for node */
- unsigned getId( Node i );
- /** Add an edge from node i to node j. Return false if successful, true if this edge would create a cycle */
- bool addEdgeNode(Node i, Node j) {
- currEdges.push_back( std::pair< Node, Node >( i, j ) );
- return addEdge( getId( i ), getId( j ) );
- }
- /** whether node i is connected to node j */
- bool isConnectedNode(Node i, Node j) {
- return isConnected( getId( i ), getId( j ) );
- }
- void debugPrint();
-};
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__UTIL__TRANSITIVE_CLOSURE_H */
projects / cvc5.git / commitdiff