Refactoring of relevance vector in quantifiers (#3070)

2 files changed, 65 insertions, 61 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 8d29cb8e1..dbf368e66 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -32,19 +32,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-struct sortQuantifierRelevance {
-  FirstOrderModel * d_fm;
-  bool operator() (Node i, Node j) {
-    int wi = d_fm->getRelevanceValue( i );
-    int wj = d_fm->getRelevanceValue( j );
-    if( wi==wj ){
-      return i<j;
-    }else{
-      return wi<wj;
-    }
-  }
-};
-
 RepSetIterator::RsiEnumType QRepBoundExt::setBound(Node owner,
                                                    unsigned i,
                                                    std::vector<Node>& elements)
@@ -122,10 +109,13 @@ bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
   return false;
 }
 
-FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) :
-TheoryModel( c, name, true ),
-d_qe( qe ), d_forall_asserts( c ){
-  d_rlv_count = 0;
+FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe,
+                                 context::Context* c,
+                                 std::string name)
+    : TheoryModel(c, name, true),
+      d_qe(qe),
+      d_forall_asserts(c)
+{
 }
 
 void FirstOrderModel::assertQuantifier( Node n ){
@@ -232,32 +222,40 @@ bool FirstOrderModel::checkNeeded() {
 
 void FirstOrderModel::reset_round() {
   d_quant_active.clear();
-  
+
+  // compute which quantified formulas are asserted if necessary
+  std::map<Node, bool> qassert;
+  if (!d_forall_rlv_vec.empty())
+  {
+    Trace("fm-relevant-debug")
+        << "Mark asserted quantified formulas..." << std::endl;
+    for (const Node& q : d_forall_asserts)
+    {
+      qassert[q] = true;
+    }
+  }
   //order the quantified formulas
   d_forall_rlv_assert.clear();
   if( !d_forall_rlv_vec.empty() ){
     Trace("fm-relevant") << "Build sorted relevant list..." << std::endl;
-    Trace("fm-relevant-debug") << "Mark asserted quantified formulas..." << std::endl;
-    std::map< Node, bool > qassert;
-    for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
-      qassert[d_forall_asserts[i]] = true;
-    }
-    Trace("fm-relevant-debug") << "Sort the relevant quantified formulas..." << std::endl;
-    sortQuantifierRelevance sqr;
-    sqr.d_fm = this;
-    std::sort( d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), sqr );
     Trace("fm-relevant-debug") << "Add relevant asserted formulas..." << std::endl;
+    std::map<Node, bool>::iterator ita;
     for( int i=(int)(d_forall_rlv_vec.size()-1); i>=0; i-- ){
       Node q = d_forall_rlv_vec[i];
-      if( qassert.find( q )!=qassert.end() ){
-        Trace("fm-relevant") << "   " << d_forall_rlv[q] << " : " << q << std::endl;
+      ita = qassert.find(q);
+      if (ita != qassert.end())
+      {
+        Trace("fm-relevant") << "   " << q << std::endl;
         d_forall_rlv_assert.push_back( q );
+        qassert.erase(ita);
       }
     }
     Trace("fm-relevant-debug") << "Add remaining asserted formulas..." << std::endl;
-    for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
-      Node q = d_forall_asserts[i];
-      if( std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )==d_forall_rlv_assert.end() ){
+    for (const Node& q : d_forall_asserts)
+    {
+      // if we didn't include it above
+      if (qassert.find(q) != qassert.end())
+      {
         d_forall_rlv_assert.push_back( q );
       }else{
         Trace("fm-relevant-debug") << "...already included " << q << std::endl;
@@ -273,40 +271,36 @@ void FirstOrderModel::reset_round() {
 }
 
 void FirstOrderModel::markRelevant( Node q ) {
+  // Put q on the back of the vector d_forall_rlv_vec.
+  // If we were the last quantifier marked relevant, this is a no-op, return.
   if( q!=d_last_forall_rlv ){
     Trace("fm-relevant") << "Mark relevant : " << q << std::endl;
-    if( std::find( d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), q )==d_forall_rlv_vec.end() ){
-      d_forall_rlv_vec.push_back( q );
+    std::vector<Node>::iterator itr =
+        std::find(d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), q);
+    if (itr != d_forall_rlv_vec.end())
+    {
+      d_forall_rlv_vec.erase(itr, itr + 1);
     }
-    d_forall_rlv[ q ] = d_rlv_count;
-    d_rlv_count++;
+    d_forall_rlv_vec.push_back(q);
     d_last_forall_rlv = q;
   }
 }
 
-int FirstOrderModel::getRelevanceValue( Node q ) {
-  std::map< Node, unsigned >::iterator it = d_forall_rlv.find( q );
-  if( it==d_forall_rlv.end() ){
-    return -1;
-  }else{
-    return it->second;
-  }
-}
-
 void FirstOrderModel::setQuantifierActive( TNode q, bool active ) {
   d_quant_active[q] = active;
 }
 
-bool FirstOrderModel::isQuantifierActive( TNode q ) {
-  std::map< TNode, bool >::iterator it = d_quant_active.find( q );
+bool FirstOrderModel::isQuantifierActive(TNode q) const
+{
+  std::map<TNode, bool>::const_iterator it = d_quant_active.find(q);
   if( it==d_quant_active.end() ){
     return true;
-  }else{
-    return it->second;
   }
+  return it->second;
 }
 
-bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
+bool FirstOrderModel::isQuantifierAsserted(TNode q) const
+{
   Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
   return std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )!=d_forall_rlv_assert.end();
 }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index bdf1d7c15..27d21218d 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -17,9 +17,10 @@
 #ifndef CVC4__FIRST_ORDER_MODEL_H
 #define CVC4__FIRST_ORDER_MODEL_H
 
+#include "expr/attribute.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
-#include "expr/attribute.h"
 
 namespace CVC4 {
 namespace theory {
@@ -110,17 +111,28 @@ class FirstOrderModel : public TheoryModel
   void reset_round();
   /** mark quantified formula relevant */
   void markRelevant( Node q );
-  /** get relevance value */
-  int getRelevanceValue( Node q );
-  /** set quantified formula active/inactive 
-   * a quantified formula may be set inactive if for instance:
-   *   - it is entailed by other quantified formulas
+  /** set quantified formula active/inactive
+   *
+   * This indicates that quantified formula is "inactive", that is, it need
+   * not be considered during this instantiation round.
+   *
+   * A quantified formula may be set inactive if for instance:
+   *   - It is entailed by other quantified formulas, or
+   *   - All of its instances are known to be true in the current model.
+   *
+   * This method should be called after a call to FirstOrderModel::reset_round,
+   * and before calls to QuantifiersModule check calls. A common place to call
+   * this method is during QuantifiersModule reset_round calls.
    */
   void setQuantifierActive( TNode q, bool active );
-  /** is quantified formula active */
-  bool isQuantifierActive( TNode q );
+  /** is quantified formula active?
+   *
+   * Returns false if there has been a call to setQuantifierActive( q, false )
+   * during this instantiation round.
+   */
+  bool isQuantifierActive(TNode q) const;
   /** is quantified formula asserted */
-  bool isQuantifierAsserted( TNode q );
+  bool isQuantifierAsserted(TNode q) const;
   /** get model basis term */
   Node getModelBasisTerm(TypeNode tn);
   /** is model basis term */
@@ -156,8 +168,6 @@ class FirstOrderModel : public TheoryModel
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
   /** quantified formulas marked as relevant */
-  unsigned d_rlv_count;
-  std::map<Node, unsigned> d_forall_rlv;
   std::vector<Node> d_forall_rlv_vec;
   Node d_last_forall_rlv;
   std::vector<Node> d_forall_rlv_assert;