Option for shuffling condition pool in CegisUnif (#2587)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index f3baa82145abd3fc1f8a544fec0beb61fcdd7519..07c11d73a6b6a7677a85c821a8fbc35eefa375ab 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -983,6 +983,14 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
 
+[[option]]
+  name       = "sygusUnifShuffleCond"
+  category   = "regular"
+  long       = "sygus-unif-shuffle-cond"
+  type       = "bool"
+  default    = "false"
+  help       = "Shuffle condition pool when building solutions (may change solutions sizes)"
+
 [[option]]
   name       = "sygusUnifBooleanHeuristicDt"
   category   = "regular"

diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index b8d98a6f7462af5cc910822c9615848b51fd26c7..ee07efdfe78b685f8e704b55a8ad0be22114df9a 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -20,6 +20,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "util/random.h"
 
 #include <math.h>
 
@@ -563,6 +564,17 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons,
   // add conditions
   d_conds.clear();
   d_conds.insert(d_conds.end(), d_cond_mvs.begin(), d_cond_mvs.end());
+  // shuffle conditions before bulding DT
+  //
+  // this does not impact whether it's possible to build a solution, but it does
+  // impact the potential size of the resulting solution (can make it smaller,
+  // bigger, or have no impact) and which conditions will be present in the DT,
+  // which influences the "quality" of the solution for cases not covered in the
+  // current data points
+  if (options::sygusUnifShuffleCond())
+  {
+    std::shuffle(d_conds.begin(), d_conds.end(), Random::getRandom());
+  }
   unsigned num_conds = d_conds.size();
   for (unsigned i = 0; i < num_conds; ++i)
   {

diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 7b07de34eecd12d48eb010a732a67f11c9eb37ea..179a5ac16ee7ba851bb7035623799c3b599752cb 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -18,6 +18,7 @@
 #define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
 
 #include <map>
+#include "options/main_options.h"
 #include "theory/quantifiers/sygus/sygus_unif.h"
 
 #include "theory/quantifiers/lazy_trie.h"