Replace old sygus term reconstruction algorithm with a new one. (#5779)

This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.

1 files changed, 7 insertions, 7 deletions

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 3a9864ea9..831216445 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -57,7 +57,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
       d_stats(s),
       d_tds(qe->getTermDatabaseSygus()),
       d_hasSolution(false),
-      d_ceg_si(new CegSingleInv(qe)),
+      d_ceg_si(new CegSingleInv(qe, s)),
       d_templInfer(new SygusTemplateInfer),
       d_ceg_proc(new SynthConjectureProcess(qe)),
       d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
@@ -1037,7 +1037,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
   Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl;
   Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
   std::vector<Node> sols;
-  std::vector<int> statuses;
+  std::vector<int8_t> statuses;
   if (!getSynthSolutionsInternal(sols, statuses))
   {
     return;
@@ -1049,7 +1049,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
     if (!sol.isNull())
     {
       Node prog = d_embed_quant[0][i];
-      int status = statuses[i];
+      int8_t status = statuses[i];
       TypeNode tn = prog.getType();
       const DType& dt = tn.getDType();
       std::stringstream ss;
@@ -1161,7 +1161,7 @@ bool SynthConjecture::getSynthSolutions(
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> sols;
-  std::vector<int> statuses;
+  std::vector<int8_t> statuses;
   Trace("cegqi-debug") << "getSynthSolutions..." << std::endl;
   if (!getSynthSolutionsInternal(sols, statuses))
   {
@@ -1173,7 +1173,7 @@ bool SynthConjecture::getSynthSolutions(
   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
   {
     Node sol = sols[i];
-    int status = statuses[i];
+    int8_t status = statuses[i];
     Trace("cegqi-debug") << "...got " << i << ": " << sol
                          << ", status=" << status << std::endl;
     // get the builtin solution
@@ -1220,7 +1220,7 @@ void SynthConjecture::recordSolution(std::vector<Node>& vs)
 }
 
 bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
-                                                std::vector<int>& statuses)
+                                                std::vector<int8_t>& statuses)
 {
   if (!d_hasSolution)
   {
@@ -1234,7 +1234,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
     Assert(tn.isDatatype());
     // get the solution
     Node sol;
-    int status = -1;
+    int8_t status = -1;
     if (isSingleInvocation())
     {
       Assert(d_ceg_si != NULL);