@@ -110,11 +110,11 @@ static char *dimacsfile;
110110static bool mcsat ;
111111static double mcsat_rand_dec_freq ;
112112static int32_t mcsat_rand_dec_seed ;
113- static bool mcsat_nra_mgcd ;
114- static bool mcsat_nra_nlsat ;
115- static bool mcsat_nra_bound ;
116- static int32_t mcsat_nra_bound_min ;
117- static int32_t mcsat_nra_bound_max ;
113+ static bool mcsat_na_mgcd ;
114+ static bool mcsat_na_nlsat ;
115+ static bool mcsat_na_bound ;
116+ static int32_t mcsat_na_bound_min ;
117+ static int32_t mcsat_na_bound_max ;
118118static int32_t mcsat_bv_var_size ;
119119static bool mcsat_partial_restart ;
120120
@@ -167,11 +167,11 @@ typedef enum optid {
167167 mcsat_opt , // enable mcsat
168168 mcsat_rand_dec_freq_opt , // random decision frequency when making a decision in mcsat
169169 mcsat_rand_dec_seed_opt , // seed for random decisions
170- mcsat_nra_mgcd_opt , // use the mgcd instead psc in projection
171- mcsat_nra_nlsat_opt , // use the nlsat projection instead of brown single-cell
172- mcsat_nra_bound_opt , // search by increasing bound
173- mcsat_nra_bound_min_opt , // set initial bound
174- mcsat_nra_bound_max_opt , // set maximal bound
170+ mcsat_na_mgcd_opt , // use the mgcd instead psc in projection
171+ mcsat_na_nlsat_opt , // use the nlsat projection instead of brown single-cell
172+ mcsat_na_bound_opt , // search by increasing bound
173+ mcsat_na_bound_min_opt , // set initial bound
174+ mcsat_na_bound_max_opt , // set maximal bound
175175 mcsat_bv_var_size_opt , // set size of bitvector variables
176176 mcsat_partial_restart_opt , // enable partial restart heuristic in MCSAT
177177 trace_opt , // enable a trace tag
@@ -219,11 +219,11 @@ static option_desc_t options[NUM_OPTIONS] = {
219219 { "mcsat" , '\0' , FLAG_OPTION , mcsat_opt },
220220 { "mcsat-rand-dec-freq" , '\0' , MANDATORY_FLOAT , mcsat_rand_dec_freq_opt },
221221 { "mcsat-rand-dec-seed" , '\0' , MANDATORY_INT , mcsat_rand_dec_seed_opt },
222- { "mcsat-nra -mgcd" , '\0' , FLAG_OPTION , mcsat_nra_mgcd_opt },
223- { "mcsat-nra -nlsat" , '\0' , FLAG_OPTION , mcsat_nra_nlsat_opt },
224- { "mcsat-nra -bound" , '\0' , FLAG_OPTION , mcsat_nra_bound_opt },
225- { "mcsat-nra -bound-min" , '\0' , MANDATORY_INT , mcsat_nra_bound_min_opt },
226- { "mcsat-nra -bound-max" , '\0' , MANDATORY_INT , mcsat_nra_bound_max_opt },
222+ { "mcsat-na -mgcd" , '\0' , FLAG_OPTION , mcsat_na_mgcd_opt },
223+ { "mcsat-na -nlsat" , '\0' , FLAG_OPTION , mcsat_na_nlsat_opt },
224+ { "mcsat-na -bound" , '\0' , FLAG_OPTION , mcsat_na_bound_opt },
225+ { "mcsat-na -bound-min" , '\0' , MANDATORY_INT , mcsat_na_bound_min_opt },
226+ { "mcsat-na -bound-max" , '\0' , MANDATORY_INT , mcsat_na_bound_max_opt },
227227 { "mcsat-bv-var-size" , '\0' , MANDATORY_INT , mcsat_bv_var_size_opt },
228228 { "mcsat-partial-restart" , '\0' , FLAG_OPTION , mcsat_partial_restart_opt },
229229 { "trace" , 't' , MANDATORY_STRING , trace_opt },
@@ -300,11 +300,11 @@ static void print_mcsat_help(const char *progname) {
300300 printf ("MCSat options:\n"
301301 " --mcsat-rand-dec-freq=<B> Set the random decision frequency [0,1] (default = 0.02)\n"
302302 " --mcsat-rand-dec-seed=<B> Set the random decision seed (postive value)\n"
303- " --mcsat-nra -mgcd Use model-based GCD instead of PSC for projection\n"
304- " --mcsat-nra -nlsat Use NLSAT projection instead of Brown's single-cell construction\n"
305- " --mcsat-nra -bound Search by increasing the bound on variable magnitude\n"
306- " --mcsat-nra -bound-min=<B> Set initial lower bound\n"
307- " --mcsat-nra -bound-max=<B> Set maximal bound for search\n"
303+ " --mcsat-na -mgcd Use model-based GCD instead of PSC for projection\n"
304+ " --mcsat-na -nlsat Use NLSAT projection instead of Brown's single-cell construction\n"
305+ " --mcsat-na -bound Search by increasing the bound on variable magnitude\n"
306+ " --mcsat-na -bound-min=<B> Set initial lower bound\n"
307+ " --mcsat-na -bound-max=<B> Set maximal bound for search\n"
308308 " --mcsat-bv-var-size=<B> Set size of bit-vector variables in MCSAT search\n"
309309 " --mcsat-partial-restart Enable partial restart heuristic in MCSAT search"
310310 "\n" );
@@ -402,11 +402,11 @@ static void parse_command_line(int argc, char *argv[]) {
402402 mcsat = false;
403403 mcsat_rand_dec_freq = -1 ;
404404 mcsat_rand_dec_seed = -1 ;
405- mcsat_nra_mgcd = false;
406- mcsat_nra_nlsat = false;
407- mcsat_nra_bound = false;
408- mcsat_nra_bound_min = -1 ;
409- mcsat_nra_bound_max = -1 ;
405+ mcsat_na_mgcd = false;
406+ mcsat_na_nlsat = false;
407+ mcsat_na_bound = false;
408+ mcsat_na_bound_min = -1 ;
409+ mcsat_na_bound_max = -1 ;
410410 mcsat_bv_var_size = -1 ;
411411 mcsat_partial_restart = false;
412412
@@ -572,31 +572,31 @@ static void parse_command_line(int argc, char *argv[]) {
572572 mcsat_rand_dec_seed = elem .i_value ;
573573 break ;
574574
575- case mcsat_nra_mgcd_opt :
575+ case mcsat_na_mgcd_opt :
576576 if (! yices_has_mcsat ()) goto no_mcsat ;
577- mcsat_nra_mgcd = true;
577+ mcsat_na_mgcd = true;
578578 break ;
579579
580- case mcsat_nra_nlsat_opt :
580+ case mcsat_na_nlsat_opt :
581581 if (! yices_has_mcsat ()) goto no_mcsat ;
582- mcsat_nra_nlsat = true;
582+ mcsat_na_nlsat = true;
583583 break ;
584584
585- case mcsat_nra_bound_opt :
585+ case mcsat_na_bound_opt :
586586 if (! yices_has_mcsat ()) goto no_mcsat ;
587- mcsat_nra_bound = true;
587+ mcsat_na_bound = true;
588588 break ;
589589
590- case mcsat_nra_bound_min_opt :
590+ case mcsat_na_bound_min_opt :
591591 if (! yices_has_mcsat ()) goto no_mcsat ;
592592 if (! validate_integer_option (& parser , & elem , 0 , INT32_MAX )) goto bad_usage ;
593- mcsat_nra_bound_min = elem .i_value ;
593+ mcsat_na_bound_min = elem .i_value ;
594594 break ;
595595
596- case mcsat_nra_bound_max_opt :
596+ case mcsat_na_bound_max_opt :
597597 if (! yices_has_mcsat ()) goto no_mcsat ;
598598 if (! validate_integer_option (& parser , & elem , 0 , INT32_MAX )) goto bad_usage ;
599- mcsat_nra_bound_max = elem .i_value ;
599+ mcsat_na_bound_max = elem .i_value ;
600600 break ;
601601
602602 case mcsat_bv_var_size_opt :
@@ -801,35 +801,35 @@ static void setup_options_mcsat(void) {
801801 q_clear (& q );
802802 }
803803
804- if (mcsat_nra_mgcd ) {
805- smt2_set_option (":yices-mcsat-nra -mgcd" , aval_true );
804+ if (mcsat_na_mgcd ) {
805+ smt2_set_option (":yices-mcsat-na -mgcd" , aval_true );
806806 }
807807
808- if (mcsat_nra_nlsat ) {
809- smt2_set_option (":yices-mcsat-nra -nlsat" , aval_true );
808+ if (mcsat_na_nlsat ) {
809+ smt2_set_option (":yices-mcsat-na -nlsat" , aval_true );
810810 }
811811
812- if (mcsat_nra_bound ) {
813- smt2_set_option (":yices-mcsat-nra -bound" , aval_true );
812+ if (mcsat_na_bound ) {
813+ smt2_set_option (":yices-mcsat-na -bound" , aval_true );
814814 }
815815
816- if (mcsat_nra_bound_min >= 0 ) {
816+ if (mcsat_na_bound_min >= 0 ) {
817817 aval_t aval_bound_min ;
818818 rational_t q ;
819819 q_init (& q );
820- q_set32 (& q , mcsat_nra_bound_min );
820+ q_set32 (& q , mcsat_na_bound_min );
821821 aval_bound_min = attr_vtbl_rational (__smt2_globals .avtbl , & q );
822- smt2_set_option (":yices-mcsat-nra -bound-min" , aval_bound_min );
822+ smt2_set_option (":yices-mcsat-na -bound-min" , aval_bound_min );
823823 q_clear (& q );
824824 }
825825
826- if (mcsat_nra_bound_max >= 0 ) {
826+ if (mcsat_na_bound_max >= 0 ) {
827827 aval_t aval_bound_max ;
828828 rational_t q ;
829829 q_init (& q );
830- q_set32 (& q , mcsat_nra_bound_max );
830+ q_set32 (& q , mcsat_na_bound_max );
831831 aval_bound_max = attr_vtbl_rational (__smt2_globals .avtbl , & q );
832- smt2_set_option (":yices-mcsat-nra -bound-max" , aval_bound_max );
832+ smt2_set_option (":yices-mcsat-na -bound-max" , aval_bound_max );
833833 q_clear (& q );
834834 }
835835
0 commit comments