From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 27 Oct 2019 22:47:56 +0000 (-0500)
Subject: Fix collect model info for higher-order (#3409)
X-Git-Tag: cvc5-1.0.0~3872
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3af2dfea22aae0d527fcfa93600c451b323c15b7;p=cvc5.git

Fix collect model info for higher-order (#3409)

This ensures we add lemmas when collect model info fails for the higher order extension of UF. This fixes #3405 (that benchmark now answers unknown).
---

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index d3fde58a7..7a2a9ae16 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -301,12 +301,17 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
                          << std::endl;
   if (!d_te->collectModelInfo(tm))
   {
+    Trace("model-builder")
+        << "TheoryEngineModelBuilder: fail collect model info" << std::endl;
     return false;
   }
 
   // model-builder specific initialization
   if (!preProcessBuildModel(tm))
   {
+    Trace("model-builder")
+        << "TheoryEngineModelBuilder: fail preprocess build model."
+        << std::endl;
     return false;
   }
 
@@ -813,9 +818,11 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
   // modelBuilder-specific initialization
   if (!processBuildModel(tm))
   {
+    Trace("model-builder")
+        << "TheoryEngineModelBuilder: fail process build model." << std::endl;
     return false;
   }
-
+  Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl;
   tm->d_modelBuiltSuccess = true;
   return true;
 }
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 88b2ba8d2..0ca9b151f 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -186,6 +186,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
 unsigned HoExtension::checkExtensionality(TheoryModel* m)
 {
   eq::EqualityEngine* ee = d_parent.getEqualityEngine();
+  NodeManager* nm = NodeManager::currentNM();
   unsigned num_lemmas = 0;
   bool isCollectModel = (m != nullptr);
   Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel="
@@ -243,6 +244,11 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
                 << "Add extensionality deq to model : " << edeq << std::endl;
             if (!m->assertEquality(edeq[0][0], edeq[0][1], false))
             {
+              Node eq = edeq[0][0].eqNode(edeq[0][1]);
+              Node lem = nm->mkNode(OR, deq.negate(), eq);
+              Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
+                             << std::endl;
+              d_parent.getOutputChannel().lemma(lem);
               return 1;
             }
           }
@@ -423,6 +429,10 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
     Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n);
     if (!m->assertEquality(n, hn, true))
     {
+      Node eq = n.eqNode(hn);
+      Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
+                     << std::endl;
+      d_parent.getOutputChannel().lemma(eq);
       return false;
     }
   }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 6284ae31e..76e6e08bc 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -324,6 +324,7 @@ bool TheoryUF::collectModelInfo(TheoryModel* m)
 
   if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
   {
+    Trace("uf") << "Collect model info fail UF" << std::endl;
     return false;
   }
 
@@ -332,6 +333,7 @@ bool TheoryUF::collectModelInfo(TheoryModel* m)
     // function equivalence classes.
     if (!d_ho->collectModelInfoHo(termSet, m))
     {
+      Trace("uf") << "Collect model info fail HO" << std::endl;
       return false;
     }
   }