From a3b9a99404ee00bde5db42aab63ab08df3712ba3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Feb 2020 17:28:03 -0600 Subject: [PATCH] Fixes for quantifiers documentation (#3811) Minor fixes discovered during development of sygus-inst. --- src/theory/quantifiers/quant_util.h | 3 ++- src/theory/quantifiers/sygus/synth_conjecture.h | 7 +++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 640a62780..723a56415 100644 --- 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 a4f4af2e8..126facfa8 100644 --- 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. */ -- 2.30.2