1 files changed, 35 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index a4f276792..5d7017a1c 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -26,7 +26,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
+SygusUnif::SygusUnif()
+    : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false)
+{
+}
 SygusUnif::~SygusUnif() {}
 
 void SygusUnif::initializeCandidate(
@@ -42,9 +45,40 @@ void SygusUnif::initializeCandidate(
   d_strategy[f].initialize(qe, f, enums);
 }
 
+Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
+{
+  unsigned minSize = 0;
+  Node minTerm;
+  std::map<Node, unsigned>::iterator it;
+  for (const Node& n : terms)
+  {
+    it = d_termToSize.find(n);
+    unsigned ssize = 0;
+    if (it == d_termToSize.end())
+    {
+      ssize = d_tds->getSygusTermSize(n);
+      d_termToSize[n] = ssize;
+    }
+    else
+    {
+      ssize = it->second;
+    }
+    if (minTerm.isNull() || ssize < minSize)
+    {
+      minTerm = n;
+      minSize = ssize;
+    }
+  }
+  return minTerm;
+}
+
 Node SygusUnif::constructBestSolvedTerm(Node e, const std::vector<Node>& solved)
 {
   Assert(!solved.empty());
+  if (d_enableMinimality)
+  {
+    return getMinimalTerm(solved);
+  }
   return solved[0];
 }