From 4239b8bf84fcea902802812508668c866f700dda Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Jul 2021 09:51:02 -0500 Subject: [PATCH] Move enum value generator to own file (#6941) Work towards integrating the enumerator callback into the fast enumerator. --- src/CMakeLists.txt | 1 + .../sygus/enum_stream_substitution.cpp | 1 + .../sygus/enum_stream_substitution.h | 14 +++-- .../quantifiers/sygus/enum_val_generator.h | 62 +++++++++++++++++++ .../quantifiers/sygus/sygus_enumerator.h | 1 + .../sygus/sygus_enumerator_basic.h | 2 +- .../quantifiers/sygus/synth_conjecture.h | 32 +--------- 7 files changed, 75 insertions(+), 38 deletions(-) create mode 100644 src/theory/quantifiers/sygus/enum_val_generator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9f208ac46..2877ab820 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -859,6 +859,7 @@ libcvc5_add_sources( 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 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 3ae34d82c..f853ac8e8 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include // for std::iota +#include using namespace cvc5::kind; diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index ea028991b..05c693ace 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -19,12 +19,14 @@ #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 @@ -33,7 +35,7 @@ namespace quantifiers { class EnumStreamPermutation { public: - EnumStreamPermutation(quantifiers::TermDbSygus* tds); + EnumStreamPermutation(TermDbSygus* tds); ~EnumStreamPermutation() {} /** resets utility * @@ -70,7 +72,7 @@ class EnumStreamPermutation 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> d_var_classes; /** maps variables to subfield types with constructors for @@ -165,7 +167,7 @@ class EnumStreamPermutation class EnumStreamSubstitution { public: - EnumStreamSubstitution(quantifiers::TermDbSygus* tds); + EnumStreamSubstitution(TermDbSygus* tds); ~EnumStreamSubstitution() {} /** initializes utility * @@ -211,7 +213,7 @@ class EnumStreamSubstitution 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 */ @@ -281,7 +283,7 @@ class EnumStreamSubstitution 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 */ diff --git a/src/theory/quantifiers/sygus/enum_val_generator.h b/src/theory/quantifiers/sygus/enum_val_generator.h new file mode 100644 index 000000000..64c069087 --- /dev/null +++ b/src/theory/quantifiers/sygus/enum_val_generator.h @@ -0,0 +1,62 @@ +/****************************************************************************** + * 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 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 88133eb6e..39e58d5f3 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -22,6 +22,7 @@ #include #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" diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h index bae6f6327..42bce471d 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h @@ -22,7 +22,7 @@ #include #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" 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. -- 2.30.2