Refactor relevance vectors for asserted quantifiers (#3666)

4 files changed, 39 insertions, 12 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index bfef42b65..2b7f78008 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -38,7 +38,8 @@ FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe,
                                  std::string name)
     : TheoryModel(c, name, true),
       d_qe(qe),
-      d_forall_asserts(c)
+      d_forall_asserts(c),
+      d_forallRlvComputed(false)
 {
 }
 
@@ -55,12 +56,13 @@ unsigned FirstOrderModel::getNumAssertedQuantifiers() {
 }
 
 Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) { 
-  if( !ordered ){
+  if( !ordered || !d_forallRlvComputed ){
     return d_forall_asserts[i]; 
-  }else{
-    Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
-    return d_forall_rlv_assert[i];
   }
+  // If we computed the relevant forall assertion vector, in reset_round,
+  // then it should have the same size as the default assertion vector.
+  Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
+  return d_forall_rlv_assert[i];
 }
 
 void FirstOrderModel::initialize() {
@@ -160,7 +162,9 @@ void FirstOrderModel::reset_round() {
   }
   //order the quantified formulas
   d_forall_rlv_assert.clear();
+  d_forallRlvComputed = false;
   if( !d_forall_rlv_vec.empty() ){
+    d_forallRlvComputed = true;
     Trace("fm-relevant") << "Build sorted relevant list..." << std::endl;
     Trace("fm-relevant-debug") << "Add relevant asserted formulas..." << std::endl;
     std::map<Node, bool>::iterator ita;
@@ -187,10 +191,6 @@ void FirstOrderModel::reset_round() {
     }
     Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl;
     Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
-  }else{
-    for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
-      d_forall_rlv_assert.push_back( d_forall_asserts[i] );
-    }
   }
 }
 
@@ -225,8 +225,7 @@ bool FirstOrderModel::isQuantifierActive(TNode q) const
 
 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();
+  return std::find( d_forall_asserts.begin(), d_forall_asserts.end(), q )!=d_forall_asserts.end();
 }
 
 Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index a113d1b1b..ab1f7c768 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -132,10 +132,31 @@ class FirstOrderModel : public TheoryModel
   QuantifiersEngine* d_qe;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
-  /** quantified formulas marked as relevant */
+  /** 
+   * The (ordered) list of quantified formulas marked as relevant using
+   * markRelevant, where the quantified formula q in the most recent
+   * call to markRelevant comes last in the list.
+   */
   std::vector<Node> d_forall_rlv_vec;
+  /** The last quantified formula marked as relevant, if one exists. */
   Node d_last_forall_rlv;
+  /** 
+   * The list of asserted quantified formulas, ordered by relevance.
+   * Relevance is a dynamic partial ordering where q1 < q2 if there has been
+   * a call to markRelevant( q1 ) after the last call to markRelevant( q2 )
+   * (or no call to markRelevant( q2 ) has been made). 
+   * 
+   * This list is used primarily as an optimization for conflict-based
+   * instantiation so that quantifed formulas that have been instantiated
+   * most recently are processed first, since these are (statistically) more
+   * likely to have conflicting instantiations.
+   */
   std::vector<Node> d_forall_rlv_assert;
+  /** 
+   * Whether the above list has been computed. This flag is updated during
+   * reset_round and is valid within a full effort check.
+   */
+  bool d_forallRlvComputed;
   /** get variable id */
   std::map<Node, std::map<Node, int> > d_quant_var_id;
   /** process initialize model for term */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e49af0a83..e64bafe5f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1436,6 +1436,7 @@ set(regress_1_tests
   regress1/quantifiers/issue3481.smt2
   regress1/quantifiers/issue3537.smt2
   regress1/quantifiers/issue3628.smt2
+  regress1/quantifiers/issue3664.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2
diff --git a/test/regress/regress1/quantifiers/issue3664.smt2 b/test/regress/regress1/quantifiers/issue3664.smt2
new file mode 100644
index 000000000..28e999604
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue3664.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --fmf-fun-rlv --sygus-inference
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-fun a () Real)
+(assert (= (/ a a) 1.0))
+(check-sat)