diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-10-01 13:48:37 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-01 13:48:37 -0700 |
commit | 776ee02237b06eb3130e56af4d98d9ff36667d8b (patch) | |
tree | 56d55c26003f2dfa3ef23c0cf4ae32e7af2e5e11 /src/theory/quantifiers_engine.cpp | |
parent | cd91768f52349bd14399e49b2fbc4e59bb659ded (diff) |
Add additional ground terms to SyGuS instantiation grammar (#5167)
This PR adds options to add additional ground terms to the SyGuS instantiation grammars.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 557d444d6..cceb04d9f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -370,6 +370,14 @@ void QuantifiersEngine::ppNotifyAssertions( sye->preregisterAssertion(a); } } + /* The SyGuS instantiation module needs a global view of all available + * assertions to collect global terms that get added to each grammar. + */ + if (options::sygusInst()) + { + quantifiers::SygusInst* si = d_qmodules->d_sygus_inst.get(); + si->ppNotifyAssertions(assertions); + } } void QuantifiersEngine::check( Theory::Effort e ){ @@ -976,8 +984,11 @@ void QuantifiersEngine::flushLemmas(){ //take default output channel if none is provided d_hasAddedLemma = true; std::map<Node, ProofGenerator*>::iterator itp; - for (const Node& lemw : d_lemmas_waiting) + // Note: Do not use foreach loop here and do not cache size() call. + // New lemmas can be added while iterating over d_lemmas_waiting. + for (size_t i = 0; i < d_lemmas_waiting.size(); ++i) { + const Node& lemw = d_lemmas_waiting[i]; Trace("qe-lemma") << "Lemma : " << lemw << std::endl; itp = d_lemmasWaitingPg.find(lemw); if (itp != d_lemmasWaitingPg.end()) |