From b7bbe9a3bc30f41d1775a187ccc732aaeb41eaa1 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Sep 2020 16:01:11 -0500
Subject: Move finite model minimization to UF last call effort (#5050)

This moves model minimization happen in TheoryUF's last call effort check instead of being a custom call in quantifiers finite model finding. This is both a better design and avoids bugs when quantifiers are not enabled (for QF_UF+cardinality constraints).

Fixes #4850.
---
 src/theory/quantifiers/fmf/model_engine.cpp | 33 ++++++++---------------------
 1 file changed, 9 insertions(+), 24 deletions(-)

(limited to 'src/theory/quantifiers/fmf')

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 879bfd1c1..3cf90069f 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -24,9 +24,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
-#include "theory/uf/cardinality_extension.h"
 #include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf.h"
 
 using namespace std;
 using namespace CVC4;
@@ -79,7 +77,6 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e)
   if( doCheck ){
     Assert(!d_quantEngine->inConflict());
     int addedLemmas = 0;
-    FirstOrderModel* fm = d_quantEngine->getModel();
 
     //the following will test that the model satisfies all asserted universal quantifiers by
     // (model-based) exhaustive instantiation.
@@ -88,28 +85,16 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e)
       Trace("model-engine") << "---Model Engine Round---" << std::endl;
       clSet = double(clock())/double(CLOCKS_PER_SEC);
     }
-
-    Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
-    // Let the cardinality extension verify that the model is minimal.
-    // This will if there are terms in the model that the cardinality extension
-    // was not notified of.
-    uf::CardinalityExtension* ufss =
-        static_cast<uf::TheoryUF*>(
-            d_quantEngine->getTheoryEngine()->theoryOf(THEORY_UF))
-            ->getCardinalityExtension();
-    if( !ufss || ufss->debugModel( fm ) ){
-      Trace("model-engine-debug") << "Check model..." << std::endl;
-      d_incomplete_check = false;
-      //print debug
-      if( Trace.isOn("fmf-model-complete") ){
-        Trace("fmf-model-complete") << std::endl;
-        debugPrint("fmf-model-complete");
-      }
-      //successfully built an acceptable model, now check it
-      addedLemmas += checkModel();
-    }else{
-      addedLemmas++;
+    Trace("model-engine-debug") << "Check model..." << std::endl;
+    d_incomplete_check = false;
+    // print debug
+    if (Trace.isOn("fmf-model-complete"))
+    {
+      Trace("fmf-model-complete") << std::endl;
+      debugPrint("fmf-model-complete");
     }
+    // successfully built an acceptable model, now check it
+    addedLemmas += checkModel();
 
     if( Trace.isOn("model-engine") ){
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-- 
cgit v1.2.3