Refactor mkRep option for instantiation (#8657)

This removes mkRep as an option for addInstantiation.

It adds a new interface for making term vectors representative, which is required for FMF instantiation.

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 37aeaedcb07acb04f3f7cef7219a5481af57ab04..7760b9391c7fb5bfed6169003fc4f80c8eb686d5 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -521,7 +521,6 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
                                   subs,
                                   InferenceId::QUANTIFIERS_INST_CEGQI,
                                   Node::null(),
-                                  false,
                                   usedVts))
   {
     return true;

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 3c5ec49acd4331ac02e5522d29d148696c396ade..c21ed4393e59efe674069519f197f7136111b60b 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -745,11 +745,9 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
       }
       // just add the instance
       d_triedLemmas++;
-      if (instq->addInstantiation(f,
-                                  inst,
-                                  InferenceId::QUANTIFIERS_INST_FMF_FMC,
-                                  Node::null(),
-                                  true))
+      instq->processInstantiationRep(f, inst);
+      if (instq->addInstantiation(
+              f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, Node::null()))
       {
         Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
         d_addedLemmas++;
@@ -898,11 +896,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm,
       if (ev!=d_true) {
         Trace("fmc-exh-debug") << ", add!";
         //add as instantiation
+        ie->processInstantiationRep(f, inst);
         if (ie->addInstantiation(f,
                                  inst,
                                  InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH,
-                                 Node::null(),
-                                 true))
+                                 Node::null()))
         {
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 7cb2a348b48cc6b06c84e091a38661168485451e..a295c30059068afedc0e783b4d41e0949335f2e5 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -266,18 +266,17 @@ int ModelEngine::checkModel(){
   return d_addedLemmas;
 }
 
-
-
-void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
+void ModelEngine::exhaustiveInstantiate(Node q, int effort)
+{
   //first check if the builder can do the exhaustive instantiation
   unsigned prev_alem = d_builder->getNumAddedLemmas();
   unsigned prev_tlem = d_builder->getNumTriedLemmas();
   FirstOrderModel* fm = d_treg.getModel();
-  int retEi = d_builder->doExhaustiveInstantiation(fm, f, effort);
+  int retEi = d_builder->doExhaustiveInstantiation(fm, q, effort);
   if( retEi!=0 ){
     if( retEi<0 ){
       Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
-      d_incompleteQuants.insert(f);
+      d_incompleteQuants.insert(q);
     }else{
       Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
     }
@@ -286,9 +285,10 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   }else{
     if( TraceIsOn("fmf-exh-inst-debug") ){
       Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
-      for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+      for (size_t i = 0, nchild = q[0].getNumChildren(); i < nchild; i++)
+      {
         Trace("fmf-exh-inst-debug")
-            << d_qreg.getInstantiationConstant(f, i) << " ";
+            << d_qreg.getInstantiationConstant(q, i) << " ";
       }
       Trace("fmf-exh-inst-debug") << std::endl;
     }
@@ -296,7 +296,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     QRepBoundExt qrbe(qbi, fm);
     RepSetIterator riter(fm->getRepSet(), &qrbe);
-    if( riter.setQuantifier( f ) ){
+    if (riter.setQuantifier(q))
+    {
       Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
       if( !riter.isIncomplete() ){
         int triedLemmas = 0;
@@ -306,20 +307,18 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
             !riter.isFinished()
             && (addedLemmas == 0 || !options().quantifiers.fmfOneInstPerRound))
         {
-          //instantiation was not shown to be true, construct the match
-          InstMatch m( f );
-          for (unsigned i = 0; i < riter.getNumTerms(); i++)
-          {
-            m.set(d_qstate, i, riter.getCurrentTerm(i));
-          }
-          Trace("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+          // instantiation was not shown to be true, construct the term vector
+          std::vector<Node> terms;
+          riter.getCurrentTerms(terms);
+          Trace("fmf-model-eval")
+              << "* Add instantiation " << terms << std::endl;
           triedLemmas++;
           //add as instantiation
-          if (inst->addInstantiation(f,
-                                     m.d_vals,
+          inst->processInstantiationRep(q, terms);
+          if (inst->addInstantiation(q,
+                                     terms,
                                      InferenceId::QUANTIFIERS_INST_FMF_EXH,
-                                     Node::null(),
-                                     true))
+                                     Node::null()))
           {
             addedLemmas++;
             if (d_qstate.isInConflict())
@@ -327,19 +326,23 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
               break;
             }
           }else{
-            Trace("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+            Trace("fmf-model-eval")
+                << "* Failed Add instantiation " << terms << std::endl;
           }
           riter.increment();
         }
         d_addedLemmas += addedLemmas;
         d_triedLemmas += triedLemmas;
       }
-    }else{
+    }
+    else
+    {
       Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-    if( riter.isIncomplete() ){
-      d_incompleteQuants.insert(f);
+    if (riter.isIncomplete())
+    {
+      d_incompleteQuants.insert(q);
     }
   }
 }

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 7fa845d35246ba1a814108a38cbadb57c32960bb..23abba94aca320fc3145c9f345c2e2a08fcc9cc7 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -101,19 +101,28 @@ bool Instantiate::addInstantiation(Node q,
                                    std::vector<Node>& terms,
                                    InferenceId id,
                                    Node pfArg,
-                                   bool mkRep,
                                    bool doVts)
 {
   // For resource-limiting (also does a time check).
   d_qim.safePoint(Resource::QuantifierStep);
   Assert(!d_qstate.isInConflict());
+  Assert(q.getKind() == FORALL);
   Assert(terms.size() == q[0].getNumChildren());
-  Trace("inst-add-debug") << "For quantified formula " << q
-                          << ", add instantiation: " << std::endl;
-  for (unsigned i = 0, size = terms.size(); i < size; i++)
+  if (TraceIsOn("inst-add-debug"))
+  {
+    Trace("inst-add-debug") << "For quantified formula " << q
+                            << ", add instantiation: " << std::endl;
+    for (size_t i = 0, size = terms.size(); i < size; i++)
+    {
+      Trace("inst-add-debug") << "  " << q[0][i];
+      Trace("inst-add-debug") << " -> " << terms[i];
+      Trace("inst-add-debug") << std::endl;
+    }
+    Trace("inst-add-debug") << "id is " << id << std::endl;
+  }
+  // ensure the terms are non-null and well-typed
+  for (size_t i = 0, size = terms.size(); i < size; i++)
   {
-    Trace("inst-add-debug") << "  " << q[0][i];
-    Trace("inst-add-debug2") << " -> " << terms[i];
     TypeNode tn = q[0][i].getType();
     if (terms[i].isNull())
     {
@@ -123,13 +132,6 @@ bool Instantiate::addInstantiation(Node q,
     // are cast to integers for { x -> t } where x has type Int and t has
     // type Real.
     terms[i] = ensureType(terms[i], tn);
-    if (mkRep)
-    {
-      // pick the best possible representative for instantiation, based on past
-      // use and simplicity of term
-      terms[i] = d_treg.getModel()->getInternalRepresentative(terms[i], q, i);
-    }
-    Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
     if (terms[i].isNull())
     {
       Trace("inst-add-debug")
@@ -137,7 +139,12 @@ bool Instantiate::addInstantiation(Node q,
           << std::endl;
       return false;
     }
+  }
 #ifdef CVC5_ASSERTIONS
+  for (size_t i = 0, size = terms.size(); i < size; i++)
+  {
+    TypeNode tn = q[0][i].getType();
+    Assert(!terms[i].isNull());
     bool bad_inst = false;
     if (TermUtil::containsUninterpretedConstant(terms[i]))
     {
@@ -181,9 +188,8 @@ bool Instantiate::addInstantiation(Node q,
       }
       Assert(false);
     }
-#endif
   }
-  Trace("inst-add-debug") << "id is " << id << std::endl;
+#endif
 
   EntailmentCheck* ec = d_treg.getEntailmentCheck();
   // Note we check for entailment before checking for term vector duplication.
@@ -220,7 +226,7 @@ bool Instantiate::addInstantiation(Node q,
   if (options().quantifiers.instMaxLevel != -1)
   {
     TermDb* tdb = d_treg.getTermDatabase();
-    for (Node& t : terms)
+    for (const Node& t : terms)
     {
       if (!tdb->isTermEligibleForInstantiation(t, q))
       {
@@ -349,7 +355,7 @@ bool Instantiate::addInstantiation(Node q,
   if (TraceIsOn("inst"))
   {
     Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
-    for (unsigned i = 0, size = terms.size(); i < size; i++)
+    for (size_t i = 0, size = terms.size(); i < size; i++)
     {
       if (TraceIsOn("inst"))
       {
@@ -395,16 +401,30 @@ bool Instantiate::addInstantiation(Node q,
   return true;
 }
 
+void Instantiate::processInstantiationRep(Node q, std::vector<Node>& terms)
+{
+  Assert(q.getKind() == FORALL);
+  Assert(terms.size() == q[0].getNumChildren());
+  for (size_t i = 0, size = terms.size(); i < size; i++)
+  {
+    Assert(!terms[i].isNull());
+    // pick the best possible representative for instantiation, based on past
+    // use and simplicity of term
+    terms[i] = d_treg.getModel()->getInternalRepresentative(terms[i], q, i);
+    // Note it may be a null representative here, it is then replaced
+    // by an arbitrary term if necessary during addInstantiation.
+  }
+}
+
 bool Instantiate::addInstantiationExpFail(Node q,
                                           std::vector<Node>& terms,
                                           std::vector<bool>& failMask,
                                           InferenceId id,
                                           Node pfArg,
-                                          bool mkRep,
                                           bool doVts,
                                           bool expFull)
 {
-  if (addInstantiation(q, terms, id, pfArg, mkRep, doVts))
+  if (addInstantiation(q, terms, id, pfArg, doVts))
   {
     return true;
   }

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index e41740eda816c38fb9c110e88e07e17c289e8ceb..81f0d8af5aa13e5b82f0c41c9d1e06ff09ae2ac6 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -141,8 +141,6 @@ class Instantiate : public QuantifiersUtil
    * manager
    * @param pfArg an additional node to add to the arguments of the INSTANTIATE
    * step
-   * @param mkRep whether to take the representatives of the terms in the
-   * range of the substitution m,
    * @param doVts whether we must apply virtual term substitution to the
    * instantiation lemma.
    *
@@ -162,7 +160,6 @@ class Instantiate : public QuantifiersUtil
                         std::vector<Node>& terms,
                         InferenceId id,
                         Node pfArg = Node::null(),
-                        bool mkRep = false,
                         bool doVts = false);
   /**
    * Same as above, but we also compute a vector failMask indicating which
@@ -192,9 +189,13 @@ class Instantiate : public QuantifiersUtil
                                std::vector<bool>& failMask,
                                InferenceId id,
                                Node pfArg = Node::null(),
-                               bool mkRep = false,
                                bool doVts = false,
                                bool expFull = true);
+  /**
+   * Ensure each term in terms is the chosen representative for its
+   * corresponding variable in q.
+   */
+  void processInstantiationRep(Node q, std::vector<Node>& terms);
   /** record instantiation
    *
    * Explicitly record that q has been instantiated with terms, with virtual