ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
preprocess.h File Reference
#include <stdbool.h>
#include "global.h"
Include dependency graph for preprocess.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

bool kissat_preprocessing (struct kissat *)
 
int kissat_preprocess (struct kissat *)
 

Function Documentation

◆ kissat_preprocess()

int kissat_preprocess ( struct kissat * solver)

Definition at line 31 of file preprocess.c.

31 {
32 KISSAT_assert (kissat_preprocessing (solver));
33 if (!kissat_initially_propagate (solver)) {
34 KISSAT_assert (solver->inconsistent);
35 return 20;
36 }
37 START (preprocess);
38 KISSAT_assert (!solver->preprocessing);
39 solver->preprocessing = true;
40 REPORT (0, '(');
41 const unsigned max_rounds = GET_OPTION (preprocessrounds);
42#ifndef KISSAT_QUIET
43 const unsigned variables_initially = solver->active;
44 const uint64_t clauses_initially = BINIRR_CLAUSES;
45 const unsigned variables_originally = SIZE_STACK (solver->import);
46 const uint64_t clauses_originally = solver->statistics.clauses_original;
47 kissat_verbose (solver,
48 "[preprocess] running at most %u preprocesing rounds",
49 max_rounds);
50 kissat_verbose (
51 solver,
52 "[preprocess] initially %u variables %.0f%% and %" PRIu64
53 " clauses %.0f%%",
54 variables_initially,
55 kissat_percent (variables_initially, variables_originally),
56 clauses_initially,
57 kissat_percent (clauses_initially, clauses_originally));
58#endif
59 kissat_initial_sparse_collect (solver);
60 unsigned round = 1;
61 for (;;) {
62 if (solver->inconsistent)
63 break;
64 if (TERMINATED (preprocess_terminated_1))
65 break;
66 const unsigned variables_before = solver->active;
67 const uint64_t clauses_before = BINIRR_CLAUSES;
68#ifndef KISSAT_QUIET
69 kissat_verbose (solver,
70 "[preprocess-%u] started preprocessing round %u", round,
71 round);
72#endif
73 if (GET_OPTION (preprocessprobe))
74 kissat_probe_initially (solver);
75 if (GET_OPTION (fastel))
76 kissat_fast_variable_elimination (solver);
77 const unsigned variables_after = solver->active;
78 const uint64_t clauses_after = BINIRR_CLAUSES;
79#ifndef KISSAT_QUIET
80 if (variables_after < variables_before) {
81 unsigned removed = variables_before - variables_after;
82 kissat_verbose (
83 solver, "[preprocess-%u] removed %u variables %.0f%% in round %u",
84 round, removed, kissat_percent (removed, variables_before),
85 round);
86 } else if (variables_after > variables_before) {
87 unsigned added = variables_after - variables_before;
88 kissat_verbose (
89 solver, "[preprocess-%u] added %u variables %.0f%% in round %u",
90 round, added, kissat_percent (added, variables_before), round);
91 } else
92 kissat_verbose (
93 solver,
94 "[preprocess-%u] number variables %u unchanged in round %u",
95 round, variables_before, round);
96 if (clauses_after < clauses_before) {
97 uint64_t removed = clauses_before - clauses_after;
98 kissat_verbose (solver,
99 "[preprocess-%u] removed %" PRIu64
100 " irredundant and binary clauses %.0f%% in round %u",
101 round, removed,
102 kissat_percent (removed, clauses_before), round);
103 } else if (clauses_after > clauses_before) {
104 uint64_t added = clauses_after - clauses_before;
105 kissat_verbose (solver,
106 "[preprocess-%u] added %" PRIu64
107 " irredundant and binary clauses %.0f%% in round %u",
108 round, added, kissat_percent (added, clauses_before),
109 round);
110 } else
111 kissat_verbose (
112 solver,
113 "[preprocess-%u] number irredundant and binary clauses %" PRIu64
114 " unchanged in round %u",
115 round, clauses_before, round);
116#endif
117 if (round == max_rounds)
118 break;
119 if (variables_before == variables_after &&
120 clauses_before == clauses_after)
121 break;
122 round++;
123 }
124#ifndef KISSAT_QUIET
125 const unsigned variables_finally = solver->active;
126 const uint64_t clauses_finally = BINIRR_CLAUSES;
127 kissat_verbose (solver, "[preprocess] finished after %u rounds", round);
128 if (variables_finally < variables_initially) {
129 unsigned removed = variables_initially - variables_finally;
130 kissat_verbose (
131 solver,
132 "[preprocess] removed %u variables %.0f%% (%u remain %.0f%%)",
133 removed, kissat_percent (removed, variables_initially),
134 variables_finally,
135 kissat_percent (variables_finally, variables_originally));
136 } else if (variables_finally > variables_initially) {
137 unsigned added = variables_finally - variables_initially;
138 kissat_verbose (
139 solver, "[preprocess] added %u variables %.0f%% (%u remain %.0f%%)",
140 added, kissat_percent (added, variables_initially),
141 variables_finally,
142 kissat_percent (variables_finally, variables_originally));
143 } else
144 kissat_verbose (
145 solver,
146 "[preprocess] number variables %u unchanged (%u remain %.0f%%)",
147 variables_initially, variables_finally,
148 kissat_percent (variables_finally, variables_originally));
149 if (clauses_finally < clauses_initially) {
150 uint64_t removed = clauses_initially - clauses_finally;
151 kissat_verbose (solver,
152 "[preprocess] removed %" PRIu64
153 " irredundant and binary clauses %.0f%% (%" PRIu64
154 " remain %.0f%%)",
155 removed, kissat_percent (removed, clauses_initially),
156 clauses_finally,
157 kissat_percent (clauses_finally, clauses_originally));
158 } else if (clauses_finally > clauses_initially) {
159 uint64_t added = clauses_finally - clauses_initially;
160 kissat_verbose (solver,
161 "[preprocess] added %" PRIu64
162 " irredundant and binary clauses %.0f%% (%" PRIu64
163 " remain %.0f%%)",
164 added, kissat_percent (added, clauses_initially),
165 clauses_finally,
166 kissat_percent (clauses_finally, clauses_originally));
167 } else
168 kissat_verbose (
169 solver,
170 "[preprocess] number irredundant and binary clauses %" PRIu64
171 " unchanged (%" PRIu64 " remain %.0f%%)",
172 clauses_initially, clauses_finally,
173 kissat_percent (clauses_finally, clauses_originally));
174#endif
175 REPORT (0, ')');
176 KISSAT_assert (solver->preprocessing);
177 solver->preprocessing = false;
178 STOP (preprocess);
179 return solver->inconsistent ? 20 : 0;
180}
SIZE_STACK
#define SIZE_STACK(S)
Definition stack.h:19
kissat_initial_sparse_collect
void kissat_initial_sparse_collect(kissat *solver)
Definition collect.c:647
kissat_fast_variable_elimination
void kissat_fast_variable_elimination(struct kissat *)
KISSAT_assert
#define KISSAT_assert(ignore)
Definition global.h:13
solver
#define solver
Definition kitten.c:211
GET_OPTION
#define GET_OPTION(N)
Definition options.h:295
kissat_preprocessing
ABC_NAMESPACE_IMPL_START bool kissat_preprocessing(struct kissat *solver)
Definition preprocess.c:16
kissat_verbose
#define kissat_verbose(...)
Definition print.h:51
kissat_probe_initially
int kissat_probe_initially(kissat *solver)
Definition probe.c:94
STOP
#define STOP(P)
Definition profile.hpp:158
START
#define START(P)
Definition profile.hpp:150
kissat_initially_propagate
bool kissat_initially_propagate(kissat *solver)
Definition propinitially.c:36
REPORT
#define REPORT(...)
Definition report.h:10
BINIRR_CLAUSES
#define BINIRR_CLAUSES
Definition statistics.h:341
TERMINATED
#define TERMINATED(BIT)
Definition terminate.h:42
preprocess_terminated_1
#define preprocess_terminated_1
Definition terminate.h:67
Here is the call graph for this function:
Here is the caller graph for this function:

◆ kissat_preprocessing()

bool kissat_preprocessing ( struct kissat * solver)

Definition at line 16 of file preprocess.c.

16 {
17 KISSAT_assert (!solver->level);
18 KISSAT_assert (!solver->inconsistent);
19 if (!GET_OPTION (preprocess))
20 return false;
21 if (!GET_OPTION (probe))
22 return false;
23 if (!GET_OPTION (preprocessprobe))
24 return false;
25#if defined(KISSAT_NDEBUG) && defined(KISSAT_NOPTIONS)
26 (void) solver;
27#endif
28 return true;
29}
Here is the caller graph for this function: