Support for SyGuS PBE + recursive functions (#3433)

1 files changed, 11 insertions, 3 deletions

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 88d00ce3a..9f6954416 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -33,7 +33,7 @@ namespace theory {
 namespace quantifiers {
 
 SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
-    : QuantifiersModule(qe)
+    : QuantifiersModule(qe), d_tds(qe->getTermDatabaseSygus())
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
       new SynthConjecture(d_quantEngine, this)));
@@ -274,6 +274,8 @@ void SynthEngine::assignConjecture(Node q)
 
 void SynthEngine::registerQuantifier(Node q)
 {
+  Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
+                       << std::endl;
   if (d_quantEngine->getOwner(q) == this)
   {
     Trace("cegqi") << "Register conjecture : " << q << std::endl;
@@ -287,9 +289,15 @@ void SynthEngine::registerQuantifier(Node q)
       assignConjecture(q);
     }
   }
-  else
+  if (options::sygusRecFun())
   {
-    Trace("cegqi-debug") << "Register quantifier : " << q << std::endl;
+    if (d_quantEngine->getQuantAttributes()->isFunDef(q))
+    {
+      // If it is a recursive function definition, add it to the function
+      // definition evaluator class.
+      FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
+      fde->assertDefinition(q);
+    }
   }
 }