From dbfd5033054ea3836126603f8f0bb3d427502b15 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Mon, 29 Jul 2024 13:31:24 -0700 Subject: [PATCH] random dec freq and seed in the commandline --- src/frontend/common/parameters.c | 4 +++ src/frontend/common/parameters.h | 2 ++ src/frontend/smt2/smt2_commands.c | 28 ++++++++++++++++++++ src/frontend/yices_smt2.c | 43 +++++++++++++++++++++++++++++++ src/mcsat/options.c | 2 ++ src/mcsat/options.h | 2 ++ src/mcsat/solver.c | 4 +-- 7 files changed, 83 insertions(+), 2 deletions(-) diff --git a/src/frontend/common/parameters.c b/src/frontend/common/parameters.c index 85d232ec9..41a945a2c 100644 --- a/src/frontend/common/parameters.c +++ b/src/frontend/common/parameters.c @@ -88,6 +88,8 @@ static const char * const param_names[NUM_PARAMETERS] = { "mcsat-nra-bound-min", "mcsat-nra-mgcd", "mcsat-nra-nlsat", + "mcsat-rand-dec-freq", + "mcsat-rand-dec-seed", "mcsat-var-order", "optimistic-fcheck", "prop-threshold", @@ -161,6 +163,8 @@ static const yices_param_t param_code[NUM_PARAMETERS] = { PARAM_MCSAT_NRA_BOUND_MIN, PARAM_MCSAT_NRA_MGCD, PARAM_MCSAT_NRA_NLSAT, + PARAM_MCSAT_RAND_DEC_FREQ, + PARAM_MCSAT_RAND_DEC_SEED, PARAM_MCSAT_VAR_ORDER, PARAM_OPTIMISTIC_FCHECK, PARAM_PROP_THRESHOLD, diff --git a/src/frontend/common/parameters.h b/src/frontend/common/parameters.h index e4912da4a..67c3f59db 100644 --- a/src/frontend/common/parameters.h +++ b/src/frontend/common/parameters.h @@ -115,6 +115,8 @@ typedef enum yices_param { PARAM_EMATCH_TERM_EPSILON, PARAM_EMATCH_TERM_ALPHA, // mcsat options + PARAM_MCSAT_RAND_DEC_FREQ, + PARAM_MCSAT_RAND_DEC_SEED, PARAM_MCSAT_NRA_MGCD, PARAM_MCSAT_NRA_NLSAT, PARAM_MCSAT_NRA_BOUND, diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c index b5879a41c..9b7f90307 100644 --- a/src/frontend/smt2/smt2_commands.c +++ b/src/frontend/smt2/smt2_commands.c @@ -5370,6 +5370,14 @@ static bool yices_get_option(smt2_globals_t *g, yices_param_t p) { print_boolean_value(g->mcsat_options.nra_nlsat); break; + case PARAM_MCSAT_RAND_DEC_FREQ: + print_float_value(g->mcsat_options.rand_dec_freq); + break; + + case PARAM_MCSAT_RAND_DEC_SEED: + print_int32_value(g->mcsat_options.rand_dec_seed); + break; + case PARAM_MCSAT_VAR_ORDER: print_terms_value(g, &g->var_order); break; @@ -6155,6 +6163,26 @@ static void yices_set_option(smt2_globals_t *g, const char *param, const param_v } break; + case PARAM_MCSAT_RAND_DEC_FREQ: + if (param_val_to_ratio(param, val, &x, &reason)) { + g->mcsat_options.rand_dec_freq = x; + context = g->ctx; + if (context != NULL) { + context->mcsat_options.rand_dec_freq = x; + } + } + break; + + case PARAM_MCSAT_RAND_DEC_SEED: + if (param_val_to_pos32(param, val, &n, &reason)) { + g->mcsat_options.rand_dec_seed = n; + context = g->ctx; + if (context != NULL) { + context->mcsat_options.rand_dec_seed = n; + } + } + break; + case PARAM_MCSAT_VAR_ORDER: if (param_val_to_terms(param, val, &terms, &reason)) { context = g->ctx; diff --git a/src/frontend/yices_smt2.c b/src/frontend/yices_smt2.c index 0bab70b95..187c7755c 100644 --- a/src/frontend/yices_smt2.c +++ b/src/frontend/yices_smt2.c @@ -108,6 +108,8 @@ static char *dimacsfile; // mcsat options static bool mcsat; +static double mcsat_rand_dec_freq; +static int32_t mcsat_rand_dec_seed; static bool mcsat_nra_mgcd; static bool mcsat_nra_nlsat; static bool mcsat_nra_bound; @@ -162,6 +164,8 @@ typedef enum optid { delegate_opt, // use an external sat solver dimacs_opt, // bitblast then export to DIMACS mcsat_opt, // enable mcsat + mcsat_rand_dec_freq_opt, // random decision frequency when making a decision in mcsat + mcsat_rand_dec_seed_opt, // seed for random decisions mcsat_nra_mgcd_opt, // use the mgcd instead psc in projection mcsat_nra_nlsat_opt, // use the nlsat projection instead of brown single-cell mcsat_nra_bound_opt, // search by increasing bound @@ -211,6 +215,8 @@ static option_desc_t options[NUM_OPTIONS] = { { "delegate", '\0', MANDATORY_STRING, delegate_opt }, { "dimacs", '\0', MANDATORY_STRING, dimacs_opt }, { "mcsat", '\0', FLAG_OPTION, mcsat_opt }, + { "mcsat-rand-dec-freq", '\0', MANDATORY_FLOAT, mcsat_rand_dec_freq_opt }, + { "mcsat-rand-dec-seed", '\0', MANDATORY_INT, mcsat_rand_dec_seed_opt }, { "mcsat-nra-mgcd", '\0', FLAG_OPTION, mcsat_nra_mgcd_opt }, { "mcsat-nra-nlsat", '\0', FLAG_OPTION, mcsat_nra_nlsat_opt }, { "mcsat-nra-bound", '\0', FLAG_OPTION, mcsat_nra_bound_opt }, @@ -289,6 +295,8 @@ static void print_mcsat_help(const char *progname) { printf("Usage: %s [option] filename\n" " or %s [option]\n\n", progname, progname); printf("MCSat options:\n" + " --mcsat-rand-dec-freq= Set the random decision frequency [0,1] (default = 0.02)\n" + " --mcsat-rand-dec-seed= Set the random decision seed (postive value)\n" " --mcsat-nra-mgcd Use model-based GCD instead of PSC for projection\n" " --mcsat-nra-nlsat Use NLSAT projection instead of Brown's single-cell construction\n" " --mcsat-nra-bound Search by increasing the bound on variable magnitude\n" @@ -388,6 +396,8 @@ static void parse_command_line(int argc, char *argv[]) { dimacsfile = NULL; mcsat = false; + mcsat_rand_dec_freq = -1; + mcsat_rand_dec_seed = -1; mcsat_nra_mgcd = false; mcsat_nra_nlsat = false; mcsat_nra_bound = false; @@ -545,6 +555,18 @@ static void parse_command_line(int argc, char *argv[]) { mcsat = true; break; + case mcsat_rand_dec_freq_opt: + if (! yices_has_mcsat()) goto no_mcsat; + if (! validate_double_option(&parser, &elem, 0.0, false, 1.0, false)) goto bad_usage; + mcsat_rand_dec_freq = elem.d_value; + break; + + case mcsat_rand_dec_seed_opt: + if (! yices_has_mcsat()) goto no_mcsat; + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + mcsat_rand_dec_seed = elem.i_value; + break; + case mcsat_nra_mgcd_opt: if (! yices_has_mcsat()) goto no_mcsat; mcsat_nra_mgcd = true; @@ -749,6 +771,27 @@ static void setup_options_mcsat(void) { aval_true = attr_vtbl_symbol(__smt2_globals.avtbl, "true"); + if (mcsat_rand_dec_freq >= 0) { + aval_t aval_rand; + rational_t q; + q_init(&q); + // accurate upto 3 decimal places + q_set_int32(&q, (int32_t)(mcsat_rand_dec_freq*1000), 1000); + aval_rand = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-mcsat-rand-dec-freq", aval_rand); + q_clear(&q); + } + + if (mcsat_rand_dec_seed >= 0) { + aval_t aval_seed; + rational_t q; + q_init(&q); + q_set32(&q, mcsat_rand_dec_seed); + aval_seed = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-mcsat-rand-dec-seed", aval_seed); + q_clear(&q); + } + if (mcsat_nra_mgcd) { smt2_set_option(":yices-mcsat-nra-mgcd", aval_true); } diff --git a/src/mcsat/options.c b/src/mcsat/options.c index 0db08ec87..1b79af02a 100644 --- a/src/mcsat/options.c +++ b/src/mcsat/options.c @@ -21,6 +21,8 @@ #include extern void init_mcsat_options(mcsat_options_t *opts) { + opts->rand_dec_freq = 0.02; + opts->rand_dec_seed = 0xabcdef98; opts->nra_nlsat = false; opts->nra_mgcd = false; opts->nra_bound = false; diff --git a/src/mcsat/options.h b/src/mcsat/options.h index b8ca4e785..66d23bd3a 100644 --- a/src/mcsat/options.h +++ b/src/mcsat/options.h @@ -28,6 +28,8 @@ * Options for the mcsat solver. */ typedef struct mcsat_options_s { + double rand_dec_freq; + int32_t rand_dec_seed; bool nra_mgcd; bool nra_nlsat; bool nra_bound; diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 4ac73fdaa..3a775a2d8 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -332,8 +332,8 @@ static void mcsat_heuristics_init(mcsat_solver_t* mcsat) { mcsat->heuristic_params.restart_interval = 10; mcsat->heuristic_params.lemma_restart_weight_type = LEMMA_WEIGHT_SIZE; - mcsat->heuristic_params.random_decision_freq = 0.02; - mcsat->heuristic_params.random_decision_seed = 0xabcdef98; + mcsat->heuristic_params.random_decision_freq = mcsat->ctx->mcsat_options.rand_dec_freq; + mcsat->heuristic_params.random_decision_seed = mcsat->ctx->mcsat_options.rand_dec_seed; } static