Flag to check invariance of entire values in sygus explain (#1908)

1 files changed, 17 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index 818f51438..056ea7ed5 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -182,6 +182,15 @@ class SygusExplain
    * - (if applicable) exp => ( n != vnr ).
    *
    * This function updates sz to be the term size of [[exp]]_n.
+   *
+   * If strict is false, then we also test whether the invariance test holds
+   * independently of the entire value of vn.
+   *
+   * The argument var_count is used for tracking the variables that we introduce
+   * to generalize the shape of vn. This map is passed to
+   * TermDbSygus::getFreeVarInc. This argument should be used if we are
+   * calling this function multiple times and the generalization should not
+   * introduce variables that shadow the variables introduced on previous calls.
    */
   void getExplanationFor(Node n,
                          Node vn,
@@ -192,7 +201,14 @@ class SygusExplain
   void getExplanationFor(Node n,
                          Node vn,
                          std::vector<Node>& exp,
-                         SygusInvarianceTest& et);
+                         SygusInvarianceTest& et,
+                         bool strict = true);
+  void getExplanationFor(Node n,
+                         Node vn,
+                         std::vector<Node>& exp,
+                         SygusInvarianceTest& et,
+                         std::map<TypeNode, int>& var_count,
+                         bool strict = true);
 
  private:
   /** sygus term database associated with this utility */