Update copyright headers.

[cvc5.git] / src / theory / quantifiers / first_order_model.h

diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 27d21218da59f3564d21d51670c9db6d3117fbc3..4e1ef6d7f18f5582169b69f1fdbf8322471dd38a 100644 (file)
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Paul Meng, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -18,7 +18,6 @@
 #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"
 
@@ -50,40 +49,6 @@ namespace fmcheck {
 struct IsStarAttributeId {};
 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
 
-/** Quantifiers representative bound
- *
- * This class is used for computing (finite)
- * bounds for the domain of a quantifier
- * in the context of a RepSetIterator
- * (see theory/rep_set.h).
- */
-class QRepBoundExt : public RepBoundExt
-{
- public:
-  QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
-  virtual ~QRepBoundExt() {}
-  /** set bound */
-  RepSetIterator::RsiEnumType setBound(Node owner,
-                                       unsigned i,
-                                       std::vector<Node>& elements) override;
-  /** reset index */
-  bool resetIndex(RepSetIterator* rsi,
-                  Node owner,
-                  unsigned i,
-                  bool initial,
-                  std::vector<Node>& elements) override;
-  /** initialize representative set for type */
-  bool initializeRepresentativesForType(TypeNode tn) override;
-  /** get variable order */
-  bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
-
- private:
-  /** quantifiers engine associated with this bound */
-  QuantifiersEngine* d_qe;
-  /** indices that are bound integer enumeration */
-  std::map<unsigned, bool> d_bound_int;
-};
-
 // TODO (#1301) : document and refactor this class
 class FirstOrderModel : public TheoryModel
 {
@@ -167,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 */