1 files changed, 56 insertions, 60 deletions
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index dbfae5382..172e93c12 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -39,66 +39,62 @@ namespace inst {
 class IMGenerator;
 class InstMatchGenerator;
 /** A collection of nodes representing a trigger.
-*
-* This class encapsulates all implementations of E-matching in CVC4.
-* Its primary use is as a utility of the quantifiers module InstantiationEngine
-* (see theory/quantifiers/ematching/instantiation_engine.h) which uses Trigger to make
-* appropriate calls to Instantiate::addInstantiation(...)
-* (see theory/instantiate.h) for the instantiate utility of the quantifiers
-* engine (d_quantEngine) associated with this trigger.  These calls
-* queue instantiation lemmas to the output channel of TheoryQuantifiers during
-* a full effort check.
-*
-* Concretely, a Trigger* t is used in the following way during a full effort
-* check. Assume that t is associated with quantified formula q (see field d_f).
-* We call :
-*
-* // setup initial information
-* t->resetInstantiationRound();
-* // will produce instantiations based on matching with all terms
-* t->reset( Node::null() );
-* // add all instantiations based on E-matching with this trigger and the
-* // current context
-* t->addInstantiations();
-*
-* This will result in (a set of) calls to
-* Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn),
-* where m1...mn are InstMatch objects. These calls add the corresponding
-* instantiation lemma for (q,mi) on the output channel associated with
-* d_quantEngine.
-*
-* The Trigger class is wrapper around an underlying IMGenerator class, which
-* implements various forms of E-matching for its set of nodes (d_nodes), which
-* is refered to in the literature as a "trigger". A trigger is a set of terms
-* whose free variables are the bound variables of a quantified formula q,
-* and that is used to guide instantiations for q (for example, see "Efficient
-* E-Matching for SMT Solvers" by de Moura et al).
-*
-* For example of an instantiation lemma produced by E-matching :
-*
-* quantified formula : forall x. P( x )
-*            trigger : P( x )
-*     ground context : ~P( a )
-*
-* Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a }
-* which is used to generate the instantiation lemma :
-*   (forall x. P( x )) => P( a )
-*
-* Terms that are provided as input to a Trigger class via mkTrigger
-* should be in "instantiation constant form", see TermUtil::getInstConstantNode.
-* Say we have quantified formula q whose AST is the Node
-*   (FORALL
-*     (BOUND_VAR_LIST x)
-*     (NOT (P x))
-*     (INST_PATTERN_LIST (INST_PATTERN (P x))))
-* then TermUtil::getInstConstantNode( q, (P x) ) = (P IC) where
-* IC = TermUtil::getInstantiationConstant( q, i ).
-* Trigger expects as input (P IC) to represent the Trigger (P x). This form
-* ensures that references to bound variables are unique to quantified formulas,
-* which is required to ensure the correctness of instantiation lemmas we
-* generate.
-*
-*/
+ *
+ * This class encapsulates all implementations of E-matching in cvc5.
+ * Its primary use is as a utility of the quantifiers module InstantiationEngine
+ * (see theory/quantifiers/ematching/instantiation_engine.h) which uses Trigger
+ * to make appropriate calls to Instantiate::addInstantiation(...) (see
+ * theory/instantiate.h) for the instantiate utility of the quantifiers engine
+ * (d_quantEngine) associated with this trigger.  These calls queue
+ * instantiation lemmas to the output channel of TheoryQuantifiers during a full
+ * effort check.
+ *
+ * Concretely, a Trigger* t is used in the following way during a full effort
+ * check. Assume that t is associated with quantified formula q (see field d_f).
+ * We call :
+ *
+ * // setup initial information
+ * t->resetInstantiationRound();
+ * // will produce instantiations based on matching with all terms
+ * t->reset( Node::null() );
+ * // add all instantiations based on E-matching with this trigger and the
+ * // current context
+ * t->addInstantiations();
+ *
+ * This will result in (a set of) calls to
+ * Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn),
+ * where m1...mn are InstMatch objects. These calls add the corresponding
+ * instantiation lemma for (q,mi) on the output channel associated with
+ * d_quantEngine.
+ *
+ * The Trigger class is wrapper around an underlying IMGenerator class, which
+ * implements various forms of E-matching for its set of nodes (d_nodes), which
+ * is refered to in the literature as a "trigger". A trigger is a set of terms
+ * whose free variables are the bound variables of a quantified formula q,
+ * and that is used to guide instantiations for q (for example, see "Efficient
+ * E-Matching for SMT Solvers" by de Moura et al).
+ *
+ * For example of an instantiation lemma produced by E-matching :
+ *
+ * quantified formula : forall x. P( x )
+ *            trigger : P( x )
+ *     ground context : ~P( a )
+ *
+ * Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a }
+ * which is used to generate the instantiation lemma :
+ *   (forall x. P( x )) => P( a )
+ *
+ * Terms that are provided as input to a Trigger class via mkTrigger
+ * should be in "instantiation constant form", see
+ * TermUtil::getInstConstantNode. Say we have quantified formula q whose AST is
+ * the Node (FORALL (BOUND_VAR_LIST x) (NOT (P x)) (INST_PATTERN_LIST
+ * (INST_PATTERN (P x)))) then TermUtil::getInstConstantNode( q, (P x) ) = (P
+ * IC) where IC = TermUtil::getInstantiationConstant( q, i ). Trigger expects as
+ * input (P IC) to represent the Trigger (P x). This form ensures that
+ * references to bound variables are unique to quantified formulas, which is
+ * required to ensure the correctness of instantiation lemmas we generate.
+ *
+ */
 class Trigger {
   friend class IMGenerator;