1 :- module(cdclt_stats, [reset_stats/0,
2 print_stats/0,
3 log_symmetry_breaking_stats/1,
4 log_conflict/0,
5 log_restart/0,
6 log_unique_predicates/1,
7 log_theory_propagation/0,
8 log_set_of_learned_clauses_reduction/0,
9 log_forgotten_clauses/1,
10 log_inferred_implications/1,
11 log_inferred_wd_theory_implications/1,
12 log_boolean_decision/0,
13 log_unit_propagation/0]).
14
15 :- use_module(cdclt_solver('cdclt_settings')).
16 :- use_module(probsrc(module_information), [module_info/2]).
17 :- use_module(probsrc(bsyntaxtree), [conjunction_to_list/2]).
18
19 :- module_info(group, cdclt).
20 :- module_info(description,'This module logs statistics of the CDCL(T) solver if the options is set in the CDCL(T) settings module.').
21
22 :- dynamic symmetry_breaking_predicates/1, conflicts/1, restarts/1, unique_predicates/1, theory_propagations/1, clause_reductions/1, forgotten_clauses/1, inferred_implications/1, inferred_wd_theory_implications/1, boolean_decisions/1, unit_propagations/1.
23
24 %% reset_stats.
25 reset_stats :-
26 retractall(symmetry_breaking_predicates(_)),
27 retractall(conflicts(_)),
28 retractall(restarts(_)),
29 retractall(unique_predicates(_)),
30 retractall(theory_propagations(_)),
31 retractall(clause_reductions(_)),
32 retractall(forgotten_clauses(_)),
33 retractall(inferred_implications(_)),
34 retractall(inferred_wd_theory_implications(_)),
35 retractall(boolean_decisions(_)),
36 retractall(unit_propagations(_)),
37 asserta(symmetry_breaking_predicates(0)),
38 asserta(conflicts(0)),
39 asserta(restarts(0)),
40 asserta(unique_predicates(0)),
41 asserta(theory_propagations(0)),
42 asserta(clause_reductions(0)),
43 asserta(forgotten_clauses(0)),
44 asserta(inferred_implications(0)),
45 asserta(inferred_wd_theory_implications(0)),
46 asserta(boolean_decisions(0)),
47 asserta(unit_propagations(0)).
48
49 %% print_stats.
50 print_stats :-
51 log_stats(true),
52 !,
53 symmetry_breaking_predicates(SBPs),
54 conflicts(Conflicts),
55 restarts(Restarts),
56 unique_predicates(UniquePreds),
57 theory_propagations(TheoryProps),
58 clause_reductions(ClauseReductions),
59 forgotten_clauses(ForgottenClauses),
60 inferred_implications(InferredImpls),
61 inferred_wd_theory_implications(InferredWdTheoryImpls),
62 unit_propagations(UnitPropagations),
63 boolean_decisions(BooleanDecisions),
64 format("----- CDCL(T) Statistics -----~n#Symmetry breaking predicates: ~w~n", [SBPs]),
65 format("#Unique_predicates (SAT variables): ~w~n", [UniquePreds]),
66 format("#Inferred implications: ~w~n", [InferredImpls]),
67 format("#Inferred WD theory implications: ~w~n", [InferredWdTheoryImpls]),
68 format("#Unit propagations: ~w~n", [UnitPropagations]),
69 format("#Boolean decisions: ~w~n", [BooleanDecisions]),
70 format("#Conflicts: ~w~n", [Conflicts]),
71 format("#Restarts: ~w~n", [Restarts]),
72 format("#Theory propagations: ~w~n", [TheoryProps]),
73 format("#Reductions of the set of learned clauses: ~w~n", [ClauseReductions]),
74 format("#Forgotten learned clauses: ~w~n", [ForgottenClauses]).
75 print_stats.
76
77 %% log_symmetry_breaking_stats(+FoundSBPs).
78 % The amount of found symmetry breaking predicates.
79 log_symmetry_breaking_stats(FoundSBPs) :-
80 log_stats(true),
81 !,
82 retract(symmetry_breaking_predicates(_)),
83 asserta(symmetry_breaking_predicates(FoundSBPs)).
84 log_symmetry_breaking_stats(_).
85
86 %% log_conflict.
87 % The amount of conflicts that occurred during CDCL(T).
88 log_conflict :-
89 log_stats(true),
90 !,
91 retract(conflicts(Old)),
92 New is Old + 1,
93 asserta(conflicts(New)).
94 log_conflict.
95
96 %% log_restart.
97 % The amount of (random) restarts that occurred during CDCL(T).
98 log_restart :-
99 log_stats(true),
100 !,
101 retract(restarts(Old)),
102 New is Old + 1,
103 asserta(restarts(New)).
104 log_restart.
105
106 %% log_unique_predicates(+SatVarNames).
107 % The amount of unique predicates of a B formula, i.e., the amount of SAT variables.
108 log_unique_predicates(SatVarNames) :-
109 log_stats(true),
110 !,
111 length(SatVarNames, Amount),
112 retract(unique_predicates(_)),
113 asserta(unique_predicates(Amount)).
114 log_unique_predicates(_).
115
116 %% log_theory_propagation.
117 % The amount of theory propagations that occurred during CDCL(T).
118 log_theory_propagation :-
119 log_stats(true),
120 !,
121 retract(theory_propagations(Old)),
122 New is Old + 1,
123 asserta(theory_propagations(New)).
124 log_theory_propagation.
125
126 %% log_set_of_learned_clauses_reduction.
127 % The amount of clause reductions that occurred during CDCL(T).
128 log_set_of_learned_clauses_reduction :-
129 log_stats(true),
130 !,
131 retract(clause_reductions(Old)),
132 New is Old + 1,
133 asserta(clause_reductions(New)).
134 log_set_of_learned_clauses_reduction.
135
136 %% log_forgotten_clauses(+Amount).
137 % The amount of forgotten clauses during CDCL(T), which is correlated to the amount of clause reductions.
138 log_forgotten_clauses(Amount) :-
139 log_stats(true),
140 !,
141 retract(forgotten_clauses(Old)),
142 New is Old + Amount,
143 asserta(forgotten_clauses(New)).
144 log_forgotten_clauses(_).
145
146 %% log_inferred_implications(+ImplsConj).
147 % The amount of inferred implications as is done in the cdclt_preprocessing:lift_negations_find_impls/5.
148 log_inferred_implications(ImplsConj) :-
149 log_stats(true),
150 ImplsConj \= b(truth,pred,_),
151 !,
152 conjunction_to_list(ImplsConj, Impls),
153 length(Impls, Amount),
154 retract(inferred_implications(_)),
155 asserta(inferred_implications(Amount)).
156 log_inferred_implications(_).
157
158 %% log_inferred_wd_theory_implications(+ImplsConj).
159 % The amount of inferred implications as is done in the cdclt_preprocessing:get_wd_theory_implications/3.
160 log_inferred_wd_theory_implications(ImplsConj) :-
161 log_stats(true),
162 ImplsConj \= b(truth,pred,_),
163 !,
164 conjunction_to_list(ImplsConj, Impls),
165 length(Impls, Amount),
166 retract(inferred_implications(_)),
167 asserta(inferred_implications(Amount)).
168 log_inferred_wd_theory_implications(_).
169
170 %% log_boolean_decision.
171 % The amount of Boolean decisions that occurred during SAT solving.
172 log_boolean_decision :-
173 log_stats(true),
174 !,
175 retract(boolean_decisions(Old)),
176 New is Old + 1,
177 asserta(boolean_decisions(New)).
178 log_boolean_decision.
179
180 %% log_unit_propagation.
181 % The amount of unit propagations that occurred during SAT solving.
182 log_unit_propagation :-
183 log_stats(true),
184 !,
185 retract(unit_propagations(Old)),
186 New is Old + 1,
187 asserta(unit_propagations(New)).
188 log_unit_propagation.