Expand definitions in sygus operators at the SMT level (#7077)

Eliminates another call to currentSmtEngine.

This PR ensures we remember the mapping between operators that are embedded in sygus datatypes during preprocessing, instead of computing this within the sygus datatypes utilities when solving.

3 files changed, 55 insertions, 8 deletions

diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 72ddd7b0e..f1f7b45a4 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -22,8 +22,6 @@
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
 #include "smt/env.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "theory/evaluator.h"
 #include "theory/rewriter.h"
 
@@ -175,12 +173,9 @@ Node mkSygusTerm(const DType& dt,
       }
       else
       {
-        // Only expand definitions if the operator is not constant, since
-        // calling expandDefinitions on them should be a no-op. This check
-        // ensures we don't try to expand e.g. bitvector extract operators,
-        // whose type is undefined, and thus should not be passed to
-        // expandDefinitions.
-        opn = smt::currentSmtEngine()->expandDefinitions(op);
+        // Get the expanded definition form, if it has been marked. This ensures
+        // that user-defined functions have been eliminated from op.
+        opn = getExpandedDefinitionForm(op);
         opn = Rewriter::rewrite(opn);
         SygusOpRewrittenAttribute sora;
         op.setAttribute(sora, opn);
@@ -736,6 +731,28 @@ unsigned getSygusTermSize(Node n)
   return weight + sum;
 }
 
+/**
+ * Map terms to the result of expand definitions calling smt::expandDefinitions
+ * on it.
+ */
+struct SygusExpDefFormAttributeId
+{
+};
+typedef expr::Attribute<SygusExpDefFormAttributeId, Node>
+    SygusExpDefFormAttribute;
+
+void setExpandedDefinitionForm(Node op, Node eop)
+{
+  op.setAttribute(SygusExpDefFormAttribute(), eop);
+}
+
+Node getExpandedDefinitionForm(Node op)
+{
+  Node eop = op.getAttribute(SygusExpDefFormAttribute());
+  // if not set, assume original
+  return eop.isNull() ? op : eop;
+}
+
 }  // namespace utils
 }  // namespace datatypes
 }  // namespace theory
diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h
index 35672434c..5784fe34a 100644
--- a/src/theory/datatypes/sygus_datatype_utils.h
+++ b/src/theory/datatypes/sygus_datatype_utils.h
@@ -232,6 +232,22 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
  * in n.
  */
 unsigned getSygusTermSize(Node n);
+
+/**
+ * Set expanded definition form of sygus op to eop. This is called when
+ * we require associating a sygus operator op to its expanded form, which
+ * replaces user-defined functions with their definitions. This allows
+ * the utilities above to consider op to be the original form, which is
+ * printed in the final solution (see isExternal to sygusToBuiltin above),
+ * whereas the internal solver will reason about eop.
+ */
+void setExpandedDefinitionForm(Node op, Node eop);
+/**
+ * Get the expanded definition form of sygus operator op, returns the
+ * expanded form if the above method has been called for op, or returns op
+ * otherwise.
+ */
+Node getExpandedDefinitionForm(Node op);
 // ------------------------ end sygus utils
 
 }  // namespace utils
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index f9aa5bdc3..7a8ff0b1d 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -190,6 +190,20 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
     {
       d_hasBoolConnective = true;
     }
+    if (Trace.isOn("sygus-db"))
+    {
+      Node eop = datatypes::utils::getExpandedDefinitionForm(sop);
+      Trace("sygus-db") << "Expanded form: ";
+      if (eop == sop)
+      {
+        Trace("sygus-db") << "same";
+      }
+      else
+      {
+        Trace("sygus-db") << eop;
+      }
+      Trace("sygus-db") << std::endl;
+    }
   }
   // compute minimum type depth information
   computeMinTypeDepthInternal(tn, 0);