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.

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