diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-10-16 02:39:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-16 02:39:03 -0500 |
| commit | f27d423510c4e29ac32aed06912dc7284689181c (patch) | |
| tree | 3381885cabc74e9ba8e4adbc05697dc7fe8e54bc | |
| parent | 0bc40f92221e5e8c669e2409ff3120d5c2257aec (diff) | |
Option for shuffling condition pool in CegisUnif (#2587)
| -rw-r--r-- | src/options/quantifiers_options.toml | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 12 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.h | 1 |
3 files changed, 21 insertions, 0 deletions
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 @@ -984,6 +984,14 @@ header = "options/quantifiers_options.h" 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" long = "sygus-unif-boolean-heuristic-dt" 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" |