Add additional ground terms to SyGuS instantiation grammar (#5167)

This PR adds options to add additional ground terms to the SyGuS instantiation grammars.

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())