diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-10 14:35:25 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-10 14:35:37 +0100 |
commit | 81dca680f6c88d10b56a0ed065d470d907766e21 (patch) | |
tree | 4410fa473ecb6848f7976b2b6a00188ac5e44775 /src/util | |
parent | 50c8533760bfd5b1f803d52bc4318c544521e6af (diff) |
Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 33 | ||||
-rw-r--r-- | src/util/datatype.h | 2 |
2 files changed, 30 insertions, 5 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 138fb4bb0..a53759c08 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -334,6 +334,20 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { } } +Expr getSubtermWithType( Expr e, Type t, bool isTop ){ + if( !isTop && e.getType()==t ){ + return e; + }else{ + for( unsigned i=0; i<e.getNumChildren(); i++ ){ + Expr se = getSubtermWithType( e[i], t, false ); + if( !se.isNull() ){ + return se; + } + } + return Expr(); + } +} + Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) { if( std::find( processing.begin(), processing.end(), d_self )==processing.end() ){ processing.push_back( d_self ); @@ -342,8 +356,14 @@ Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) cons //do nullary constructors first if( ((*i).getNumArgs()==0)==(r==0)){ Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl; - Expr e = (*i).computeGroundTerm( t, processing ); + Expr e = (*i).computeGroundTerm( t, processing, d_ground_term ); if( !e.isNull() ){ + //must check subterms for the same type to avoid infinite loops in type enumeration + Expr se = getSubtermWithType( e, t, true ); + if( !se.isNull() ){ + Debug("datatypes") << "Take subterm " << se << std::endl; + e = se; + } processing.pop_back(); return e; }else{ @@ -780,7 +800,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { return true; } -Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) { +Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) { // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); @@ -801,8 +821,13 @@ Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& proces } Expr arg; if( selType.isDatatype() ){ - const Datatype & dt = DatatypeType(selType).getDatatype(); - arg = dt.computeGroundTerm( selType, processing ); + std::map< Type, Expr >::iterator itgt = gt.find( selType ); + if( itgt != gt.end() ){ + arg = itgt->second; + }else{ + const Datatype & dt = DatatypeType(selType).getDatatype(); + arg = dt.computeGroundTerm( selType, processing ); + } }else{ arg = selType.mkGroundTerm(); } diff --git a/src/util/datatype.h b/src/util/datatype.h index 0b8b8c61f..85668cd55 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -218,7 +218,7 @@ private: /** compute whether this datatype is well-founded */ bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute ground term */ - Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException); + Expr computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException); public: /** * Create a new Datatype constructor with the given name for the |