Do not exhaustive instantiation when FMF is disabled (#6899)

This makes FMF not handle quantified formulas when FMF options are disabled, apart from those marked internal.

This is required for combinations of sequences + quantified formulas.

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 5eba4665715405ffd74f5b9c556cc81e6d72b0e8..747b0621fe7d3a87794d2e88e91b6c47e721ac8a 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -103,7 +103,9 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e)
     }
 
     if( addedLemmas==0 ){
-      Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl;
+      Trace("model-engine-debug")
+          << "No lemmas added, incomplete = "
+          << (d_incomplete_check || !d_incompleteQuants.empty()) << std::endl;
       // cvc5 will answer SAT or unknown
       if( Trace.isOn("fmf-consistent") ){
         Trace("fmf-consistent") << std::endl;
@@ -124,7 +126,7 @@ bool ModelEngine::checkComplete(IncompleteId& incId)
 }
 
 bool ModelEngine::checkCompleteFor( Node q ) {
-  return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end();
+  return d_incompleteQuants.find(q) == d_incompleteQuants.end();
 }
 
 void ModelEngine::registerQuantifier( Node f ){
@@ -151,10 +153,6 @@ void ModelEngine::registerQuantifier( Node f ){
   }
 }
 
-void ModelEngine::assertNode( Node f ){
-
-}
-
 int ModelEngine::checkModel(){
   FirstOrderModel* fm = d_treg.getModel();
 
@@ -194,7 +192,7 @@ int ModelEngine::checkModel(){
   if( Trace.isOn("model-engine") ){
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node f = fm->getAssertedQuantifier( i );
-      if (fm->isQuantifierActive(f) && d_qreg.hasOwnership(f, this))
+      if (fm->isQuantifierActive(f) && shouldProcess(f))
       {
         int totalInst = 1;
         for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
@@ -216,20 +214,26 @@ int ModelEngine::checkModel(){
                   ? 2
                   : (options::mbqiMode() == options::MbqiMode::TRUST ? 0 : 1);
   for( int e=0; e<e_max; e++) {
-    d_incomplete_quants.clear();
+    d_incompleteQuants.clear();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node q = fm->getAssertedQuantifier( i, true );
       Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
       //determine if we should check this quantifier
-      if (fm->isQuantifierActive(q) && d_qreg.hasOwnership(q, this))
+      if (!fm->isQuantifierActive(q))
       {
-        exhaustiveInstantiate( q, e );
-        if (d_qstate.isInConflict())
-        {
-          break;
-        }
-      }else{
         Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
+        continue;
+      }
+      if (!shouldProcess(q))
+      {
+        Trace("fmf-exh-inst") << "-> Not processed : " << q << std::endl;
+        d_incompleteQuants.insert(q);
+        continue;
+      }
+      exhaustiveInstantiate(q, e);
+      if (d_qstate.isInConflict())
+      {
+        break;
       }
     }
     if( d_addedLemmas>0 ){
@@ -262,7 +266,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   if( retEi!=0 ){
     if( retEi<0 ){
       Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
-      d_incomplete_quants.push_back( f );
+      d_incompleteQuants.insert(f);
     }else{
       Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
     }
@@ -318,7 +322,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
     if( riter.isIncomplete() ){
-      d_incomplete_quants.push_back( f );
+      d_incompleteQuants.insert(f);
     }
   }
 }
@@ -348,6 +352,23 @@ void ModelEngine::debugPrint( const char* c ){
   }
 }
 
+bool ModelEngine::shouldProcess(Node q)
+{
+  if (!d_qreg.hasOwnership(q, this))
+  {
+    return false;
+  }
+  // if finite model finding or fmf bound is on, we process everything
+  if (options::finiteModelFind() || options::fmfBound())
+  {
+    return true;
+  }
+  // otherwise, we are only using model-based instantiation for internal
+  // quantified formulas
+  QuantAttributes& qattr = d_qreg.getQuantAttributes();
+  return qattr.isInternal(q);
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 89150bda4f0805326798061a83077e193b748c9f..f818a63621a06c40676de03d6d5235c169e51304 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -38,8 +38,6 @@ private:
   //temporary statistics
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;
-  // set of quantified formulas for which check was incomplete
-  std::vector< Node > d_incomplete_quants;
   int d_addedLemmas;
   int d_triedLemmas;
   int d_totalLemmas;
@@ -59,15 +57,18 @@ public:
  bool checkComplete(IncompleteId& incId) override;
  bool checkCompleteFor(Node q) override;
  void registerQuantifier(Node f) override;
- void assertNode(Node f) override;
  Node explain(TNode n) { return Node::null(); }
  void debugPrint(const char* c);
  /** Identify this module */
  std::string identify() const override { return "ModelEngine"; }
 
 private:
+ /** Should we process quantified formula q? */
+ bool shouldProcess(Node q);
  /** Pointer to the model builder of quantifiers engine */
  QModelBuilder* d_builder;
+ /** set of quantified formulas for which check was incomplete */
+ std::unordered_set<Node> d_incompleteQuants;
 };/* class ModelEngine */
 
 }  // namespace quantifiers