sygusComp2018: Improvements to datatypes sygus solver (#2177)

1 files changed, 12 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 665390271..ddf52001e 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -284,11 +284,22 @@ void SygusExplain::getExplanationFor(Node n,
                                      Node vnr,
                                      unsigned& sz)
 {
+  std::map<TypeNode, int> var_count;
+  return getExplanationFor(n, vn, exp, et, vnr, var_count, sz);
+}
+
+void SygusExplain::getExplanationFor(Node n,
+                                     Node vn,
+                                     std::vector<Node>& exp,
+                                     SygusInvarianceTest& et,
+                                     Node vnr,
+                                     std::map<TypeNode, int>& var_count,
+                                     unsigned& sz)
+{
   // naive :
   // return getExplanationForEquality( n, vn, exp );
 
   // set up the recursion object;
-  std::map<TypeNode, int> var_count;
   TermRecBuild trb;
   trb.init(vn);
   Node vnr_exp;