From ea970ad8f995bb58303a1a594a39e1cc9bfc8d79 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 13 Feb 2015 14:59:42 +0100 Subject: Minor cleanup, remove unused files. --- src/theory/datatypes/kinds | 4 - src/theory/datatypes/theory_datatypes_type_rules.h | 43 ------ src/util/Makefile.am | 3 - src/util/datatype.cpp | 98 ++----------- src/util/datatype.h | 16 +-- src/util/recursion_breaker.h | 135 ------------------ src/util/trans_closure.cpp | 128 ----------------- src/util/trans_closure.h | 154 --------------------- 8 files changed, 15 insertions(+), 566 deletions(-) delete mode 100644 src/util/recursion_breaker.h delete mode 100644 src/util/trans_closure.cpp delete mode 100644 src/util/trans_closure.h diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 55db44c29..a4cd0d124 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -16,10 +16,6 @@ operator CONSTRUCTOR_TYPE 1: "constructor" 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" diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index b97645ecb..15d1c6c9e 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -264,49 +264,6 @@ struct ConstructorProperties { } 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(); - 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 { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index df787d049..59591dc3b 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -60,7 +60,6 @@ libutil_la_SOURCES = \ channel.h \ language.cpp \ ntuple.h \ - recursion_breaker.h \ subrange_bound.h \ dump.h \ dump.cpp \ @@ -70,8 +69,6 @@ libutil_la_SOURCES = \ cardinality.cpp \ cache.h \ utility.h \ - trans_closure.h \ - trans_closure.cpp \ boolean_simplification.h \ boolean_simplification.cpp \ ite_removal.h \ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index cd27a897b..47bd7de66 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -25,7 +25,6 @@ #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" @@ -38,20 +37,14 @@ namespace expr { struct DatatypeIndexTag {}; struct DatatypeConsIndexTag {}; struct DatatypeFiniteTag {}; - struct DatatypeWellFoundedTag {}; struct DatatypeFiniteComputedTag {}; - struct DatatypeWellFoundedComputedTag {}; - struct DatatypeGroundTermTag {}; }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ typedef expr::Attribute DatatypeIndexAttr; typedef expr::Attribute DatatypeConsIndexAttr; typedef expr::Attribute DatatypeFiniteAttr; -typedef expr::Attribute DatatypeWellFoundedAttr; typedef expr::Attribute DatatypeFiniteComputedAttr; -typedef expr::Attribute DatatypeWellFoundedComputedAttr; -typedef expr::Attribute DatatypeGroundTermAttr; const Datatype& Datatype::datatypeOf(Expr item) { ExprManagerScope ems(item); @@ -312,30 +305,30 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { 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; } } @@ -753,69 +746,6 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { 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 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 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); diff --git a/src/util/datatype.h b/src/util/datatype.h index 445048440..6e7e09fa0 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -319,20 +319,6 @@ public: */ 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. @@ -483,7 +469,7 @@ private: // 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 diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h deleted file mode 100644 index 3369c5c23..000000000 --- a/src/util/recursion_breaker.h +++ /dev/null @@ -1,135 +0,0 @@ -/********************* */ -/*! \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 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(__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. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__RECURSION_BREAKER_H -#define __CVC4__RECURSION_BREAKER_H - -#include -#include -#include -#include "util/hash.h" -#include "util/tls.h" -#include "util/cvc4_assert.h" - -namespace CVC4 { - -template > -class RecursionBreaker { - typedef std::hash_set Set; - typedef std::map 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 */ - -template -CVC4_THREADLOCAL(typename RecursionBreaker::Map*) RecursionBreaker::s_maps; - -}/* CVC4 namespace */ - -#endif /* __CVC4__RECURSION_BREAKER_H */ diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp deleted file mode 100644 index 02b51d751..000000000 --- a/src/util/trans_closure.cpp +++ /dev/null @@ -1,128 +0,0 @@ -/********************* */ -/*! \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 */ diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h deleted file mode 100644 index 27f32377e..000000000 --- a/src/util/trans_closure.h +++ /dev/null @@ -1,154 +0,0 @@ -/********************* */ -/*! \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 - -#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 adjMatrix; - context::CDO 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 */ -- cgit v1.2.3