From ae83890dc38177f7c5c9cf07d7905ea7bf62d055 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 Aug 2019 15:25:26 -0500 Subject: [PATCH] Move basic sygus enumerator to its own file (#3149) --- src/CMakeLists.txt | 2 + .../sygus/sygus_enumerator_basic.cpp | 58 +++++++++++++++ .../sygus/sygus_enumerator_basic.h | 70 +++++++++++++++++++ .../quantifiers/sygus/synth_conjecture.cpp | 58 +-------------- 4 files changed, 131 insertions(+), 57 deletions(-) create mode 100644 src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp create mode 100644 src/theory/quantifiers/sygus/sygus_enumerator_basic.h 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 +#include +#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 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& 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 d_cache; -}; - Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) { bool isEnum = d_tds->isEnumerator(e); -- 2.30.2