Skip to content

Commit c1cb3e7

Browse files
committed
Optimize for 5 min timeout, too
1 parent 95716d9 commit c1cb3e7

1 file changed

Lines changed: 8 additions & 0 deletions

File tree

src/main.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,14 @@ void add_ganak_options()
193193
add_arg("--epsilon", conf.appmc_epsilon, fc_double, "AppMC epsilon");
194194
add_arg("--chronobt", conf.do_chronobt, fc_int, "ChronoBT. SAT must be DISABLED or this will fail");
195195
add_arg("--prob", conf.do_probabilistic_hashing, fc_int, "Use probabilistic hashing. When set to 0, we are not running in probabilistic mode, but in deterministic mode, i.e. delta is 0 in Ganak mode (not in case we switch to ApproxMC mode via --appmct)");
196+
program.add_argument("-fast")
197+
.action([&](const auto&) {
198+
arjun_cms_glob_mult = 0.1;
199+
simp_conf.oracle_mult = 0.1;
200+
arjun_backw_maxc = 50;
201+
})
202+
.flag()
203+
.help("Optimize for quick/easy instances (<5 mins)");
196204

197205
// d-DNNF compilation
198206
add_arg("--compile", conf.compile_fname, fc_string, "Compile the search trace into a (Decision-)d-DNNF circuit and write it to this file (d4 .nnf format). Forces a clean single-threaded search (no restarts, exact cache, no BuDDy/vivify, no Arjun/Puura). SAT oracle stays on (witnesses synthesized vars on projected inputs).");

0 commit comments

Comments
 (0)