Merge branch 'master' into docsLinkdocsLink

1 files changed, 1 insertions, 31 deletions

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index e6645ddf2..04999da0d 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/cegis_core_connective.h"
 #include "theory/quantifiers/sygus/cegis_unif.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
 #include "theory/quantifiers/sygus/example_eval_cache.h"
 #include "theory/quantifiers/sygus/example_infer.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
@@ -42,37 +43,6 @@ class CegGrammarConstructor;
 class SygusPbe;
 class SygusStatistics;
 
-/**
- * A base class for generating values for actively-generated enumerators.
- * At a high level, the job of this class is to accept a stream of "abstract
- * values" a1, ..., an, ..., and generate a (possibly larger) stream of
- * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, ....
- */
-class EnumValGenerator
-{
- public:
-  virtual ~EnumValGenerator() {}
-  /** initialize this class with enumerator e */
-  virtual void initialize(Node e) = 0;
-  /** Inform this generator that abstract value v was enumerated. */
-  virtual void addValue(Node v) = 0;
-  /**
-   * 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. */
-  virtual Node getCurrent() = 0;
-};
-
 /** a synthesis conjecture
  * This class implements approaches for a synthesis conjecture, given by data
  * member d_quant.