Skip to content

Commit f058da1

Browse files
author
Tero Laitinen
committed
fixed default values, xor/total time now seconds
1 parent 43d7bbc commit f058da1

File tree

2 files changed

+37
-35
lines changed
  • up-dsimplex-minisat/minisat/core
  • up-minisat/minisat/core

2 files changed

+37
-35
lines changed

‎up-dsimplex-minisat/minisat/core/Main.C

+20-18
Original file line numberDiff line numberDiff line change
@@ -251,8 +251,10 @@ void printStats(Solver& solver, StopWatch& totalTime)
251251
if (up.stats.learnts)
252252
reportf("UP-xor learnt size : %.2f\n", (float) up.stats.learntLits / (float) up.stats.learnts);
253253
reportf("UP-xor explained : %-12lld\n", up.stats.explained);
254-
reportf("total time : %-12lld\n", totalTime.total());
255-
reportf("xor time : %-12lld\n", solver.xorTime.total());
254+
reportf("total time : %-12g\n", ((double) totalTime.total()) / ((double) 1000000000.0) );
255+
reportf("xor time : %-12g\n", ((double) solver.xorTime.total()) / ((double) 1000000000.0));
256+
257+
256258
reportf("learnt / conflict : %.2f\n", (float) solver.learnts_in_conflicts / solver.conflicts);
257259

258260

