From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 16 Oct 2018 07:39:03 +0000 (-0500)
Subject: Option for shuffling condition pool in CegisUnif (#2587)
X-Git-Tag: cvc5-1.0.0~4422
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f27d423510c4e29ac32aed06912dc7284689181c;p=cvc5.git

Option for shuffling condition pool in CegisUnif (#2587)
---

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index f3baa8214..07c11d73a 100644
--- 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 b8d98a6f7..ee07efdfe 100644
--- 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 7b07de34e..179a5ac16 100644
--- 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"