Fix preinitialization pass for finite model finding (#2047)

4 files changed, 57 insertions, 8 deletions

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index e97f716cb..9e77a31c1 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -339,12 +339,14 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
   
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
   Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
+  d_preinitialized_eqc.clear();
   d_preinitialized_types.clear();
   //traverse equality engine
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
   while( !eqcs_i.isFinished() ){
-    TypeNode tr = (*eqcs_i).getType();
-    d_preinitialized_types[tr] = true;
+    Node r = *eqcs_i;
+    TypeNode tr = r.getType();
+    d_preinitialized_eqc[tr] = r;
     ++eqcs_i;
   }
 
@@ -352,8 +354,10 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
   fm->initialize();
   for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
     Node op = it->first;
+    Trace("fmc") << "preInitialize types for " << op << std::endl;
     TypeNode tno = op.getType();
     for( unsigned i=0; i<tno.getNumChildren(); i++) {
+      Trace("fmc") << "preInitializeType " << tno[i] << std::endl;
       preInitializeType( fm, tno[i] );
     }
   }
@@ -461,6 +465,8 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     for( size_t i=0; i<add_conds.size(); i++ ){
       Node c = add_conds[i];
       Node v = add_values[i];
+      Trace("fmc-model-debug")
+          << "Add cond/value : " << c << " -> " << v << std::endl;
       std::vector< Node > children;
       std::vector< Node > entry_children;
       children.push_back(op);
@@ -486,6 +492,8 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
       }
       Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
       Node nv = fm->getRepresentative( v );
+      Trace("fmc-model-debug")
+          << "Representative of " << v << " is " << nv << std::endl;
       if( !nv.isConst() ){
         Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
         Assert( false );
@@ -562,11 +570,26 @@ void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn )
     if (!tn.isFunction() || options::ufHo())
     {
       Node mb = fm->getModelBasisTerm(tn);
-      if (!mb.isConst())
+      // if the model basis term does not exist in the model,
+      // either add it directly to the model's equality engine if no other terms
+      // of this type exist, or otherwise assert that it is equal to the first
+      // equivalence class of its type.
+      if (!fm->hasTerm(mb) && !mb.isConst())
       {
-        Trace("fmc") << "...add model basis term to EE of model " << mb << " "
-                     << tn << std::endl;
-        fm->d_equalityEngine->addTerm(mb);
+        std::map<TypeNode, Node>::iterator itpe = d_preinitialized_eqc.find(tn);
+        if (itpe == d_preinitialized_eqc.end())
+        {
+          Trace("fmc") << "...add model basis term to EE of model " << mb << " "
+                       << tn << std::endl;
+          fm->d_equalityEngine->addTerm(mb);
+        }
+        else
+        {
+          Trace("fmc") << "...add model basis eqc equality to model " << mb
+                       << " == " << itpe->second << " " << tn << std::endl;
+          bool ret = fm->assertEquality(mb, itpe->second, true);
+          AlwaysAssert(ret);
+        }
       }
     }
   }
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index a64c33303..852f96e4c 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -93,8 +93,25 @@ protected:
   std::map< TypeNode, Node > d_array_cond;
   std::map< Node, Node > d_array_term_cond;
   std::map< Node, std::vector< int > > d_star_insts;
-  std::map< TypeNode, bool > d_preinitialized_types;
+  //--------------------for preinitialization
+  /** preInitializeType
+   *
+   * This function ensures that the model fm is properly initialized with
+   * respect to type tn.
+   *
+   * In particular, this class relies on the use of "model basis" terms, which
+   * are distinguished terms that are used to specify default values for
+   * uninterpreted functions. This method enforces that the model basis term
+   * occurs in the model for each relevant type T, where a type T is relevant
+   * if a bound variable is of type T, or an uninterpreted function has an
+   * argument or a return value of type T.
+   */
   void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn );
+  /** for each type, an equivalence class of that type from the model */
+  std::map<TypeNode, Node> d_preinitialized_eqc;
+  /** map from types to whether we have called the method above */
+  std::map<TypeNode, bool> d_preinitialized_types;
+  //--------------------end for preinitialization
   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
   bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
 protected:
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index d235f27d3..0e0cee7f8 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1085,6 +1085,7 @@ REG1_TESTS = \
 	regress1/fmf/german169.smt2 \
 	regress1/fmf/german73.smt2 \
 	regress1/fmf/issue916-fmf-or.smt2 \
+	regress1/fmf/issue2034-preinit.smt2 \
 	regress1/fmf/jasmin-cdt-crash.smt2 \
 	regress1/fmf/ko-bound-set.cvc \
 	regress1/fmf/loopy_coda.smt2 \
@@ -1589,7 +1590,6 @@ REG2_TESTS = \
 	regress2/ooo.tag10.smt2 \
 	regress2/piVC_5581bd.smt2 \
 	regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 \
-	regress2/quantifiers/ForElimination-scala-9.smt2 \
 	regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 \
 	regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 \
 	regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 \
@@ -1958,6 +1958,7 @@ DISABLED_TESTS = \
 	regress2/bug396.smt2 \
 	regress2/nl/dumortier-050317.smt2 \
 	regress2/nl/nt-lemmas-bad.smt2 \
+	regress2/quantifiers/ForElimination-scala-9.smt2 \
 	regress2/quantifiers/small-bug1-fixpoint-3.smt2 \
 	regress2/xs-11-20-5-2-5-3.smt \
 	regress2/xs-11-20-5-2-5-3.smt2
diff --git a/test/regress/regress1/fmf/issue2034-preinit.smt2 b/test/regress/regress1/fmf/issue2034-preinit.smt2
new file mode 100644
index 000000000..e80e698fd
--- /dev/null
+++ b/test/regress/regress1/fmf/issue2034-preinit.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unknown
+(set-logic AUFLIRA)
+(set-info :status unknown)
+(declare-fun _substvar_1_ () Int)
+(declare-fun tptp_const_array1 (Int Real) (Array Int Real))
+(assert (forall ((?I_4 Int) (?L_5 Int) (?U_6 Int) (?Val_7 Real)) (=> true (= (select (tptp_const_array1 _substvar_1_ ?Val_7) 0) ?Val_7))))
+(check-sat)
\ No newline at end of file