1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
* parm_parm_dependency(p->max_minutes, p->max_seconds, 60, TRUE);
* parm_parm_dependency(p->max_hours, p->max_seconds, 3600, TRUE);
* parm_parm_dependency(p->max_days, p->max_seconds, 86400, TRUE);
flag_flag_dependency(p->paramodulation, TRUE, p->back_demod, TRUE);
back demod default on, get rid of dependency DONE
* flag_parm_dependency(p->para_units_only, TRUE, p->para_lit_limit, 1);
flag_flag_dependency(p->back_unit_deletion, TRUE, p->unit_deletion, TRUE);
only one flag: unit_deletion. No dependency DONE
* flag_flag_dependency(p->hyper_resolution, TRUE, p->pos_hyper_resolution, TRUE);
* flag_flag_dependency(p->hyper_resolution, FALSE, p->pos_hyper_resolution, FALSE);
* flag_flag_dependency(p->ur_resolution, TRUE, p->pos_ur_resolution, TRUE);
* flag_flag_dependency(p->ur_resolution, TRUE, p->neg_ur_resolution, TRUE);
* flag_flag_dependency(p->ur_resolution, FALSE, p->pos_ur_resolution, FALSE);
* flag_flag_dependency(p->ur_resolution, FALSE, p->neg_ur_resolution, FALSE);
flag_stringparm_dependency(p->positive_inference, TRUE, p->literal_selection, "max_negative");
eliminate flag positive_inference
* flag_parm_dependency(p->lex_dep_demod, FALSE, p->lex_dep_demod_lim, 0);
* flag_parm_dependency(p->lex_dep_demod, TRUE, p->lex_dep_demod_lim, -1);
* flag_parm_dependency(p->lightest_first, TRUE, p->weight_part, 1);
* flag_parm_dependency(p->lightest_first, TRUE, p->age_part, 0);
* flag_parm_dependency(p->lightest_first, TRUE, p->false_part, 0);
* flag_parm_dependency(p->lightest_first, TRUE, p->true_part, 0);
* flag_parm_dependency(p->lightest_first, TRUE, p->random_part, 0);
* flag_parm_dependency(p->random_given, TRUE, p->weight_part, 0);
* flag_parm_dependency(p->random_given, TRUE, p->age_part, 0);
* flag_parm_dependency(p->random_given, TRUE, p->false_part, 0);
* flag_parm_dependency(p->random_given, TRUE, p->true_part, 0);
* flag_parm_dependency(p->random_given, TRUE, p->random_part, 1);
* parm_parm_dependency(p->pick_given_ratio, p->age_part, 1, FALSE);
* parm_parm_dependency(p->pick_given_ratio, p->weight_part, 1, TRUE);
* parm_parm_dependency(p->pick_given_ratio, p->false_part, 0, FALSE);
* parm_parm_dependency(p->pick_given_ratio, p->true_part, 0, FALSE);
* parm_parm_dependency(p->pick_given_ratio, p->random_part, 0, FALSE);
* flag_parm_dependency(p->breadth_first, TRUE, p->age_part, 1);
* flag_parm_dependency(p->breadth_first, TRUE, p->weight_part, 0);
* flag_parm_dependency(p->breadth_first, TRUE, p->false_part, 0);
* flag_parm_dependency(p->breadth_first, TRUE, p->true_part, 0);
* flag_parm_dependency(p->breadth_first, TRUE, p->random_part, 0);
* flag_parm_dependency(p->default_parts, TRUE, p->hints_part, INT_MAX);
* flag_parm_dependency(p->default_parts, TRUE, p->age_part, 1);
* flag_parm_dependency(p->default_parts, TRUE, p->weight_part, 0);
* flag_parm_dependency(p->default_parts, TRUE, p->false_part, 4);
* flag_parm_dependency(p->default_parts, TRUE, p->true_part, 4);
* flag_parm_dependency(p->default_parts, TRUE, p->random_part, 0);
* flag_parm_dependency(p->default_parts, FALSE, p->hints_part, 0);
* flag_parm_dependency(p->default_parts, FALSE, p->age_part, 0);
* flag_parm_dependency(p->default_parts, FALSE, p->weight_part, 0);
* flag_parm_dependency(p->default_parts, FALSE, p->false_part, 0);
* flag_parm_dependency(p->default_parts, FALSE, p->true_part, 0);
* flag_parm_dependency(p->default_parts, FALSE, p->random_part, 0);
flag_flag_dependency(p->print_gen, TRUE, p->print_kept, TRUE);
flag_flag_dependency(p->print_gen, FALSE, p->print_kept, FALSE);
No dependency. Print KEPT for print_gen. DONE
flag_flag_dependency(p->quiet, TRUE, p->bell, FALSE);
No dependency DONE
* flag_flag_dependency(p->default_output, TRUE, p->quiet, FALSE);
* flag_flag_dependency(p->default_output, TRUE, p->echo_input, TRUE);
* flag_flag_dependency(p->default_output, TRUE, p->print_initial_clauses,TRUE);
* flag_flag_dependency(p->default_output, TRUE, p->print_given, TRUE);
* flag_flag_dependency(p->default_output, TRUE, p->print_proofs, TRUE);
* flag_stringparm_dependency(p->default_output, TRUE, p->stats, "lots");
* flag_flag_dependency(p->default_output, TRUE, p->print_kept, FALSE);
* flag_flag_dependency(p->default_output, TRUE, p->print_gen, FALSE);
* flag_parm_dependency(p->auto_limits, TRUE, p->max_weight, 100);
* flag_parm_dependency(p->auto_limits, TRUE, p->sos_limit, 10000);
* flag_parm_dependency(p->auto_limits, FALSE, p->max_weight, INT_MAX);
* flag_parm_dependency(p->auto_limits, FALSE, p->sos_limit, -1);
flag_flag_dependency(p->auto_inference, TRUE, p->predicate_elim, TRUE);
flag_stringparm_dependency(p->auto_inference, TRUE, p->eq_defs, "unfold");
flag_flag_dependency(p->auto_inference, FALSE, p->predicate_elim, FALSE);
flag_stringparm_dependency(p->auto_inference, FALSE, p->eq_defs, "pass");
make these dependences of new auto_setup DONE
* flag_flag_dependency(p->automatic, TRUE, p->auto_inference, TRUE);
* flag_flag_dependency(p->automatic, TRUE, p->auto_limits, TRUE);
* flag_flag_dependency(p->automatic, TRUE, p->auto_denials, TRUE);
* flag_flag_dependency(p->automatic, TRUE, p->auto_process, TRUE);
* flag_flag_dependency(p->automatic, FALSE, p->auto_inference, FALSE);
* flag_flag_dependency(p->automatic, FALSE, p->auto_limits, FALSE);
* flag_flag_dependency(p->automatic, FALSE, p->auto_denials, FALSE);
* flag_flag_dependency(p->automatic, FALSE, p->auto_process, FALSE);
* flag_flag_dependency(p->auto2, TRUE, p->automatic, TRUE);
* flag_parm_dependency(p->auto2, TRUE, p->new_constants, 1);
* flag_parm_dependency(p->auto2, TRUE, p->fold_denial_max, 3);
* flag_parm_dependency(p->auto2, TRUE, p->max_weight, 200);
* flag_parm_dependency(p->auto2, TRUE, p->nest_penalty, 1);
* flag_parm_dependency(p->auto2, TRUE, p->skolem_penalty, 3);
* flag_parm_dependency(p->auto2, TRUE, p->sk_constant_weight, 0);
* flag_parm_dependency(p->auto2, TRUE, p->prop_atom_weight, 5);
* flag_flag_dependency(p->auto2, TRUE, p->sort_initial_sos, TRUE);
* flag_parm_dependency(p->auto2, TRUE, p->sos_limit, -1);
* flag_parm_dependency(p->auto2, TRUE, p->lrs_ticks, 3000);
* flag_parm_dependency(p->auto2, TRUE, p->max_megs, 400);
* flag_stringparm_dependency(p->auto2, TRUE, p->stats, "some");
* flag_flag_dependency(p->auto2, TRUE, p->echo_input, FALSE);
* flag_flag_dependency(p->auto2, TRUE, p->quiet, TRUE);
* flag_flag_dependency(p->auto2, TRUE, p->print_initial_clauses, FALSE);
* flag_flag_dependency(p->auto2, TRUE, p->print_given, FALSE);
|
