This moves the method SynthConjecture::getEnumeratedValue to its own class, EnumManager.
It also integrates the sygus enumerator callback into the fast enumerator.
theory/quantifiers/sygus/example_min_eval.h
theory/quantifiers/sygus/enum_stream_substitution.cpp
theory/quantifiers/sygus/enum_stream_substitution.h
+ theory/quantifiers/sygus/enum_value_manager.cpp
+ theory/quantifiers/sygus/enum_value_manager.h
theory/quantifiers/sygus/example_infer.cpp
theory/quantifiers/sygus/example_infer.h
theory/quantifiers/sygus/example_min_eval.cpp
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Mathias Preiner, Haniel Barbosa
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Management of current value for an enumerator
+ */
+#include "theory/quantifiers/sygus/enum_value_manager.h"
+
+#include "options/datatypes_options.h"
+#include "options/quantifiers_options.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_inference_manager.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/term_database_sygus.h"
+#include "theory/quantifiers/term_registry.h"
+
+using namespace cvc5::kind;
+using namespace std;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+EnumValueManager::EnumValueManager(Node e,
+ QuantifiersInferenceManager& qim,
+ TermRegistry& tr,
+ SygusStatistics& s,
+ bool hasExamples)
+ : d_enum(e),
+ d_qim(qim),
+ d_treg(tr),
+ d_stats(s),
+ d_tds(tr.getTermDatabaseSygus()),
+ d_eec(hasExamples ? new ExampleEvalCache(d_tds, e) : nullptr)
+{
+}
+
+EnumValueManager::~EnumValueManager() {}
+
+Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
+{
+ Node e = d_enum;
+ bool isEnum = d_tds->isEnumerator(e);
+
+ if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
+ {
+ // if the current model value of e was not registered by the datatypes
+ // sygus solver, or was excluded by symmetry breaking, then it does not
+ // have a proper model value that we should consider, thus we return null.
+ Trace("sygus-engine-debug")
+ << "Enumerator " << e << " does not have proper model value."
+ << std::endl;
+ return Node::null();
+ }
+
+ if (!isEnum || d_tds->isPassiveEnumerator(e))
+ {
+ return getModelValue(e);
+ }
+
+ // management of actively generated enumerators goes here
+
+ // initialize the enumerated value generator for e
+ if (d_evg == nullptr)
+ {
+ if (d_tds->isVariableAgnosticEnumerator(e))
+ {
+ d_evg.reset(new EnumStreamConcrete(d_tds));
+ }
+ else
+ {
+ // Actively-generated enumerators are currently either variable agnostic
+ // or basic. The auto mode always prefers the optimized enumerator over
+ // the basic one.
+ Assert(d_tds->isBasicEnumerator(e));
+ if (options::sygusActiveGenMode()
+ == options::SygusActiveGenMode::ENUM_BASIC)
+ {
+ d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType()));
+ }
+ else
+ {
+ Assert(options::sygusActiveGenMode()
+ == options::SygusActiveGenMode::ENUM
+ || options::sygusActiveGenMode()
+ == options::SygusActiveGenMode::AUTO);
+ // create the enumerator callback
+ if (options::sygusSymBreakDynamic())
+ {
+ if (options::sygusRewVerify())
+ {
+ d_samplerRrV.reset(new SygusSampler);
+ d_samplerRrV->initializeSygus(
+ d_tds, e, options::sygusSamples(), false);
+ }
+ d_secd.reset(new SygusEnumeratorCallbackDefault(
+ e, &d_stats, d_eec.get(), d_samplerRrV.get()));
+ }
+ // if sygus repair const is enabled, we enumerate terms with free
+ // variables as arguments to any-constant constructors
+ d_evg.reset(new SygusEnumerator(
+ d_tds, d_secd.get(), &d_stats, false, options::sygusRepairConst()));
+ }
+ }
+ Trace("sygus-active-gen")
+ << "Active-gen: initialize for " << e << std::endl;
+ d_evg->initialize(e);
+ d_ev_curr_active_gen = Node::null();
+ Trace("sygus-active-gen-debug") << "...finish" << std::endl;
+ }
+ // if we have a waiting value, return it
+ if (!d_evActiveGenWaiting.isNull())
+ {
+ Trace("sygus-active-gen-debug")
+ << "Active-gen: return waiting " << d_evActiveGenWaiting << std::endl;
+ return d_evActiveGenWaiting;
+ }
+ // Check if there is an (abstract) value absE we were actively generating
+ // values based on.
+ Node absE = d_ev_curr_active_gen;
+ bool firstTime = false;
+ if (absE.isNull())
+ {
+ // None currently exist. The next abstract value is the model value for e.
+ absE = getModelValue(e);
+ if (Trace.isOn("sygus-active-gen"))
+ {
+ Trace("sygus-active-gen") << "Active-gen: new abstract value : ";
+ TermDbSygus::toStreamSygus("sygus-active-gen", e);
+ Trace("sygus-active-gen") << " -> ";
+ TermDbSygus::toStreamSygus("sygus-active-gen", absE);
+ Trace("sygus-active-gen") << std::endl;
+ }
+ d_ev_curr_active_gen = absE;
+ d_evg->addValue(absE);
+ firstTime = true;
+ }
+ bool inc = true;
+ if (!firstTime)
+ {
+ inc = d_evg->increment();
+ }
+ Node v;
+ if (inc)
+ {
+ v = d_evg->getCurrent();
+ }
+ Trace("sygus-active-gen-debug")
+ << "...generated " << v << ", with increment success : " << inc
+ << std::endl;
+ if (!inc)
+ {
+ // No more concrete values generated from absE.
+ NodeManager* nm = NodeManager::currentNM();
+ d_ev_curr_active_gen = Node::null();
+ std::vector<Node> exp;
+ // If we are a basic enumerator, a single abstract value maps to *all*
+ // concrete values of its type, thus we don't depend on the current
+ // solution.
+ if (!d_tds->isBasicEnumerator(e))
+ {
+ // We must block e = absE
+ d_tds->getExplain()->getExplanationForEquality(e, absE, exp);
+ for (unsigned i = 0, size = exp.size(); i < size; i++)
+ {
+ exp[i] = exp[i].negate();
+ }
+ }
+ Node g = d_tds->getActiveGuardForEnumerator(e);
+ if (!g.isNull())
+ {
+ if (d_evActiveGenFirstVal.isNull())
+ {
+ exp.push_back(g.negate());
+ d_evActiveGenFirstVal = absE;
+ }
+ }
+ else
+ {
+ Assert(false);
+ }
+ Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp);
+ Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator "
+ "exclude current solution : "
+ << lem << std::endl;
+ if (Trace.isOn("sygus-active-gen-debug"))
+ {
+ Trace("sygus-active-gen-debug") << "Active-gen: block ";
+ TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
+ Trace("sygus-active-gen-debug") << std::endl;
+ }
+ d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT);
+ }
+ else
+ {
+ // We are waiting to send e -> v to the module that requested it.
+ if (v.isNull())
+ {
+ activeIncomplete = true;
+ }
+ else
+ {
+ d_evActiveGenWaiting = v;
+ }
+ if (Trace.isOn("sygus-active-gen"))
+ {
+ Trace("sygus-active-gen") << "Active-gen : " << e << " : ";
+ TermDbSygus::toStreamSygus("sygus-active-gen", absE);
+ Trace("sygus-active-gen") << " -> ";
+ TermDbSygus::toStreamSygus("sygus-active-gen", v);
+ Trace("sygus-active-gen") << std::endl;
+ }
+ }
+
+ return v;
+}
+
+void EnumValueManager::notifyCandidate(bool modelSuccess)
+{
+ d_evActiveGenWaiting = Node::null();
+ // clear evaluation
+ if (modelSuccess && d_eec != nullptr)
+ {
+ d_eec->clearEvaluationAll();
+ }
+}
+
+ExampleEvalCache* EnumValueManager::getExampleEvalCache()
+{
+ return d_eec.get();
+}
+
+Node EnumValueManager::getModelValue(Node n)
+{
+ return d_treg.getModel()->getValue(n);
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
--- /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.
+ * ****************************************************************************
+ *
+ * Management of current value for an enumerator
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VALUE_MANAGER_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VALUE_MANAGER_H
+
+#include "expr/node.h"
+#include "theory/quantifiers/sygus/enum_val_generator.h"
+#include "theory/quantifiers/sygus/example_eval_cache.h"
+#include "theory/quantifiers/sygus/sygus_enumerator_callback.h"
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifiersInferenceManager;
+class TermRegistry;
+class SygusStatistics;
+
+/**
+ * Management of current value for an enumerator. This class determines the
+ * current value of an enumerator, which may be its model value if it is
+ * not actively generated, or may be determined by the (fast) enumerator
+ * when it is actively generated.
+ */
+class EnumValueManager
+{
+ public:
+ EnumValueManager(Node e,
+ QuantifiersInferenceManager& qim,
+ TermRegistry& tr,
+ SygusStatistics& s,
+ bool hasExamples);
+ ~EnumValueManager();
+ /**
+ * Get model value for term n. If n has a value that was excluded by
+ * datatypes sygus symmetry breaking, this method returns null. It sets
+ * activeIncomplete to true if the enumerator we are managing is
+ * actively-generated, and its current value is null but it has not finished
+ * generating values.
+ */
+ Node getEnumeratedValue(bool& activeIncomplete);
+ /**
+ * Notify that a synthesis candidate was tried, which clears the value
+ * of d_evActiveGenWaiting, as well as the evaluation cache if modelSuccess
+ * is true
+ */
+ void notifyCandidate(bool modelSuccess);
+ /** Get the example evaluation cache */
+ ExampleEvalCache* getExampleEvalCache();
+
+ private:
+ /**
+ * Get model value for term n.
+ */
+ Node getModelValue(Node n);
+ /** The enumerator */
+ Node d_enum;
+ /** Reference to the quantifiers inference manager */
+ QuantifiersInferenceManager& d_qim;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
+ /** reference to the statistics of parent */
+ SygusStatistics& d_stats;
+ /** term database sygus of d_qe */
+ TermDbSygus* d_tds;
+ /** Sygus sampler (for --sygus-rr-verify) */
+ std::unique_ptr<SygusSampler> d_samplerRrV;
+ /** if we allocated a default sygus enumerator callback */
+ std::unique_ptr<SygusEnumeratorCallbackDefault> d_secd;
+ /** enumerator generators for each actively-generated enumerator */
+ std::unique_ptr<EnumValGenerator> d_evg;
+ /** example evaluation cache utility for each enumerator */
+ std::unique_ptr<ExampleEvalCache> d_eec;
+ /**
+ * Map from enumerators to whether they are currently being
+ * "actively-generated". That is, we are in a state where we have called
+ * d_evg.addValue(v) for some v, and d_evg.getNext() has not yet
+ * returned null. The range of this map stores the abstract value that
+ * we are currently generating values from.
+ */
+ Node d_ev_curr_active_gen;
+ /** the current waiting value of the actively-generated enumerator, if any
+ *
+ * This caches values that are actively generated and that we have not yet
+ * passed to a call to SygusModule::constructCandidates. An example of when
+ * this may occur is when there are two actively-generated enumerators e1 and
+ * e2. Say on some iteration we actively-generate v1 for e1, the value
+ * of e2 was excluded by symmetry breaking, and say the current master sygus
+ * module does not handle partial models. Hence, we abort the current check.
+ * We remember that the value of e1 was v1 by storing it here, so that on
+ * a future check when v2 has a proper value, it is returned.
+ */
+ Node d_evActiveGenWaiting;
+ /** the first value enumerated for the actively-generated enumerator
+ *
+ * This is to implement an optimization that only guards the blocking lemma
+ * for the first value of an actively-generated enumerator.
+ */
+ Node d_evActiveGenFirstVal;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
+
+#endif
#include "theory/quantifiers/sygus/example_eval_cache.h"
#include "theory/quantifiers/sygus/example_min_eval.h"
-#include "theory/quantifiers/sygus/synth_conjecture.h"
using namespace cvc5;
using namespace cvc5::kind;
namespace quantifiers {
ExampleEvalCache::ExampleEvalCache(TermDbSygus* tds,
- SynthConjecture* p,
- Node f,
Node e)
: d_tds(tds), d_stn(e.getType())
{
- ExampleInfer* ei = p->getExampleInfer();
- Assert(ei->hasExamples(f));
- for (unsigned i = 0, nex = ei->getNumExamples(f); i < nex; i++)
- {
- std::vector<Node> input;
- ei->getExample(f, i, input);
- d_examples.push_back(input);
- }
d_indexSearchVals = !d_tds->isVariableAgnosticEnumerator(e);
}
ExampleEvalCache::~ExampleEvalCache() {}
+void ExampleEvalCache::addExample(const std::vector<Node>& ex)
+{
+ d_examples.push_back(ex);
+}
+
Node ExampleEvalCache::addSearchVal(TypeNode tn, Node bv)
{
if (!d_indexSearchVals)
* are builtin terms that the analog of values taken by enumerator e that
* is associated with f.
*/
- ExampleEvalCache(TermDbSygus* tds, SynthConjecture* p, Node f, Node e);
+ ExampleEvalCache(TermDbSygus* tds, Node e);
~ExampleEvalCache();
+ /**
+ * Add example to the list of examples maintained by this class.
+ */
+ void addExample(const std::vector<Node>& ex);
/** Add search value
*
#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
#define CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
+#include "theory/quantifiers/candidate_rewrite_database.h"
#include "theory/quantifiers/sygus/sygus_enumerator.h"
+#include "theory/quantifiers/sygus_sampler.h"
namespace cvc5 {
namespace theory {
namespace quantifiers {
class RConsObligation;
+class CandidateRewriteDatabase;
/**
* A utility class for Sygus Reconstruct datatype types (grammar non-terminals).
namespace quantifiers {
SygusEnumerator::SygusEnumerator(TermDbSygus* tds,
- SynthConjecture* p,
+ SygusEnumeratorCallback* sec,
SygusStatistics* s,
bool enumShapes,
bool enumAnyConstHoles)
: d_tds(tds),
- d_parent(p),
+ d_sec(sec),
d_stats(s),
d_enumShapes(enumShapes),
d_enumAnyConstHoles(enumAnyConstHoles),
{
Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl;
d_enum = e;
+ // allocate the default callback
+ if (d_sec == nullptr && options::sygusSymBreakDynamic())
+ {
+ d_secd.reset(new SygusEnumeratorCallbackDefault(e, d_stats));
+ d_sec = d_secd.get();
+ }
d_etype = d_enum.getType();
Assert(d_etype.isDatatype());
Assert(d_etype.getDType().isSygus());
// if we don't have a term database, we don't register symmetry breaking
// lemmas
- if (!d_tds)
+ if (d_tds == nullptr)
{
return;
}
bool SygusEnumerator::isEnumShapes() const { return d_enumShapes; }
SygusEnumerator::TermCache::TermCache()
- : d_tds(nullptr),
- d_eec(nullptr),
+ : d_sec(nullptr),
d_isSygusType(false),
d_numConClasses(0),
d_sizeEnum(0),
- d_isComplete(false),
- d_sampleRrVInit(false)
+ d_isComplete(false)
{
}
void SygusEnumerator::TermCache::initialize(SygusStatistics* s,
Node e,
TypeNode tn,
- TermDbSygus* tds,
- ExampleEvalCache* eec)
+ SygusEnumeratorCallback* sec)
{
Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl;
d_stats = s;
d_enum = e;
d_tn = tn;
- d_tds = tds;
- d_eec = eec;
+ d_sec = sec;
d_sizeStartIndex[0] = 0;
d_isSygusType = false;
return true;
}
Assert(!n.isNull());
- if (options::sygusSymBreakDynamic())
+ if (d_sec != nullptr)
{
- Node bn = datatypes::utils::sygusToBuiltin(n);
- Node bnr = d_extr.extendedRewrite(bn);
- if (d_stats != nullptr)
- {
- ++(d_stats->d_enumTermsRewrite);
- }
- if (options::sygusRewVerify())
+ if (!d_sec->addTerm(n, d_bterms))
{
- if (bn != bnr)
- {
- if (!d_sampleRrVInit)
- {
- d_sampleRrVInit = true;
- d_samplerRrV.initializeSygus(
- d_tds, d_enum, options::sygusSamples(), false);
- }
- d_samplerRrV.checkEquivalent(bn, bnr);
- }
- }
- // must be unique up to rewriting
- if (d_bterms.find(bnr) != d_bterms.end())
- {
- Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
+ Trace("sygus-enum-exc")
+ << "Exclude: " << datatypes::utils::sygusToBuiltin(n)
+ << " due to callback" << std::endl;
return false;
}
- // insert to builtin term cache, regardless of whether it is redundant
- // based on examples.
- d_bterms.insert(bnr);
- // if we are doing PBE symmetry breaking
- if (d_eec != nullptr)
- {
- if (d_stats != nullptr)
- {
- ++(d_stats->d_enumTermsExampleEval);
- }
- // Is it equivalent under examples?
- Node bne = d_eec->addSearchVal(d_tn, bnr);
- if (!bne.isNull())
- {
- if (bnr != bne)
- {
- Trace("sygus-enum-exc")
- << "Exclude (by examples): " << bn << ", since we already have "
- << bne << std::endl;
- return false;
- }
- }
- }
- Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
}
if (d_stats != nullptr)
{
void SygusEnumerator::initializeTermCache(TypeNode tn)
{
// initialize the term cache
- // see if we use an example evaluation cache for symmetry breaking
- ExampleEvalCache* eec = nullptr;
- if (d_parent != nullptr && options::sygusSymBreakPbe())
- {
- eec = d_parent->getExampleEvalCache(d_enum);
- }
- d_tcache[tn].initialize(d_stats, d_enum, tn, d_tds, eec);
+ d_tcache[tn].initialize(d_stats, d_enum, tn, d_sec);
}
SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
#include <map>
#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/sygus_enumerator_callback.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
namespace cvc5 {
* @param tds Pointer to the term database, required if enumShapes or
* enumAnyConstHoles is true, or if we want to include symmetry breaking from
* lemmas stored in the sygus term database,
- * @param p Pointer to the conjecture, required if we wish to do
+ * @param sec Pointer to the callback, required e.g. if we wish to do
* conjecture-specific symmetry breaking
* @param s Pointer to the statistics
* @param enumShapes If true, this enumerator will generate terms having any
* free variables are the arguments to any-constant constructors.
*/
SygusEnumerator(TermDbSygus* tds = nullptr,
- SynthConjecture* p = nullptr,
+ SygusEnumeratorCallback* sec = nullptr,
SygusStatistics* s = nullptr,
bool enumShapes = false,
bool enumAnyConstHoles = false);
private:
/** pointer to term database sygus */
TermDbSygus* d_tds;
- /** pointer to the synth conjecture that owns this enumerator */
- SynthConjecture* d_parent;
+ /** pointer to the enumerator callback we are using (if any) */
+ SygusEnumeratorCallback* d_sec;
+ /** if we allocated a default sygus enumerator callback */
+ std::unique_ptr<SygusEnumeratorCallbackDefault> d_secd;
/** pointer to the statistics */
SygusStatistics* d_stats;
/** Whether we are enumerating shapes */
void initialize(SygusStatistics* s,
Node e,
TypeNode tn,
- TermDbSygus* tds,
- ExampleEvalCache* ece = nullptr);
+ SygusEnumeratorCallback* sec = nullptr);
/** get last constructor class index for weight
*
* This returns a minimal index n such that all constructor classes at
Node d_enum;
/** the sygus type of terms in this cache */
TypeNode d_tn;
- /** pointer to term database sygus */
- TermDbSygus* d_tds;
- /** extended rewriter */
- ExtendedRewriter d_extr;
- /**
- * Pointer to the example evaluation cache utility (used for symmetry
- * breaking).
- */
- ExampleEvalCache* d_eec;
+ /** Pointer to the callback (used for symmetry breaking). */
+ SygusEnumeratorCallback* d_sec;
//-------------------------static information about type
/** is d_tn a sygus type? */
bool d_isSygusType;
unsigned d_sizeEnum;
/** whether this term cache is complete */
bool d_isComplete;
- /** sampler (for --sygus-rr-verify) */
- quantifiers::SygusSampler d_samplerRrV;
- /** is the above sampler initialized? */
- bool d_sampleRrVInit;
};
/** above cache for each sygus type */
std::map<TypeNode, TermCache> d_tcache;
* @param bterms The (rewritten, builtin) terms we have already enumerated
* @return true if n should be considered in the enumeration.
*/
- virtual bool addTerm(Node n, std::unordered_set<Node>& bterms) = 0;
+ virtual bool addTerm(Node n, std::unordered_set<Node>& bterms);
protected:
/**
* @param bn The builtin version of the enumerated term
* @param bnr The (extended) rewritten form of bn
*/
- virtual void notifyTermInternal(Node n, Node bn, Node bnr) = 0;
+ virtual void notifyTermInternal(Node n, Node bn, Node bnr) {}
/**
* Callback-specific add term
*
* @param bnr The (extended) rewritten form of bn
* @return true if the term should be considered in the enumeration.
*/
- virtual bool addTermInternal(Node n, Node bn, Node bnr) = 0;
+ virtual bool addTermInternal(Node n, Node bn, Node bnr) { return true; }
/** The enumerator */
Node d_enum;
/** The type of enum */
#include <map>
#include <vector>
+#include "expr/match_trie.h"
#include "theory/quantifiers/sygus/rcons_obligation.h"
#include "theory/quantifiers/sygus/rcons_type_info.h"
using BuiltinSet = std::unordered_set<Node>;
using TypeBuiltinSetMap = std::unordered_map<TypeNode, BuiltinSet>;
+using NodePairMap = std::unordered_map<Node, Node>;
/** SygusReconstruct
*
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.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/enum_value_manager.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/sygus_pbe.h"
#include "theory/quantifiers/sygus/synth_engine.h"
// on the next call
return !activeIncomplete;
}
- // the waiting values are passed to the module below, clear
- d_ev_active_gen_waiting.clear();
-
+ // determine if we had at least one value for an enumerator
Assert(terms.size() == enum_values.size());
- bool emptyModel = true;
+ bool modelSuccess = false;
for (unsigned i = 0, size = terms.size(); i < size; i++)
{
if (!enum_values[i].isNull())
{
- emptyModel = false;
+ modelSuccess = true;
}
}
- if (emptyModel)
- {
- Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
- return !activeIncomplete;
- }
- // Must separately compute whether trace is on due to compilation of
- // Trace.isOn.
- bool traceIsOn = Trace.isOn("sygus-engine");
- if (printDebug || traceIsOn)
+ if (modelSuccess)
{
- Trace("sygus-engine") << " * Value is : ";
- std::stringstream sygusEnumOut;
- FirstOrderModel* m = d_treg.getModel();
- for (unsigned i = 0, size = terms.size(); i < size; i++)
+ // Must separately compute whether trace is on due to compilation of
+ // Trace.isOn.
+ bool traceIsOn = Trace.isOn("sygus-engine");
+ if (printDebug || traceIsOn)
{
- Node nv = enum_values[i];
- Node onv = nv.isNull() ? m->getValue(terms[i]) : nv;
- TypeNode tn = onv.getType();
- std::stringstream ss;
- TermDbSygus::toStreamSygus(ss, onv);
- if (printDebug)
- {
- sygusEnumOut << " " << ss.str();
- }
- Trace("sygus-engine") << terms[i] << " -> ";
- if (nv.isNull())
- {
- Trace("sygus-engine") << "[EXC: " << ss.str() << "] ";
- }
- else
+ Trace("sygus-engine") << " * Value is : ";
+ std::stringstream sygusEnumOut;
+ FirstOrderModel* m = d_treg.getModel();
+ for (unsigned i = 0, size = terms.size(); i < size; i++)
{
- Trace("sygus-engine") << ss.str() << " ";
- if (Trace.isOn("sygus-engine-rr"))
+ Node nv = enum_values[i];
+ Node onv = nv.isNull() ? m->getValue(terms[i]) : nv;
+ TypeNode tn = onv.getType();
+ std::stringstream ss;
+ TermDbSygus::toStreamSygus(ss, onv);
+ if (printDebug)
+ {
+ sygusEnumOut << " " << ss.str();
+ }
+ Trace("sygus-engine") << terms[i] << " -> ";
+ if (nv.isNull())
{
- Node bv = d_tds->sygusToBuiltin(nv, tn);
- bv = Rewriter::rewrite(bv);
- Trace("sygus-engine-rr") << " -> " << bv << std::endl;
+ Trace("sygus-engine") << "[EXC: " << ss.str() << "] ";
+ }
+ else
+ {
+ Trace("sygus-engine") << ss.str() << " ";
+ if (Trace.isOn("sygus-engine-rr"))
+ {
+ Node bv = d_tds->sygusToBuiltin(nv, tn);
+ bv = Rewriter::rewrite(bv);
+ Trace("sygus-engine-rr") << " -> " << bv << std::endl;
+ }
}
}
+ Trace("sygus-engine") << std::endl;
+ Output(options::OutputTag::SYGUS)
+ << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
}
- Trace("sygus-engine") << std::endl;
- Output(options::OutputTag::SYGUS)
- << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
+ Assert(candidate_values.empty());
+ constructed_cand = d_master->constructCandidates(
+ terms, enum_values, d_candidates, candidate_values);
}
- Assert(candidate_values.empty());
- constructed_cand = d_master->constructCandidates(
- terms, enum_values, d_candidates, candidate_values);
- // now clear the evaluation caches
- for (std::pair<const Node, std::unique_ptr<ExampleEvalCache> >& ecp :
- d_exampleEvalCache)
+ // notify the enumerator managers of the status of the candidate
+ for (std::pair<const Node, std::unique_ptr<EnumValueManager>>& ecp :
+ d_enumManager)
{
- ExampleEvalCache* eec = ecp.second.get();
- if (eec != nullptr)
- {
- eec->clearEvaluationAll();
- }
+ ecp.second->notifyCandidate(modelSuccess);
+ }
+ // if we did not generate a candidate, return now
+ if (!modelSuccess)
+ {
+ Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
+ return !activeIncomplete;
}
}
continue;
}
}
- Node nv = getEnumeratedValue(e, activeIncomplete);
+ EnumValueManager* eman = getEnumValueManagerFor(e);
+ Node nv = eman->getEnumeratedValue(activeIncomplete);
n.push_back(e);
v.push_back(nv);
ret = ret && !nv.isNull();
return ret;
}
-Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
+EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e)
{
- bool isEnum = d_tds->isEnumerator(e);
-
- if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
- {
- // if the current model value of e was not registered by the datatypes
- // sygus solver, or was excluded by symmetry breaking, then it does not
- // have a proper model value that we should consider, thus we return null.
- Trace("sygus-engine-debug")
- << "Enumerator " << e << " does not have proper model value."
- << std::endl;
- return Node::null();
- }
-
- if (!isEnum || d_tds->isPassiveEnumerator(e))
- {
- return getModelValue(e);
- }
-
- // management of actively generated enumerators goes here
-
- // initialize the enumerated value generator for e
- std::map<Node, std::unique_ptr<EnumValGenerator> >::iterator iteg =
- d_evg.find(e);
- if (iteg == d_evg.end())
- {
- if (d_tds->isVariableAgnosticEnumerator(e))
- {
- d_evg[e].reset(new EnumStreamConcrete(d_tds));
- }
- else
- {
- // Actively-generated enumerators are currently either variable agnostic
- // or basic. The auto mode always prefers the optimized enumerator over
- // the basic one.
- Assert(d_tds->isBasicEnumerator(e));
- if (options::sygusActiveGenMode()
- == options::SygusActiveGenMode::ENUM_BASIC)
- {
- d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
- }
- else
- {
- Assert(options::sygusActiveGenMode()
- == options::SygusActiveGenMode::ENUM
- || options::sygusActiveGenMode()
- == options::SygusActiveGenMode::AUTO);
- // if sygus repair const is enabled, we enumerate terms with free
- // variables as arguments to any-constant constructors
- d_evg[e].reset(new SygusEnumerator(
- d_tds, this, &d_stats, false, options::sygusRepairConst()));
- }
- }
- Trace("sygus-active-gen")
- << "Active-gen: initialize for " << e << std::endl;
- d_evg[e]->initialize(e);
- d_ev_curr_active_gen[e] = Node::null();
- iteg = d_evg.find(e);
- Trace("sygus-active-gen-debug") << "...finish" << std::endl;
- }
- // if we have a waiting value, return it
- std::map<Node, Node>::iterator itw = d_ev_active_gen_waiting.find(e);
- if (itw != d_ev_active_gen_waiting.end())
- {
- Trace("sygus-active-gen-debug")
- << "Active-gen: return waiting " << itw->second << std::endl;
- return itw->second;
- }
- // Check if there is an (abstract) value absE we were actively generating
- // values based on.
- Node absE = d_ev_curr_active_gen[e];
- bool firstTime = false;
- if (absE.isNull())
- {
- // None currently exist. The next abstract value is the model value for e.
- absE = getModelValue(e);
- if (Trace.isOn("sygus-active-gen"))
- {
- Trace("sygus-active-gen") << "Active-gen: new abstract value : ";
- TermDbSygus::toStreamSygus("sygus-active-gen", e);
- Trace("sygus-active-gen") << " -> ";
- TermDbSygus::toStreamSygus("sygus-active-gen", absE);
- Trace("sygus-active-gen") << std::endl;
- }
- d_ev_curr_active_gen[e] = absE;
- iteg->second->addValue(absE);
- firstTime = true;
- }
- bool inc = true;
- if (!firstTime)
- {
- inc = iteg->second->increment();
- }
- Node v;
- if (inc)
- {
- v = iteg->second->getCurrent();
- }
- Trace("sygus-active-gen-debug") << "...generated " << v
- << ", with increment success : " << inc
- << std::endl;
- if (!inc)
+ std::map<Node, std::unique_ptr<EnumValueManager>>::iterator it =
+ d_enumManager.find(e);
+ if (it != d_enumManager.end())
{
- // No more concrete values generated from absE.
- NodeManager* nm = NodeManager::currentNM();
- d_ev_curr_active_gen[e] = Node::null();
- std::vector<Node> exp;
- // If we are a basic enumerator, a single abstract value maps to *all*
- // concrete values of its type, thus we don't depend on the current
- // solution.
- if (!d_tds->isBasicEnumerator(e))
- {
- // We must block e = absE
- d_tds->getExplain()->getExplanationForEquality(e, absE, exp);
- for (unsigned i = 0, size = exp.size(); i < size; i++)
- {
- exp[i] = exp[i].negate();
- }
- }
- Node g = d_tds->getActiveGuardForEnumerator(e);
- if (!g.isNull())
- {
- if (d_ev_active_gen_first_val.find(e) == d_ev_active_gen_first_val.end())
- {
- exp.push_back(g.negate());
- d_ev_active_gen_first_val[e] = absE;
- }
- }
- else
- {
- Assert(false);
- }
- Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp);
- Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator "
- "exclude current solution : "
- << lem << std::endl;
- if (Trace.isOn("sygus-active-gen-debug"))
- {
- Trace("sygus-active-gen-debug") << "Active-gen: block ";
- TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
- Trace("sygus-active-gen-debug") << std::endl;
- }
- d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT);
+ return it->second.get();
}
- else
+ // otherwise, allocate it
+ Node f = d_tds->getSynthFunForEnumerator(e);
+ bool hasExamples = (d_exampleInfer->hasExamples(f)
+ && d_exampleInfer->getNumExamples(f) != 0);
+ d_enumManager[e].reset(
+ new EnumValueManager(e, d_qim, d_treg, d_stats, hasExamples));
+ EnumValueManager* eman = d_enumManager[e].get();
+ // set up the examples
+ if (hasExamples)
{
- // We are waiting to send e -> v to the module that requested it.
- if (v.isNull())
- {
- activeIncomplete = true;
- }
- else
- {
- d_ev_active_gen_waiting[e] = v;
- }
- if (Trace.isOn("sygus-active-gen"))
+ ExampleEvalCache* eec = eman->getExampleEvalCache();
+ Assert(eec != nullptr);
+ for (unsigned i = 0, nex = d_exampleInfer->getNumExamples(f); i < nex; i++)
{
- Trace("sygus-active-gen") << "Active-gen : " << e << " : ";
- TermDbSygus::toStreamSygus("sygus-active-gen", absE);
- Trace("sygus-active-gen") << " -> ";
- TermDbSygus::toStreamSygus("sygus-active-gen", v);
- Trace("sygus-active-gen") << std::endl;
+ std::vector<Node> input;
+ d_exampleInfer->getExample(f, i, input);
+ eec->addExample(input);
}
}
-
- return v;
+ return eman;
}
Node SynthConjecture::getModelValue(Node n)
ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e)
{
- std::map<Node, std::unique_ptr<ExampleEvalCache> >::iterator it =
- d_exampleEvalCache.find(e);
- if (it != d_exampleEvalCache.end())
- {
- return it->second.get();
- }
- Node f = d_tds->getSynthFunForEnumerator(e);
- // if f does not have examples, we don't construct the utility
- if (!d_exampleInfer->hasExamples(f) || d_exampleInfer->getNumExamples(f) == 0)
- {
- d_exampleEvalCache[e].reset(nullptr);
- return nullptr;
- }
- d_exampleEvalCache[e].reset(new ExampleEvalCache(d_tds, this, f, e));
- return d_exampleEvalCache[e].get();
+ EnumValueManager* eman = getEnumValueManagerFor(e);
+ return eman->getExampleEvalCache();
}
} // namespace quantifiers
class CegGrammarConstructor;
class SygusPbe;
class SygusStatistics;
+class EnumValueManager;
/** a synthesis conjecture
* This class implements approaches for a synthesis conjecture, given by data
std::unique_ptr<SygusRepairConst> d_sygus_rconst;
/** example inference utility */
std::unique_ptr<ExampleInfer> d_exampleInfer;
- /** example evaluation cache utility for each enumerator */
- std::map<Node, std::unique_ptr<ExampleEvalCache> > d_exampleEvalCache;
+ /** map from enumerators to their enumerator manager */
+ std::map<Node, std::unique_ptr<EnumValueManager>> d_enumManager;
//------------------------modules
/** program by examples module */
std::vector<Node>& v,
bool& activeIncomplete);
/**
- * Get model value for term n. If n has a value that was excluded by
- * datatypes sygus symmetry breaking, this method returns null. It sets
- * activeIncomplete to true if there is an actively-generated enumerator whose
- * current value is null but it has not finished generating values.
+ * Get or make enumerator manager for the enumerator e.
*/
- Node getEnumeratedValue(Node n, bool& activeIncomplete);
- /** enumerator generators for each actively-generated enumerator */
- std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg;
- /**
- * Map from enumerators to whether they are currently being
- * "actively-generated". That is, we are in a state where we have called
- * d_evg[e].addValue(v) for some v, and d_evg[e].getNext() has not yet
- * returned null. The range of this map stores the abstract value that
- * we are currently generating values from.
- */
- std::map<Node, Node> d_ev_curr_active_gen;
- /** the current waiting value of each actively-generated enumerator, if any
- *
- * This caches values that are actively generated and that we have not yet
- * passed to a call to SygusModule::constructCandidates. An example of when
- * this may occur is when there are two actively-generated enumerators e1 and
- * e2. Say on some iteration we actively-generate v1 for e1, the value
- * of e2 was excluded by symmetry breaking, and say the current master sygus
- * module does not handle partial models. Hence, we abort the current check.
- * We remember that the value of e1 was v1 by storing it here, so that on
- * a future check when v2 has a proper value, it is returned.
- */
- std::map<Node, Node> d_ev_active_gen_waiting;
- /** the first value enumerated for each actively-generated enumerator
- *
- * This is to implement an optimization that only guards the blocking lemma
- * for the first value of an actively-generated enumerator.
- */
- std::map<Node, Node> d_ev_active_gen_first_val;
+ EnumValueManager* getEnumValueManagerFor(Node e);
//------------------------end enumerators
/** list of constants for quantified formula
void SygusSampler::checkEquivalent(Node bv, Node bvr)
{
+ if (bv == bvr)
+ {
+ return;
+ }
Trace("sygus-rr-verify") << "Testing rewrite rule " << bv << " ---> " << bvr
<< std::endl;
projects / cvc5.git / commitdiff