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.

9 files changed, 57 insertions, 45 deletions

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);
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index f22a652c0..d5f9f4d0b 100644
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -130,5 +130,7 @@ bool TheoryState::isSatLiteral(TNode lit) const
   return d_valuation.isSatLiteral(lit);
 }
 
+TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 4ae381e78..633937991 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -74,6 +74,11 @@ class TheoryState
 
   /** Returns true if lit is a SAT literal. */
   virtual bool isSatLiteral(TNode lit) const;
+  /**
+   * Returns pointer to model. This model is only valid during last call effort
+   * check.
+   */
+  TheoryModel* getModel();
 
  protected:
   /** Pointer to the SAT context object used by the theory. */
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index b35efc23a..4f9483667 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1182,7 +1182,9 @@ void SortModel::debugPrint( const char* c ){
   }
 }
 
-bool SortModel::debugModel( TheoryModel* m ){
+bool SortModel::checkLastCall()
+{
+  TheoryModel* m = d_state.getModel();
   if( Trace.isOn("uf-ss-warn") ){
     std::vector< Node > eqcs;
     eq::EqClassesIterator eqcs_i =
@@ -1572,6 +1574,18 @@ bool CardinalityExtension::areDisequal(Node a, Node b)
 /** check */
 void CardinalityExtension::check(Theory::Effort level)
 {
+  if (level == Theory::EFFORT_LAST_CALL)
+  {
+    // if last call, call last call check for each sort
+    for (std::pair<const TypeNode, SortModel*>& r : d_rep_model)
+    {
+      if (!r.second->checkLastCall())
+      {
+        break;
+      }
+    }
+    return;
+  }
   if (!d_state.isInConflict())
   {
     if (options::ufssMode() == options::UfssMode::FULL)
@@ -1750,16 +1764,6 @@ void CardinalityExtension::debugPrint(const char* c)
   }
 }
 
-bool CardinalityExtension::debugModel(TheoryModel* m)
-{
-  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-    if( !it->second->debugModel( m ) ){
-      return false;
-    }
-  }
-  return true;
-}
-
 /** initialize */
 void CardinalityExtension::initializeCombinedCardinality()
 {
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 4c2707c17..d75b6d62d 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -327,8 +327,15 @@ class CardinalityExtension
     int getMaximumNegativeCardinality() { return d_maxNegCard.get(); }
     //print debug
     void debugPrint( const char* c );
-    /** debug a model */
-    bool debugModel( TheoryModel* m );
+    /**
+     * Check at last call effort. This will verify that the model is minimal.
+     * This return lemmas if there are terms in the model that the cardinality
+     * extension was not notified of.
+     *
+     * @return false if current model is not minimal. In this case, lemmas are
+     * sent on the output channel of the UF theory.
+     */
+    bool checkLastCall();
     /** get number of regions (for debugging) */
     int getNumRegions();
 
@@ -387,8 +394,6 @@ class CardinalityExtension
   std::string identify() const { return std::string("CardinalityExtension"); }
   //print debug
   void debugPrint( const char* c );
-  /** debug a model */
-  bool debugModel( TheoryModel* m );
   /** get cardinality for node */
   int getCardinality( Node n );
   /** get cardinality for type */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 0a48d4c71..18ab70d46 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -125,6 +125,12 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
 
 //--------------------------------- standard check
 
+bool TheoryUF::needsCheckLastEffort()
+{
+  // last call effort needed if using finite model finding
+  return d_thss != nullptr;
+}
+
 void TheoryUF::postCheck(Effort level)
 {
   if (d_state.isInConflict())
@@ -136,7 +142,7 @@ void TheoryUF::postCheck(Effort level)
   {
     d_thss->check(level);
   }
-  // check with the higher-order extension
+  // check with the higher-order extension at full effort
   if (!d_state.isInConflict() && fullEffort(level))
   {
     if (options::ufHo())
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 4a8369483..86c1b62c8 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -158,6 +158,8 @@ private:
   //--------------------------------- end initialization
 
   //--------------------------------- standard check
+  /** Do we need a check call at last call effort? */
+  bool needsCheckLastEffort() override;
   /** Post-check, called after the fact queue of the theory is processed. */
   void postCheck(Effort level) override;
   /** Pre-notify fact, return true if processed. */
@@ -187,10 +189,6 @@ private:
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
   std::string identify() const override { return "THEORY_UF"; }
-
-  /** get a pointer to the uf with cardinality */
-  CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
-
  private:
   /** Explain why this literal is true by building an explanation */
   void explain(TNode literal, Node& exp);
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index dc12d030d..d7d711b65 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -107,7 +107,8 @@ public:
   Node getModelValue(TNode var);
 
   /**
-   * Returns pointer to model.
+   * Returns pointer to model. This model is only valid during last call effort
+   * check.
    */
   TheoryModel* getModel();
 
diff --git a/test/regress/regress0/fmf/issue4850-force-card.smt2 b/test/regress/regress0/fmf/issue4850-force-card.smt2
new file mode 100644
index 000000000..5aa7fc894
--- /dev/null
+++ b/test/regress/regress0/fmf/issue4850-force-card.smt2
@@ -0,0 +1,6 @@
+(set-logic UFC)
+(set-info :status sat)
+(declare-sort a 0)
+(declare-fun b () a)
+(assert (not (fmf.card b 1)))
+(check-sat)