2929#include < memory>
3030#include < string>
3131#include < vector>
32+ #include < charconv>
33+ #include < stdexcept>
3234#if defined(__GNUC__) && defined(__linux__)
3335#include < cfenv>
3436#endif
@@ -77,14 +79,30 @@ int with_e = 0;
7779bool do_arjun = true ;
7880bool do_backbone = false ;
7981
82+ static int fc_int (const std::string& s) {
83+ int val = 0 ;
84+ auto [ptr, ec] = std::from_chars (s.data (), s.data () + s.size (), val);
85+ if (ec != std::errc{}) throw std::invalid_argument (" not an integer: " + s);
86+ if (ptr != s.data () + s.size ()) throw std::invalid_argument (" trailing characters in integer: " + s);
87+ return val;
88+ }
89+ static double fc_double (const std::string& s) {
90+ size_t pos = 0 ;
91+ double val;
92+ try { val = std::stod (s, &pos); }
93+ catch (const std::exception&) { throw std::invalid_argument (" not a double: " + s); }
94+ if (pos != s.size ()) throw std::invalid_argument (" trailing characters in double: " + s);
95+ return val;
96+ }
97+
8098#define myopt (name, var, fun, hhelp ) \
8199 program.add_argument(name) \
82- .action([&](const auto & a) {var = std:: fun (a. c_str () );}) \
100+ .action([&](const auto & a) {var = fun (a);}) \
83101 .default_value(var) \
84102 .help(hhelp)
85103#define myopt2 (name1, name2, var, fun, hhelp ) \
86104 program.add_argument(name1, name2) \
87- .action([&](const auto & a) {var = std:: fun (a. c_str () );}) \
105+ .action([&](const auto & a) {var = fun (a);}) \
88106 .default_value(var) \
89107 .help(hhelp)
90108
@@ -108,14 +126,14 @@ void add_appmc_options()
108126 sparse = tmp.get_sparse ();
109127 seed = tmp.get_seed ();
110128
111- myopt2 (" -v" , " --verb" , verb, atoi , " Verbosity" );
112- myopt2 (" -s" , " --seed" , seed, atoi , " Seed" );
113- myopt2 (" -e" , " --epsilon" , epsilon, stod ,
129+ myopt2 (" -v" , " --verb" , verb, fc_int , " Verbosity" );
130+ myopt2 (" -s" , " --seed" , seed, fc_int , " Seed" );
131+ myopt2 (" -e" , " --epsilon" , epsilon, fc_double ,
114132 " Tolerance parameter, i.e. how close is the count from the correct count? "
115133 " Count output is within bounds of (exact_count/(1+e)) < count < (exact_count*(1+e)). "
116134 " So e=0.8 means we'll output at most 180%% of exact count and at least 55%% of exact count. "
117135 " Lower value means more precise." );
118- myopt2 (" -d" , " --delta" , delta, stod , " Confidence parameter, i.e. how sure are we of the result? "
136+ myopt2 (" -d" , " --delta" , delta, fc_double , " Confidence parameter, i.e. how sure are we of the result? "
119137 " (1-d) = probability the count is within range as per epsilon parameter. "
120138 " So d=0.2 means we are 80%% sure the count is within range as specified by epsilon. "
121139 " The lower, the higher confidence we have in the count." );
@@ -125,29 +143,29 @@ void add_appmc_options()
125143 .help (" Print version and exit" );
126144
127145 /* arjun_options.add_options() */
128- myopt (" --arjun" , do_arjun, atoi , " Use arjun to minimize sampling set" );
146+ myopt (" --arjun" , do_arjun, fc_int , " Use arjun to minimize sampling set" );
129147
130148 /* improvement_options.add_options() */
131- myopt (" --sparse" , sparse, atoi ,
149+ myopt (" --sparse" , sparse, fc_int ,
132150 " 0 = (default) Do not use sparse method. 1 = Generate sparse XORs when possible." );
133- myopt (" --reusemodels" , reuse_models, atoi , " Reuse models while counting solutions" );
134- myopt (" --forcesolextension" , force_sol_extension, atoi ,
151+ myopt (" --reusemodels" , reuse_models, fc_int , " Reuse models while counting solutions" );
152+ myopt (" --forcesolextension" , force_sol_extension, fc_int ,
135153 " Use trick of not extending solutions in the SAT solver to full solution" );
136- myopt (" --withe" , with_e, atoi , " Eliminate variables and simplify CNF as well" );
137- myopt (" --eiter1" , simp_conf.iter1 , atoi , " Num iters of E on 1st round" );
138- myopt (" --eiter2" , simp_conf.iter2 , atoi , " Num iters of E on 1st round" );
139- myopt (" --evivif" , simp_conf.oracle_vivify , atoi , " E vivif" );
140- myopt (" --esparsif" , simp_conf.oracle_sparsify , atoi , " E sparsify" );
141- myopt (" --egetreds" , simp_conf.oracle_vivify_get_learnts , atoi , " Get redundant from E" );
154+ myopt (" --withe" , with_e, fc_int , " Eliminate variables and simplify CNF as well" );
155+ myopt (" --eiter1" , simp_conf.iter1 , fc_int , " Num iters of E on 1st round" );
156+ myopt (" --eiter2" , simp_conf.iter2 , fc_int , " Num iters of E on 1st round" );
157+ myopt (" --evivif" , simp_conf.oracle_vivify , fc_int , " E vivif" );
158+ myopt (" --esparsif" , simp_conf.oracle_sparsify , fc_int , " E sparsify" );
159+ myopt (" --egetreds" , simp_conf.oracle_vivify_get_learnts , fc_int , " Get redundant from E" );
142160
143161 /* misc_options.add_options() */
144- myopt (" --verbcls" , verb_cls, atoi , " Print banning clause + xor clauses. Highly verbose." );
145- myopt (" --simplify" , simplify, atoi , " Simplify aggressiveness" );
146- myopt (" --velimratio" , var_elim_ratio, stod , " Variable elimination ratio for each simplify run" );
147- myopt (" --dumpintercnf" , dump_intermediary_cnf, atoi ,
162+ myopt (" --verbcls" , verb_cls, fc_int , " Print banning clause + xor clauses. Highly verbose." );
163+ myopt (" --simplify" , simplify, fc_int , " Simplify aggressiveness" );
164+ myopt (" --velimratio" , var_elim_ratio, fc_double , " Variable elimination ratio for each simplify run" );
165+ myopt (" --dumpintercnf" , dump_intermediary_cnf, fc_int ,
148166 " Dump intermediary CNFs during solving into files cnf_dump-X.cnf. If set to 1 only UNSAT is dumped, if set to 2, all are dumped" );
149- myopt (" --debug" , debug, atoi , " Turn on more heavy internal debugging" );
150- myopt (" --backbone" , do_backbone, atoi , " Run backbone analysis" );
167+ myopt (" --debug" , debug, fc_int , " Turn on more heavy internal debugging" );
168+ myopt (" --backbone" , do_backbone, fc_int , " Run backbone analysis" );
151169
152170 program.add_argument (" inputfile" ).remaining ().help (" input CNF" );
153171}
0 commit comments