From 081351e87edeb52facba0d0abc2e933433480444 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 15 Jan 2016 00:18:49 +0100
Subject: [PATCH] Ensure model construction for parametric sorts involving
 uninterpreted sorts respect cardinality bounds on when finite model finding
 is enabled.

---
 src/theory/theory_model.cpp                   | 68 ++++++++++++++++++-
 src/theory/theory_model.h                     |  3 +
 test/regress/regress0/fmf/Makefile.am         |  8 ++-
 .../regress/regress0/fmf/dt-proper-model.smt2 | 16 +++++
 4 files changed, 91 insertions(+), 4 deletions(-)
 create mode 100755 test/regress/regress0/fmf/dt-proper-model.smt2

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(){}
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index bca9f2e4f..5abadbcb8 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -20,7 +20,6 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 TESTS =	\
 	array_card.smt2 \
-	agree466.smt2 \
 	ALG008-1.smt2 \
 	german169.smt2 \
 	QEpres-uf.855035.smt \
@@ -43,7 +42,8 @@ TESTS =	\
 	syn002-si-real-int.smt2 \
 	krs-sat.smt2 \
 	forall_unit_data2.smt2 \
-	sc_bad_model_1221.smt2
+  sc_bad_model_1221.smt2 \
+  dt-proper-model.smt2
 
 
 EXTRA_DIST = $(TESTS)
@@ -54,11 +54,13 @@ EXTRA_DIST = $(TESTS)
 #TESTS += \
 #	error.cvc
 #endif
-#
+# 
 # and make sure to distribute it
 #EXTRA_DIST += \
 #	error.cvc
 
+# agree466.smt2 timeout after commit on 1/14 due to Array+FMF model construction
+
 # synonyms for "check" in this directory
 .PHONY: regress regress0 test
 regress regress0 test: check
diff --git a/test/regress/regress0/fmf/dt-proper-model.smt2 b/test/regress/regress0/fmf/dt-proper-model.smt2
new file mode 100755
index 000000000..60a0b6377
--- /dev/null
+++ b/test/regress/regress0/fmf/dt-proper-model.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-datatypes () ((D (cons (x Int) (y U)))))
+(declare-fun d1 () D)
+(declare-fun d2 () D)
+(declare-fun d3 () D)
+(declare-fun d4 () D)
+(assert (distinct d1 d2 d3 d4))
+(assert (forall ((x U) (y U)) (= x y)))
+(declare-fun a () U)
+(declare-fun P (U) Bool)
+(assert (P a))
+(check-sat)
\ No newline at end of file
-- 
2.30.2