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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
#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"
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);
projects / cvc5.git / commitdiff