From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Aug 2019 20:25:26 +0000 (-0500)
Subject:  Move basic sygus enumerator to its own file (#3149)
X-Git-Tag: cvc5-1.0.0~4050
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ae83890dc38177f7c5c9cf07d7905ea7bf62d055;p=cvc5.git

 Move basic sygus enumerator to its own file (#3149)
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 68c22daef..30594e269 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -555,6 +555,8 @@ libcvc4_add_sources(
   theory/quantifiers/sygus/sygus_abduct.h
   theory/quantifiers/sygus/sygus_enumerator.cpp
   theory/quantifiers/sygus/sygus_enumerator.h
+  theory/quantifiers/sygus/sygus_enumerator_basic.cpp
+  theory/quantifiers/sygus/sygus_enumerator_basic.h
   theory/quantifiers/sygus/sygus_eval_unfold.cpp
   theory/quantifiers/sygus/sygus_eval_unfold.h
   theory/quantifiers/sygus/sygus_explain.cpp
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp
new file mode 100644
index 000000000..2e7b80429
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/*! \file sygus_enumerator_basic.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Haniel Barbosa, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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
+ **
+ ** \brief Implementation of sygus basic enumerator
+ **/
+#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
+
+#include "options/datatypes_options.h"
+
+using namespace CVC4::kind;
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+EnumValGeneratorBasic::EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn)
+    : d_tds(tds), d_te(tn)
+{
+}
+
+bool EnumValGeneratorBasic::increment()
+{
+  ++d_te;
+  if (d_te.isFinished())
+  {
+    d_currTerm = Node::null();
+    return false;
+  }
+  d_currTerm = *d_te;
+  if (options::sygusSymBreakDynamic())
+  {
+    Node nextb = d_tds->sygusToBuiltin(d_currTerm);
+    nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
+    if (d_cache.find(nextb) == d_cache.end())
+    {
+      d_cache.insert(nextb);
+      // only return the current term if not unique
+    }
+    else
+    {
+      d_currTerm = Node::null();
+    }
+  }
+  return true;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+} /* namespace CVC4 */
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
new file mode 100644
index 000000000..5336d898f
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
@@ -0,0 +1,70 @@
+/*********************                                                        */
+/*! \file sygus_enumerator_basic.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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
+ **
+ ** \brief Basic sygus enumerator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
+
+#include <map>
+#include <unordered_set>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** A basic sygus value generator
+ *
+ * This class is a "naive" term generator for sygus conjectures, which invokes
+ * the type enumerator to generate a stream of (all) sygus terms of a given
+ * type.
+ */
+class EnumValGeneratorBasic : public EnumValGenerator
+{
+ public:
+  EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn);
+  ~EnumValGeneratorBasic() {}
+  /** initialize (do nothing) */
+  void initialize(Node e) override {}
+  /** initialize (do nothing) */
+  void addValue(Node v) override { d_currTerm = *d_te; }
+  /**
+   * Get next returns the next (T-rewriter-unique) value based on the type
+   * enumerator.
+   */
+  bool increment() override;
+  /** get the current term */
+  Node getCurrent() override { return d_currTerm; }
+
+ private:
+  /** pointer to term database sygus */
+  TermDbSygus* d_tds;
+  /** the type enumerator */
+  TypeEnumerator d_te;
+  /** the current term */
+  Node d_currTerm;
+  /** cache of (enumerated) builtin values we have enumerated so far */
+  std::unordered_set<Node, NodeHashFunction> d_cache;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 756e1f791..ee5af62c9 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -29,6 +29,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/enum_stream_substitution.h"
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
+#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -733,63 +734,6 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
   return ret;
 }
 
-/** A basic sygus value generator
- *
- * This class is a "naive" term generator for sygus conjectures, which invokes
- * the type enumerator to generate a stream of (all) sygus terms of a given
- * type.
- */
-class EnumValGeneratorBasic : public EnumValGenerator
-{
- public:
-  EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn) : d_tds(tds), d_te(tn) {}
-  ~EnumValGeneratorBasic() {}
-  /** initialize (do nothing) */
-  void initialize(Node e) override {}
-  /** initialize (do nothing) */
-  void addValue(Node v) override { d_currTerm = *d_te; }
-  /**
-   * Get next returns the next (T-rewriter-unique) value based on the type
-   * enumerator.
-   */
-  bool increment() override
-  {
-    ++d_te;
-    if (d_te.isFinished())
-    {
-      d_currTerm = Node::null();
-      return false;
-    }
-    d_currTerm = *d_te;
-    if (options::sygusSymBreakDynamic())
-    {
-      Node nextb = d_tds->sygusToBuiltin(d_currTerm);
-      nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
-      if (d_cache.find(nextb) == d_cache.end())
-      {
-        d_cache.insert(nextb);
-        // only return the current term if not unique
-      }
-      else
-      {
-        d_currTerm = Node::null();
-      }
-    }
-    return true;
-  }
-  /** get the current term */
-  Node getCurrent() override { return d_currTerm; }
- private:
-  /** pointer to term database sygus */
-  TermDbSygus* d_tds;
-  /** the type enumerator */
-  TypeEnumerator d_te;
-  /** the current term */
-  Node d_currTerm;
-  /** cache of (enumerated) builtin values we have enumerated so far */
-  std::unordered_set<Node, NodeHashFunction> d_cache;
-};
-
 Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
 {
   bool isEnum = d_tds->isEnumerator(e);