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, 0 deletions

diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 2361c4a2b..c95c6a026 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -82,6 +82,9 @@ class SygusInst : public QuantifiersModule
   /* Called once for every quantifier 'q' per context. */
   void preRegisterQuantifier(Node q) override;
 
+  /* For collecting global terms from all available assertions. */
+  void ppNotifyAssertions(const std::vector<Node>& assertions);
+
   std::string identify() const override { return "SygusInst"; }
 
  private:
@@ -124,6 +127,15 @@ class SygusInst : public QuantifiersModule
   /* Indicates whether a counterexample lemma was added for a quantified
    * formula in the current context. */
   context::CDHashSet<Node, NodeHashFunction> d_ce_lemma_added;
+
+  /* Set of global ground terms in assertions (outside of quantifiers). */
+  context::CDHashMap<TypeNode,
+                     std::unordered_set<Node, NodeHashFunction>,
+                     TypeNodeHashFunction>
+      d_global_terms;
+
+  /* Assertions sent by ppNotifyAssertions. */
+  context::CDHashSet<Node, NodeHashFunction> d_notified_assertions;
 };
 
 }  // namespace quantifiers