Work towards integrating the enumerator callback into the fast enumerator.
theory/quantifiers/sygus/cegis_core_connective.h
theory/quantifiers/sygus/cegis_unif.cpp
theory/quantifiers/sygus/cegis_unif.h
+ theory/quantifiers/sygus/enum_val_generator.h
theory/quantifiers/sygus/example_eval_cache.cpp
theory/quantifiers/sygus/example_eval_cache.h
theory/quantifiers/sygus/example_infer.cpp
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include <numeric> // for std::iota
+#include <sstream>
using namespace cvc5::kind;
#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
#include "expr/node.h"
-#include "theory/quantifiers/sygus/synth_conjecture.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
namespace cvc5 {
namespace theory {
namespace quantifiers {
+class TermDbSygus;
+
/** Streamer of different values according to variable permutations
*
* Generates a new value (modulo rewriting) when queried in which its variables
class EnumStreamPermutation
{
public:
- EnumStreamPermutation(quantifiers::TermDbSygus* tds);
+ EnumStreamPermutation(TermDbSygus* tds);
~EnumStreamPermutation() {}
/** resets utility
*
private:
/** sygus term database of current quantifiers engine */
- quantifiers::TermDbSygus* d_tds;
+ TermDbSygus* d_tds;
/** maps subclass ids to subset of d_vars with that subclass id */
std::map<unsigned, std::vector<Node>> d_var_classes;
/** maps variables to subfield types with constructors for
class EnumStreamSubstitution
{
public:
- EnumStreamSubstitution(quantifiers::TermDbSygus* tds);
+ EnumStreamSubstitution(TermDbSygus* tds);
~EnumStreamSubstitution() {}
/** initializes utility
*
private:
/** sygus term database of current quantifiers engine */
- quantifiers::TermDbSygus* d_tds;
+ TermDbSygus* d_tds;
/** type this utility has been initialized for */
TypeNode d_tn;
/** current value */
class EnumStreamConcrete : public EnumValGenerator
{
public:
- EnumStreamConcrete(quantifiers::TermDbSygus* tds) : d_ess(tds) {}
+ EnumStreamConcrete(TermDbSygus* tds) : d_ess(tds) {}
/** initialize this class with enumerator e */
void initialize(Node e) override;
/** get that value v was enumerated */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Base class for sygus enumerators
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VAL_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VAL_GENERATOR_H
+
+#include "expr/node.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * 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;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
+
+#endif
#include <unordered_set>
#include "expr/node.h"
#include "expr/type_node.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include <unordered_set>
#include "expr/node.h"
#include "expr/type_node.h"
-#include "theory/quantifiers/sygus/synth_conjecture.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/type_enumerator.h"
#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"
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.
projects / cvc5.git / commitdiff