Require that FMF model basis terms are variables (#3031)

The commit fixes an issue where FMF could theoretically chose interpreted function applications as "model basis terms". This triggered an incorrect model (caught by an AlwaysAssert) when the interpreted function later did not appear in a model and was chosen by FMF to be equal to a wrong value.

3 files changed, 23 insertions, 11 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 5428d9f1a..8d29cb8e1 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -328,7 +328,11 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
       }
       else
       {
-        mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
+        // The model basis term cannot be an interpreted function, or else we
+        // may produce an inconsistent model by choosing an arbitrary
+        // equivalence class for it. Hence, we require that it be an existing or
+        // fresh variable.
+        mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
       }
     }
     ModelBasisAttribute mba;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index c4b10eb6f..989609a76 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -113,19 +113,26 @@ Node TermDb::getTypeGroundTerm(TypeNode tn, unsigned i) const
   }
 }
 
-Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn)
+Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar)
 {
   std::map<TypeNode, std::vector<Node> >::const_iterator it =
       d_type_map.find(tn);
   if (it != d_type_map.end())
   {
     Assert(!it->second.empty());
-    return it->second[0];
-  }
-  else
-  {
-    return getOrMakeTypeFreshVariable(tn);
+    if (!reqVar)
+    {
+      return it->second[0];
+    }
+    for (const Node& v : it->second)
+    {
+      if (v.isVar())
+      {
+        return v;
+      }
+    }
   }
+  return getOrMakeTypeFreshVariable(tn);
 }
 
 Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index cd5c27f0d..d58d33673 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -108,10 +108,11 @@ class TermDb : public QuantifiersUtil {
   */
   Node getTypeGroundTerm(TypeNode tn, unsigned i) const;
   /** get or make ground term
-  * Returns the first ground term of type tn,
-  * or makes one if none exist.
-  */
-  Node getOrMakeTypeGroundTerm(TypeNode tn);
+   *
+   * Returns the first ground term of type tn, or makes one if none exist. If
+   * reqVar is true, then the ground term must be a variable.
+   */
+  Node getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar = false);
   /** make fresh variable
   * Returns a fresh variable of type tn.
   * This will return only a single fresh