Disable argument relevance for sygus by default (#2288)

5 files changed, 45 insertions, 28 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index aac84e92c..5f6638dce 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1175,6 +1175,14 @@ header = "options/quantifiers_options.h"
   default    = "true"
   help       = "use optimized approach for evaluation in sygus"
 
+[[option]]
+  name       = "sygusArgRelevant"
+  category   = "regular"
+  long       = "sygus-arg-relevant"
+  type       = "bool"
+  default    = "false"
+  help       = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
+  
 # Internal uses of sygus
 
 [[option]]
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index 76e484549..b0b6159be 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -17,6 +17,7 @@
 #include <stack>
 
 #include "expr/datatype.h"
+#include "options/quantifiers_options.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -533,39 +534,43 @@ Node CegConjectureProcess::postSimplify(Node q)
   Trace("sygus-process") << "Post-simplify conjecture : " << q << std::endl;
   Assert(q.getKind() == FORALL);
 
-  // initialize the information about each function to synthesize
-  for (unsigned i = 0; i < q[0].getNumChildren(); i++)
+  if (options::sygusArgRelevant())
   {
-    Node f = q[0][i];
-    if (f.getType().isFunction())
+    // initialize the information about each function to synthesize
+    for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
     {
-      d_sf_info[f].init(f);
+      Node f = q[0][i];
+      if (f.getType().isFunction())
+      {
+        d_sf_info[f].init(f);
+      }
     }
-  }
 
-  // get the base on the conjecture
-  Node base = q[1];
-  std::unordered_set<Node, NodeHashFunction> synth_fv;
-  if (base.getKind() == NOT && base[0].getKind() == FORALL)
-  {
-    for (unsigned j = 0; j < base[0][0].getNumChildren(); j++)
+    // get the base on the conjecture
+    Node base = q[1];
+    std::unordered_set<Node, NodeHashFunction> synth_fv;
+    if (base.getKind() == NOT && base[0].getKind() == FORALL)
     {
-      synth_fv.insert(base[0][0][j]);
+      for (unsigned j = 0, size = base[0][0].getNumChildren(); j < size; j++)
+      {
+        synth_fv.insert(base[0][0][j]);
+      }
+      base = base[0][1];
     }
-    base = base[0][1];
-  }
-  std::vector<Node> conjuncts;
-  getComponentVector(AND, base, conjuncts);
+    std::vector<Node> conjuncts;
+    getComponentVector(AND, base, conjuncts);
 
-  // process the conjunctions
-  for (std::map<Node, CegConjectureProcessFun>::iterator it = d_sf_info.begin();
-       it != d_sf_info.end();
-       ++it)
-  {
-    Node f = it->first;
-    for (unsigned i = 0; i < conjuncts.size(); i++)
+    // process the conjunctions
+    for (std::map<Node, CegConjectureProcessFun>::iterator it =
+             d_sf_info.begin();
+         it != d_sf_info.end();
+         ++it)
     {
-      processConjunct(conjuncts[i], f, synth_fv);
+      Node f = it->first;
+      for (const Node& conj : conjuncts)
+      {
+        processConjunct(conj, f, synth_fv);
+      }
     }
   }
 
@@ -587,6 +592,10 @@ void CegConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
 
 bool CegConjectureProcess::isArgRelevant(Node f, unsigned i)
 {
+  if (!options::sygusArgRelevant())
+  {
+    return true;
+  }
   std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f);
   if (its != d_sf_info.end())
   {
diff --git a/test/regress/regress1/sygus/process-10-vars.sy b/test/regress/regress1/sygus/process-10-vars.sy
index 523abd70d..77990473f 100644
--- a/test/regress/regress1/sygus/process-10-vars.sy
+++ b/test/regress/regress1/sygus/process-10-vars.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-arg-relevant
 ; EXPECT: unsat
 (set-logic LIA)
 
diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy
index a107fd88b..214da82c8 100644
--- a/test/regress/regress2/sygus/process-10-vars-2fun.sy
+++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-repair-const
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant
 ; EXPECT: unsat
 (set-logic LIA)
 
diff --git a/test/regress/regress2/sygus/process-arg-invariance.sy b/test/regress/regress2/sygus/process-arg-invariance.sy
index 3c18b6c75..2f1b74ddf 100644
--- a/test/regress/regress2/sygus/process-arg-invariance.sy
+++ b/test/regress/regress2/sygus/process-arg-invariance.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant
 ; EXPECT: unsat
 (set-logic LIA)