Fixes for quantifiers documentation (#3811)

Minor fixes discovered during development of sygus-inst.

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 640a62780ace88a7824e5ebd3a183a534d41d209..723a564152baeb13edf75d6f7cec04d604f1a146 100644 (file)
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -119,7 +119,8 @@ class QuantifiersModule {
    *
    * Called once for new quantified formulas q that are pre-registered by the
    * quantifiers theory, after internal ownership of quantified formulas is
-   * finalized. This does context-dependent initialization of this module.
+   * finalized. This does context-independent initialization of this module
+   * for quantified formula q.
    */
   virtual void registerQuantifier(Node q) {}
   /** Pre-register quantifier

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index a4f4af2e8674cb64fc65055ba84f165b6cb2904d..126facfa8704a31f37505f2513c550c2034eb1a5 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -59,6 +59,13 @@ class EnumValGenerator
    * Increment this value generator. If this returns false, then we are out of
    * values. If this returns true, getCurrent(), if non-null, returns the
    * current term.
+   *
+   * Notice that increment() may return true and afterwards it may be the case
+   * getCurrent() is null. We do this so that increment() does not take too
+   * much time per call, which can be the case for grammars where it is
+   * difficult to find the next (non-redundant) term. Returning true with
+   * a null current term gives the caller the chance to interleave other
+   * reasoning.
    */
   virtual bool increment() = 0;
   /** Get the current concrete value generated by this class. */