@@ -276,25 +278,25 @@ static void SIGINT_handler(int signum) {
276278

277279
void printUsage(char** argv)
278280
{
281+
Solver s;
279282
reportf("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n\n", argv[0]);
280283
reportf("OPTIONS:\n\n");
281284
reportf(" -polarity-mode = {true,false,rnd} default: false\n");
282-
reportf(" -xor-propagation = {eager,lazy} default: eager\n");
283-
reportf(" -xor-split = <num> [ 1 - N ] default: 1\n");
284-
reportf(" -xor-lazy-factor = <num> [ 1 - N ] default: 2\n");
285-
reportf(" -xor-rule-priority = {external,internal} default: external\n");
286-
// reportf(" -xor-internal-vars = {on,off} default: off\n");
287-
reportf(" -xor-store-clauses = {true,false} default: false\n");
288-
reportf(" -xor-exp-length = <num> [ 3 - N ] default: 3\n");
289-
reportf(" -xor-bump-activity = {0,1,2} default: 0\n");
290-
reportf(" -xor-even-elim = {true,false} default: false\n");
291-
reportf(" -xor-up-xors = {true,false} default: true\n");
292-
reportf(" -xor-up-cache-exp = {true,false} default: true\n");
293-
reportf(" -xor-split-cycle-components = {true,false} default: true\n");
294-
reportf(" -xor-create-vars = {true,false} default: false\n");
295-
reportf(" -xor-to-cnf = {true,false} default: false\n");
296-
reportf(" -xor-deep-cuts = {true,false} default: true\n");
297-
reportf(" -xor-store-exp = <num> [ 3 - N ] default: 0\n");
285+
reportf(" -xor-propagation = {eager,lazy} default: %s\n", (s.xor_propagation == Solver::xor_propagation_eager) ? "eager" : "lazy" );
286+
reportf(" -xor-split = <num> [ 1 - N ] default: %d\n", s.xor_split);
287+
reportf(" -xor-lazy-factor = <num> [ 1 - N ] default: %d\n", s.xor_lazy_factor);
288+
reportf(" -xor-rule-priority = {external,internal} default: %s\n", (s.xor_rule_priority == Solver::xor_rule_priority_external) ? "external" : "internal");
289+
reportf(" -xor-store-clauses = {true,false} default: %s\n", s.xor_store_clauses ? "true" : "false");
290+
reportf(" -xor-exp-length = <num> [ 3 - N ] default: %d\n", s.xor_exp_length);
291+
reportf(" -xor-bump-activity = {0,1,2} default: %d\n", s.xor_bump_activity);
292+
reportf(" -xor-even-elim = {true,false} default: %s\n", s.xor_even_elim ? "true" : "false");
293+
reportf(" -xor-up-xors = {true,false} default: %s\n", (s.xor_up_xors) ? "true" : "false");
294+
reportf(" -xor-up-cache-exp = {true,false} default: %s\n", s.xor_up_cache_exp ? "true" : "false");
295+
reportf(" -xor-split-cycle-components = {true,false} default: %s\n", s.xor_split_cycle_components ? "true" : "false");
296+
reportf(" -xor-create-vars = {true,false} default: %s\n", s.xor_create_vars ? "true" : "false");
297+
reportf(" -xor-to-cnf = {true,false} default: %s\n", s.xor_to_cnf ? "true" : "false");
298+
reportf(" -xor-deep-cuts = {true,false} default: %s\n", s.xor_deep_cuts ? "true" : "false");
299+
reportf(" -xor-store-exp = <num> [ 3 - N ] default: %d\n", s.xor_store_exp);
298300
reportf(" -log-conflicts = <PATH> default: off\n");
299301
reportf(" -decay = <num> [ 0 - 1 ]\n");
300302
reportf(" -rnd-freq = <num> [ 0 - 1 ]\n");

‎up-minisat/minisat/core/Main.C

+17-17
Original file line numberDiff line numberDiff line change
@@ -233,8 +233,8 @@ void printStats(Solver& solver, StopWatch& totalTime)
233233
reportf("UP-xor explained : %-12lld\n", up.stats.explained);
234234
reportf("UP-xor deep cuts : %-12lld\n", up.stats.deepCuts);
235235
reportf("UP-xor cached exp. : %-12lld\n", up.stats.cachedExplained);
236-
reportf("total time : %-12lld\n", totalTime.total());
237-
reportf("xor time : %-12lld\n", solver.xorTime.total());
236+
reportf("total time : %-12g\n", ((double) totalTime.total()) / ((double) 1000000000.0) );
237+
reportf("xor time : %-12g\n", ((double) solver.xorTime.total()) / ((double) 1000000000.0));
238238

239239
if (up.stats.explained) {
240240
reportf("UP-xor exp. length : %.2f\n", (float) up.stats.explanationLits / up.stats.explained);
@@ -274,24 +274,24 @@ static void SIGINT_handler(int signum) {
274274

275275
void printUsage(char** argv)
276276
{
277+
Solver S;
277278
reportf("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n\n", argv[0]);
278279
reportf("OPTIONS:\n\n");
279280
reportf(" -polarity-mode = {true,false,rnd} default: false\n");
280-
reportf(" -xor-propagation = {eager,lazy} default: eager\n");
281-
reportf(" -xor-lazy-factor = <num> [ 1 - N ] default: 2\n");
282-
reportf(" -xor-rule-priority = {external,internal} default: external\n");
283-
// reportf(" -xor-internal-vars = {on,off} default: off\n");
284-
reportf(" -xor-store-clauses = {true,false} default: false\n");
285-
reportf(" -xor-exp-length = <num> [ 3 - N ] default: 3\n");
286-
reportf(" -xor-bump-activity = {0,1,2} default: 0\n");
287-
reportf(" -xor-even-elim = {true,false} default: false\n");
288-
reportf(" -xor-create-vars = {true,false} default: false\n");
289-
reportf(" -xor-to-cnf = {true,false} default: true\n");
290-
reportf(" -xor-deep-cuts = <num> [ 0 - N ] default: 100000\n");
291-
reportf(" -xor-1uip-cuts = {true,false} default: false\n");
292-
reportf(" -xor-store-exp = <num> [ 3 - N ] default: 0\n");
293-
reportf(" -xor-tree-exp = {true,false} default: true\n");
294-
reportf(" -xor-learn-all = {true,false} default: false\n");
281+
reportf(" -xor-propagation = {eager,lazy} default: %s\n", (S.xor_propagation == Solver::xor_propagation_eager) ? "eager" : "lazy");
282+
reportf(" -xor-lazy-factor = <num> [ 1 - N ] default: %d\n", S.xor_lazy_factor);
283+
reportf(" -xor-rule-priority = {external,internal} default: %s\n", (S.xor_rule_priority == Solver::xor_rule_priority_internal) ? "internal" : "external" );
284+
reportf(" -xor-store-clauses = {true,false} default: %s\n", (S.xor_store_clauses) ? "true" : "false");
285+
reportf(" -xor-exp-length = <num> [ 3 - N ] default: %d\n", S.xor_exp_length);
286+
reportf(" -xor-bump-activity = {0,1,2} default: %d\n", S.xor_bump_activity);
287+
reportf(" -xor-even-elim = {true,false} default: %s\n", S.xor_even_elim ? "true" : "false");
288+
reportf(" -xor-create-vars = {true,false} default: %s\n", S.xor_create_vars ? "true" : "false");
289+
reportf(" -xor-to-cnf = {true,false} default: %s\n", S.xor_to_cnf ? "true" : "false");
290+
reportf(" -xor-deep-cuts = {true,false}] default: %s\n", S.xor_deep_cuts ? "true" : "false");
291+
reportf(" -xor-1uip-cuts = {true,false} default: %s\n", S.xor_1uip_cuts ? "true" : "false");
292+
reportf(" -xor-store-exp = <num> [ 3 - N ] default: %d\n", S.xor_store_exp);
293+
reportf(" -xor-tree-exp = {true,false} default: %s\n", S.xor_tree_exp ? "true" : "false");
294+
reportf(" -xor-learn-all = {true,false} default: %s\n", S.xor_learn_all ? "true" : "false");
295295
reportf(" -log-conflicts = <PATH> default: off\n");
296296
reportf(" -decay = <num> [ 0 - 1 ]\n");
297297
reportf(" -rnd-freq = <num> [ 0 - 1 ]\n");

0 commit comments

Comments
 (0)