Ensure model construction for parametric sorts involving uninterpreted sorts respect cardinality bounds on when finite model finding is enabled.

2 files changed, 70 insertions, 1 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index fb5fb0f0c..c6837ddf4 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -15,6 +15,7 @@
 
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
@@ -506,6 +507,43 @@ bool TheoryEngineModelBuilder::isCdtValueMatch( Node v, Node r, Node eqc, Node&
   return false;
 }
 
+bool TheoryEngineModelBuilder::involvesUSort( TypeNode tn ) {
+  if( tn.isSort() ){
+    return true;
+  }else if( tn.isArray() ){
+    return involvesUSort( tn.getArrayIndexType() ) || involvesUSort( tn.getArrayConstituentType() );
+  }else if( tn.isSet() ){
+    return involvesUSort( tn.getSetElementType() );
+  }else if( tn.isDatatype() ){
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    return dt.involvesUninterpretedType();
+  }else{
+    return false;
+  }
+}
+
+bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited ) {
+  Assert( v.isConst() );
+  if( visited.find( v )==visited.end() ){
+    visited[v] = true;
+    TypeNode tn = v.getType();
+    if( tn.isSort() ){
+      Trace("exc-value-debug") << "Is excluded usort value : " << v << " " << tn << std::endl;
+      unsigned card = eqc_usort_count[tn];
+      Trace("exc-value-debug") << "  Cardinality is " << card << std::endl;
+      unsigned index = v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
+      Trace("exc-value-debug") << "  Index is " << index << std::endl;
+      return index>0 && index>=card;
+    }
+    for( unsigned i=0; i<v.getNumChildren(); i++ ){
+      if( isExcludedUSortValue( eqc_usort_count, v[i], visited ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
 void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 {
   Trace("model-builder") << "TheoryEngineModelBuilder: buildModel, fullModel = " << fullModel << std::endl;
@@ -523,6 +561,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   d_te->collectModelInfo(tm, fullModel);
 
   // Loop through all terms and make sure that assignable sub-terms are in the equality engine
+  // Also, record #eqc per type (for finite model finding)
+  std::map< TypeNode, unsigned > eqc_usort_count;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
   {
     NodeSet cache;
@@ -531,6 +571,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       for ( ; !eqc_i.isFinished(); ++eqc_i) {
         checkTerms(*eqc_i, tm, cache);
       }
+      TypeNode tn = (*eqcs_i).getType();
+      if( tn.isSort() ){
+        if( eqc_usort_count.find( tn )==eqc_usort_count.end() ){
+          eqc_usort_count[tn] = 1;
+        }else{
+          eqc_usort_count[tn]++;
+        }
+      }
     }
   }
 
@@ -715,11 +763,16 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       if(t.isTuple() || t.isRecord()) {
         t = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
       }
+      //get properties of this type
       bool isCorecursive = false;
+      bool isUSortFiniteRestricted = false;
       if( t.isDatatype() ){
         const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
         isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() );
       }
+      if( options::finiteModelFind() ){
+        isUSortFiniteRestricted = !t.isSort() && involvesUSort( t );
+      }
       set<Node>* repSet = typeRepSet.getSet(t);
       TypeNode tb = t.getBaseType();
       if (!assignOne) {
@@ -756,14 +809,27 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
             bool success;
             do{
               n = typeConstSet.nextTypeEnum(t, true);
+              //--- AJR: this code checks whether n is a legal value
               success = true;
-              if( isCorecursive ){
+              if( isUSortFiniteRestricted ){
+                //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc)
+                std::map< Node, bool > visited;
+                success = !isExcludedUSortValue( eqc_usort_count, n, visited );
+                if( !success ){
+                  Trace("exc-value") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl;
+                }
+              }
+              if( success && isCorecursive ){
                 if (repSet != NULL && !repSet->empty()) {
                   // in the case of codatatypes, check if it is in the set of values that we cannot assign
                   // this will check whether n \not\in V^x_I from page 9 of Reynolds/Blanchette CADE 2015
                   success = !isExcludedCdtValue( n, repSet, assertedReps, *i2 );
+                  if( !success ){
+                    Trace("exc-value") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl;
+                  }
                 }
               }
+              //---
             }while( !success );
           }
           else {
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index fb2c3cd01..8ee4e843d 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -260,6 +260,9 @@ protected:
   /** is v an excluded codatatype value */
   bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
   bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
+  /** involves usort */
+  bool involvesUSort( TypeNode tn );
+  bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited );
 public:
   TheoryEngineModelBuilder(TheoryEngine* te);
   virtual ~TheoryEngineModelBuilder(){}