1.
|
1. 关于APP界面的使用
（1）运行arc==2,且arg[2]为指定参数（非.cnf文件），例如使用参数'-h' $ ./cadical.exe -h usage: cadical [ <option> ... ] [ <input> [ <proof> ] ] where '<option>' is one of the following common options: -h print this short list of common options -n do not print witness -t <sec> set wall clock time limit The input is read from '<input>' assumed to be in DIMACS format.
(2) 运行cadical.exe 后跟两个文件，arg[1]对应cnf文件，arg[2]对应输出的DART proof文件。后跟更多的文件名会报错--需要相应的参数做引导。
如果需要输出运行结果到文件，需要参数引导arg[3]。
至此，了解了增加输出文件切入点。
|
|
2.了解app（Slover）访问Interal数据成员的过程
|
（1）基本的架构 // More precisely the CaDiCaL code is split into three layers:
App类作为程序访问的界面.在cadical.cpp中定义App类型，其重要的数据成员为：Solver *solver; Solver 类型在cadical.hpp中定义，其重要的数据成员为： Internal *internal; // Hidden internal solver. Solver类型的成员函数实现见文件Solver.cpp
//cadical.cpp文件中定义App类型 1 class App : public Handler, public Terminator {
2
3 Solver *solver; // Global solver.
4
5 int force_strict_parsing;
6
7 bool force_writing;
8 static bool most_likely_existing_cnf_file (const char *path);
9
10 // Internal variables.
11 int max_var; // Set after parsing.
12 volatile bool timesup; // Asynchronous termination.
13
14 // Printing.
15 void print_usage (bool all = false);
16 void print_witness (FILE *);
17
18 // Option handling.
19 bool set (const char *);
20 bool set (const char *, int);
21 int get (const char *);
22 bool verbose () { return get ("verbose") && !get ("quiet"); }
23
24 /*-----------------------------------------------------------------*/
25
26 // The actual initialization.
27 void init ();
28
29 // Terminator interface.
30 bool terminate () { return timesup; }
31
32 // Handler interface.
33 void catch_signal (int sig);
34 void catch_alarm ();
35
36 public:
37 App ();
38 ~App ();
39
40 // Parse the arguments and run the solver.
41 int main (int arg, char **argv);
42 };
//cadical.hpp文件中定义了Solver类型 1 class Solver {
2
3 public:
4
5 Solver ();
6 ~Solver ();
7
8 static const char *signature (); // name of this library
9
10 void add (int lit);
11
12 void clause (int); // Add unit clause.
13 void clause (int, int); // Add binary clause.
14 void clause (int, int, int); // Add ternary clause.
15 void clause (int, int, int, int); // Add quaternary clause.
16 void clause (int, int, int, int, int); // Add quinternary clause.
17 void clause (const std::vector<int> &); // Add literal vector as clause.
18 void clause (const int *, size_t); // Add literal array as clause.
19
20
21 bool inconsistent ();
22
23 void assume (int lit);
24
25 int solve ();
26
27 int val (int lit);
28
29 bool flip (int lit);
30
31 bool flippable (int lit);
32
33 bool failed (int lit);
34
35 void connect_terminator (Terminator *terminator);
36 void disconnect_terminator ();
37
38 void connect_learner (Learner *learner);
39 void disconnect_learner ();
40
41
42 void connect_external_propagator (ExternalPropagator *propagator);
43 void disconnect_external_propagator ();
44
45 void add_observed_var (int var);
46
47 void remove_observed_var (int var);
48
49 void reset_observed_vars ();
50
51 bool is_decision (int lit);
52
53
54 void constrain (int lit);
55 bool constraint_failed ();
56
57 int lookahead (void);
58
59 struct CubesWithStatus {
60 int status;
61 std::vector<std::vector<int>> cubes;
62 };
63
64 CubesWithStatus generate_cubes (int, int min_depth = 0);
65
66 void reset_assumptions ();
67 void reset_constraint ();
68
69 const State &state () const { return _state; }
70
71
72 int status () const {
73 if (_state == SATISFIED)
74 return 10;
75 else if (_state == UNSATISFIED)
76 return 20;
77 else
78 return 0;
79 }
80
81 static const char *version (); // return version string
82
83 void copy (Solver &other) const;
84
85 int vars ();
86
87 void reserve (int min_max_var);
88
89
90 void trace_api_calls (FILE *file);
91
92 static bool is_preprocessing_option (const char *name);
93
94 static bool is_valid_long_option (const char *arg);
95
96 int get (const char *name);
97
98 void prefix (const char *verbose_message_prefix);
99
100 bool set (const char *name, int val);
101
102 bool set_long_option (const char *arg);
103
104 static bool is_valid_configuration (const char *);
105
106 bool configure (const char *);
107
108 void optimize (int val);
109
110 bool limit (const char *arg, int val);
111 bool is_valid_limit (const char *arg);
112
113 int active () const; // Number of active variables.
114 int64_t redundant () const; // Number of active redundant clauses.
115 int64_t irredundant () const; // Number of active irredundant clauses.
116
117
118 int simplify (int rounds = 3);
119
120 void terminate ();
121
122
123 bool frozen (int lit) const;
124 void freeze (int lit);
125 void melt (int lit); // Also needs 'require (frozen (lit))'.
126
127
128 int fixed (int lit) const;
129
130
131 void phase (int lit);
132 void unphase (int lit);
133
134 bool trace_proof (FILE *file, const char *name); // Write DRAT proof.
135 bool trace_proof (const char *path); // Open & write proof.
136
137
138 void flush_proof_trace (bool print = false);
139
140
141 void close_proof_trace (bool print = false);
142
143 void connect_proof_tracer (Tracer *tracer, bool antecedents);
144 void connect_proof_tracer (InternalTracer *tracer, bool antecedents);
145 void connect_proof_tracer (StatTracer *tracer, bool antecedents);
146 void connect_proof_tracer (FileTracer *tracer, bool antecedents);
147
148
149 void conclude ();
150
151 bool disconnect_proof_tracer (Tracer *tracer);
152 bool disconnect_proof_tracer (StatTracer *tracer);
153 bool disconnect_proof_tracer (FileTracer *tracer);
154
155 void options (); // print current option and value list
156
157
158 bool traverse_clauses (ClauseIterator &) const;
159 bool traverse_witnesses_backward (WitnessIterator &) const;
160 bool traverse_witnesses_forward (WitnessIterator &) const;
161
162
163 const char *read_dimacs (FILE *file, const char *name, int &vars,
164 int strict = 1);
165
166 const char *read_dimacs (const char *path, int &vars, int strict = 1);
167
168
169 const char *read_dimacs (FILE *file, const char *name, int &vars,
170 int strict, bool &incremental,
171 std::vector<int> &cubes);
172
173 const char *read_dimacs (const char *path, int &vars, int strict,
174 bool &incremental, std::vector<int> &cubes);
175
176
177 const char *write_dimacs (const char *path, int min_max_var = 0);
178
179
180 static void build (FILE *file, const char *prefix = "c ");
181
182 private:
183
184 bool adding_clause;
185 bool adding_constraint;
186
187 State _state; // API states as discussed above.
188
189
190 Internal *internal; // Hidden internal solver.
191 External *external; // Hidden API to internal solver mapping.
192
193
194
195 bool close_trace_api_file; // Close file if owned by solver it.
196 FILE *trace_api_file; // Also acts as flag that we are tracing.
197
198 static bool tracing_api_through_environment;
199
200
201 void trace_api_call (const char *) const;
202 void trace_api_call (const char *, int) const;
203 void trace_api_call (const char *, const char *) const;
204 void trace_api_call (const char *, const char *, int) const;
205
206
207 void transition_to_steady_state ();
208
209
210 friend class App;
211 friend class Mobical;
212 friend class Parser;
213
214 const char *read_solution (const char *path);
215
216
217 void section (const char *); // print section header
218 void message (const char *, ...) // ordinary message
219 CADICAL_ATTRIBUTE_FORMAT (2, 3);
220
221 void message (); // empty line - only prefix
222 void error (const char *, ...) // produce error message
223 CADICAL_ATTRIBUTE_FORMAT (2, 3);
224
225
226 void verbose (int level, const char *, ...)
227 CADICAL_ATTRIBUTE_FORMAT (3, 4);
228
229 const char *read_dimacs (File *, int &, int strict, bool *incremental = 0,
230 std::vector<int> * = 0);
231
232 int call_external_solve_and_check_results (bool preprocess_only);
233
234
235 void dump_cnf ();
236 friend struct DumpCall; // Mobical calls 'dump_cnf' in 'DumpCall::execute'
237
238
239 ExternalPropagator *get_propagator ();
240 bool observed (int lit);
241 bool is_witness (int lit);
242
243 friend struct LemmaCall;
244 friend struct ObserveCall;
245 friend struct DisconnectCall;
246 friend class MockPropagator;
247 };
|
|
|
（2）APP中调用函数输出结果到外部文件 1 int App::main (int argc, char **argv) {
2
3 ......
4 .......
5
6 // Now initialize solver.
7 init ();
8
9 const char *read_solution_path = 0, *write_result_path = 0;
10 const char *dimacs_path = 0, *proof_path = 0;
11 ......
12 bool witness = true, less = false;
13 const char *dimacs_name, *err;
14
15 for (int i = 1; i < argc; i++) {
16 .......
17 else if (!strcmp (argv[i], "-w")) {
18 if (++i == argc)
19 APPERR ("argument to '-w' missing");
20 else if (write_result_path)
21 APPERR ("multiple solution file options '-w %s' and '-w %s'",
22 write_result_path, argv[i]);
23 else
24 write_result_path = argv[i];
25 }
26
27 ......
28
29 } else if (set (argv[i])) {
30 /* nothing do be done */
31 } else if (argv[i][0] == '-')
32 APPERR ("invalid option '%s'", argv[i]);
33 else if (proof_specified)
34 APPERR ("too many arguments");
35 else if (dimacs_specified) {
36 proof_path = argv[i];
37 proof_specified = true;
38 if (!force_writing && most_likely_existing_cnf_file (proof_path))
39 APPERR ("DRAT proof file '%s' most likely existing CNF (use '-f')",
40 proof_path);
41 else if (!File::writable (proof_path))
42 APPERR ("DRAT proof file '%s' not writable", proof_path);
43 } else
44 dimacs_specified = true, dimacs_path = argv[i];
45 }
46
47
48 FILE *less_pipe;
49 if (less) {
50 assert (isatty (1));
51 less_pipe = popen ("less -r", "w");
52 if (!less_pipe)
53 APPERR ("could not execute and open pipe to 'less -r' command");
54 dup2 (fileno (less_pipe), 1);
55 } else
56 less_pipe = 0;
57
58 /*---------------------------------------------------------------*/
59
60 if (read_solution_path && !get ("check"))
61 set ("--check");
62 #ifndef QUIET
63 if (!get ("quiet")) {
64 solver->section ("banner");
65 solver->message ("%sCaDiCaL SAT Solver%s", tout.bright_magenta_code (),
66 tout.normal_code ());
67 solver->message ("%s%s%s", tout.bright_magenta_code (), copyright (),
68 tout.normal_code ());
69 solver->message ();
70 CaDiCaL::Solver::build (stdout, "c ");
71 }
72 #endif
73 if (preprocessing > 0 || localsearch > 0 ||
74 #ifndef __WIN32
75 time_limit >= 0 ||
76 #endif
77 conflict_limit >= 0 || decision_limit >= 0) {
78 solver->section ("limit");
79 if (preprocessing > 0) {
80 solver->message (
81 "enabling %d initial rounds of preprocessing (due to '%s')",
82 preprocessing, preprocessing_specified);
83 solver->limit ("preprocessing", preprocessing);
84 }
85 if (localsearch > 0) {
86 solver->message (
87 "enabling %d initial rounds of local search (due to '%s')",
88 localsearch, localsearch_specified);
89 solver->limit ("localsearch", localsearch);
90 }
91 #ifndef __WIN32
92 if (time_limit >= 0) {
93 solver->message (
94 "setting time limit to %d seconds real time (due to '-t %s')",
95 time_limit, time_limit_specified);
96 Signal::alarm (time_limit);
97 solver->connect_terminator (this);
98 }
99 #endif
100 if (conflict_limit >= 0) {
101 solver->message (
102 "setting conflict limit to %d conflicts (due to '%s')",
103 conflict_limit, conflict_limit_specified);
104 bool succeeded = solver->limit ("conflicts", conflict_limit);
105 assert (succeeded), (void) succeeded;
106 }
107 if (decision_limit >= 0) {
108 solver->message (
109 "setting decision limit to %d decisions (due to '%s')",
110 decision_limit, decision_limit_specified);
111 bool succeeded = solver->limit ("decisions", decision_limit);
112 assert (succeeded), (void) succeeded;
113 }
114 }
115 if (verbose () || proof_specified)
116 solver->section ("proof tracing");
117 if (proof_specified) {
118 if (!proof_path) {
119 const bool force_binary = (isatty (1) && get ("binary"));
120 if (force_binary)
121 set ("--no-binary");
122 solver->message ("writing %s proof trace to %s'<stdout>'%s",
123 (get ("binary") ? "binary" : "non-binary"),
124 tout.green_code (), tout.normal_code ());
125 if (force_binary)
126 solver->message (
127 "connected to terminal thus non-binary proof forced");
128 solver->trace_proof (stdout, "<stdout>");
129 } else if (!solver->trace_proof (proof_path))
130 APPERR ("can not open and write proof trace to '%s'", proof_path);
131 else
132 solver->message ("writing %s proof trace to %s'%s'%s",
133 (get ("binary") ? "binary" : "non-binary"),
134 tout.green_code (), proof_path, tout.normal_code ());
135 } else
136 solver->verbose (1, "will not generate nor write DRAT proof");
137 solver->section ("parsing input");
138 dimacs_name = dimacs_path ? dimacs_path : "<stdin>";
139 string help;
140 if (!dimacs_path) {
141 help += " ";
142 help += tout.magenta_code ();
143 help += "(use '-h' for a list of common options)";
144 help += tout.normal_code ();
145 }
146 solver->message ("reading DIMACS file from %s'%s'%s%s",
147 tout.green_code (), dimacs_name, tout.normal_code (),
148 help.c_str ());
149 bool incremental;
150 vector<int> cube_literals;
151 if (dimacs_path)
152 err = solver->read_dimacs (dimacs_path, max_var, force_strict_parsing,
153 incremental, cube_literals);
154 else
155 err = solver->read_dimacs (stdin, dimacs_name, max_var,
156 force_strict_parsing, incremental,
157 cube_literals);
158 if (err)
159 APPERR ("%s", err);
160 if (read_solution_path) {
161 solver->section ("parsing solution");
162 solver->message ("reading solution file from '%s'", read_solution_path);
163 if ((err = solver->read_solution (read_solution_path)))
164 APPERR ("%s", err);
165 }
166
167 solver->section ("options");
168 if (optimize > 0) {
169 solver->optimize (optimize);
170 solver->message ();
171 }
172 solver->options ();
173
174 int res = 0;
175 .......
176 .......
177
178
179 res = solver->solve ();
180 #ifndef QUIET
181 if (!quiet) {
182 time.delta = absolute_process_time () - time.start;
183 time.sum += time.delta;
184 snprintf (buffer, sizeof buffer,
185 "%s"
186 "in %.3f sec "
187 "(%.0f%% after %.2f sec at %.0f ms/cube)"
188 "%s",
189 tout.magenta_code (), time.delta,
190 percent (solved, cubes), time.sum,
191 relative (1e3 * time.sum, solved), tout.normal_code ());
192 if (reporting)
193 solver->message ();
194 const char *cube_str, *status_str, *color_code;
195 if (res == 10) {
196 cube_str = "CUBE";
197 color_code = tout.green_code ();
198 status_str = "SATISFIABLE";
199 } else if (res == 20) {
200 cube_str = "CUBE";
201 color_code = tout.cyan_code ();
202 status_str = "UNSATISFIABLE";
203 } else {
204 cube_str = "cube";
205 color_code = tout.magenta_code ();
206 status_str = "inconclusive";
207 }
208 const char *fmt;
209 if (reporting)
210 fmt = "%s%s %zu %s%s %s";
211 else
212 fmt = "%s%s %zu %-13s%s %s";
213 solver->message (fmt, color_code, cube_str, solved, status_str,
214 tout.normal_code (), buffer);
215 }
216 #endif
217 if (res == 10) {
218 satisfiable++;
219 solver->conclude ();
220 break;
221 } else if (res == 20) {
222 unsatisfiable++;
223 solver->conclude ();
224 for (auto other : cube)
225 if (solver->failed (other))
226 failed.push_back (other);
227 for (auto other : failed)
228 solver->add (-other);
229 solver->add (0);
230 failed.clear ();
231 } else {
232 assert (!res);
233 inconclusive++;
234 if (timesup)
235 break;
236 }
237 cube.clear ();
238 }
239 }
240
241 if (inconclusive && res == 20)
242 res = 0;
243 } else {
244 solver->section ("solving");
245 res = solver->solve ();
246 }
247
248 if (proof_specified) {
249 solver->section ("closing proof");
250 solver->close_proof_trace (!get ("quiet"));
251 }
252
253 if (output_path) {
254 solver->section ("writing output");
255 solver->message ("writing simplified CNF to DIMACS file %s'%s'%s",
256 tout.green_code (), output_path, tout.normal_code ());
257 err = solver->write_dimacs (output_path, max_var);
258 if (err)
259 APPERR ("%s", err);
260 }
261
262 if (extension_path) {
263 solver->section ("writing extension");
264 solver->message ("writing extension stack to %s'%s'%s",
265 tout.green_code (), extension_path,
266 tout.normal_code ());
267 err = solver->write_extension (extension_path);
268 if (err)
269 APPERR ("%s", err);
270 }
271
272 solver->section ("result");
273
274 FILE *write_result_file;
275 write_result_file = stdout;
276 if (write_result_path) {
277 write_result_file = fopen (write_result_path, "w");
278 if (!write_result_file)
279 APPERR ("could not write solution to '%s'", write_result_path);
280 solver->message ("writing result to '%s'", write_result_path);
281 }
282
283 if (res == 10) {
284 fputs ("s {SATISFIABLE}\n", write_result_file);
285 if (witness)
286 print_witness (write_result_file);
287 } else if (res == 20)
288 fputs ("s {UNSATISFIABLE}\n", write_result_file);
289 else
290 fputs ("c UNKNOWN\n", write_result_file);
291 fflush (write_result_file);
292 if (write_result_path)
293 fclose (write_result_file);
294 solver->statistics ();
295 solver->resources ();
296 solver->section ("shutting down");
297 solver->message ("exit %d", res);
298 if (less_pipe) {
299 close (1);
300 pclose (less_pipe);
301 }
302 ......
303
304 return res;
305 }
1 // Pretty print competition format witness with 'v' lines.
2
3 void App::print_witness (FILE *file) {
4 int c = 0, i = 0, tmp;
5 do {
6 if (!c)
7 fputc ('v', file), c = 1;
8 if (i++ == max_var)
9 tmp = 0;
10 else
11 tmp = solver->val (i) < 0 ? -i : i;
12 char str[32];
13 snprintf (str, sizeof str, " %d", tmp);
14 int l = strlen (str);
15 if (c + l > 78)
16 fputs ("\nv", file), c = 1;
17 fputs (str, file);
18 c += l;
19 } while (tmp);
20 if (c)
21 fputc ('\n', file);
22 }
1 int Solver::val (int lit) {
2 TRACE ("val", lit);
3 REQUIRE_VALID_STATE ();
4 REQUIRE_VALID_LIT (lit);
5 REQUIRE (state () == SATISFIED, "can only get value in satisfied state");
6 if (!external->extended)
7 external->extend ();
8 external->conclude_sat ();
9 int res = external->ival (lit);
10 LOG_API_CALL_RETURNS ("val", lit, res);
11 assert (state () == SATISFIED);
12 assert (res == lit || res == -lit);
13 return res;
14 }
|
|
|
（3）External中调用函数访问内部数据 //external.cpp中定义了External类型，其中重要的数据成员有： Internal *internal; External (Internal *); //构造函数 1 struct External {
2
3 Internal *internal; // The actual internal solver.
4
5 int max_var; // External maximum variable index.
6 size_t vsize; // Allocated external size.
7
8 vector<bool> vals; // Current external (extended) assignment.
9 vector<int> e2i; // External 'idx' to internal 'lit'.
10
11 vector<int> assumptions; // External assumptions.
12 vector<int> constraint; // External constraint. Terminated by zero.
13
14 vector<uint64_t>
15 ext_units; // External units. Needed to compute LRAT for eclause
16 vector<bool> ext_flags; // to avoid duplicate units
17 vector<int> eclause; // External version of original input clause.
18
19 bool extended; // Have been extended.
20 bool concluded;
21 vector<int> extension; // Solution reconstruction extension stack.
22
23 vector<bool> witness; // Literal witness on extension stack.
24 vector<bool> tainted; // Literal tainted in adding literals.
25
26 vector<unsigned> frozentab; // Reference counts for frozen variables.
27
28 'Internal::terminating ()'.
29
30 Terminator *terminator;
31
32 // If there is a learner export learned clauses.
33
34 Learner *learner;
35
36 void export_learned_empty_clause ();
37 void export_learned_unit_clause (int ilit);
38 void export_learned_large_clause (const vector<int> &);
39
40 // If there is an external propagator.
41
42 ExternalPropagator *propagator;
43
44 vector<bool> is_observed; // Quick flag for each external variable
45
46 void add_observed_var (int elit);
47 void remove_observed_var (int elit);
48 void reset_observed_vars ();
49
50 bool observed (int elit);
51 bool is_witness (int elit);
52 bool is_decision (int elit);
53
54 signed char *solution; // Given solution checking for debugging.
55 vector<int> original; // Saved original formula for checking.
56
57
58 vector<bool> moltentab;
59
60 const Range vars; // Provides safe variable iterations.
61
62
63 inline int vidx (int elit) const {
64 assert (elit);
65 assert (elit != INT_MIN);
66 int res = abs (elit);
67 assert (res <= max_var);
68 return res;
69 }
70
71 inline int vlit (int elit) const {
72 assert (elit);
73 assert (elit != INT_MIN);
74 assert (abs (elit) <= max_var);
75 return elit;
76 }
77
78
79 void push_zero_on_extension_stack ();
80
81
82 void push_clause_literal_on_extension_stack (int ilit);
83 void push_witness_literal_on_extension_stack (int ilit);
84
85 void push_clause_on_extension_stack (Clause *);
86 void push_clause_on_extension_stack (Clause *, int witness);
87 void push_binary_clause_on_extension_stack (uint64_t id, int witness,
88 int other);
89
90
91 void extend ();
92 void conclude_sat ();
93
94
95 unsigned elit2ulit (int elit) const {
96 assert (elit);
97 assert (elit != INT_MIN);
98 const int idx = abs (elit) - 1;
99 assert (idx <= max_var);
100 return 2u * idx + (elit < 0);
101 }
102
103 bool marked (const vector<bool> &map, int elit) const {
104 const unsigned ulit = elit2ulit (elit);
105 return ulit < map.size () ? map[ulit] : false;
106 }
107
108 void mark (vector<bool> &map, int elit) {
109 const unsigned ulit = elit2ulit (elit);
110 if (ulit >= map.size ())
111 map.resize (ulit + 1, false);
112 map[ulit] = true;
113 }
114
115 void unmark (vector<bool> &map, int elit) {
116 const unsigned ulit = elit2ulit (elit);
117 if (ulit < map.size ())
118 map[ulit] = false;
119 }
120
121
122 void push_external_clause_and_witness_on_extension_stack (
123 const vector<int> &clause, const vector<int> &witness, uint64_t id);
124
125 void push_id_on_extension_stack (uint64_t id);
126
127 // Restore a clause, which was pushed on the extension stack.
128 void restore_clause (const vector<int>::const_iterator &begin,
129 const vector<int>::const_iterator &end,
130 const uint64_t id);
131
132 void restore_clauses ();
133
134
135 void freeze (int elit);
136 void melt (int elit);
137
138 bool frozen (int elit) {
139 assert (elit);
140 assert (elit != INT_MIN);
141 int eidx = abs (elit);
142 if (eidx > max_var)
143 return false;
144 if (eidx >= (int) frozentab.size ())
145 return false;
146 return frozentab[eidx] > 0;
147 }
148
149
150 External (Internal *);
151 ~External ();
152
153 void enlarge (int new_max_var); // Enlarge allocated 'vsize'.
154 void init (int new_max_var); // Initialize up-to 'new_max_var'.
155
156 int internalize (int); // Translate external to internal literal.
157
158
159 void reset_assumptions ();
160
161 void reset_concluded ();
162
163 void reset_extended ();
164
165 void reset_limits ();
166
167
168 void add (int elit);
169 void assume (int elit);
170 int solve (bool preprocess_only);
171
172
173 inline int ival (int elit) const {
174 assert (elit != INT_MIN);
175 int eidx = abs (elit), res;
176 if (eidx > max_var)
177 res = -eidx;
178 else if ((size_t) eidx >= vals.size ())
179 res = -eidx;
180 else
181 res = vals[eidx] ? eidx : -eidx;
182 if (elit < 0)
183 res = -res;
184 return res;
185 }
186
187 bool flip (int elit);
188 bool flippable (int elit);
189
190 bool failed (int elit);
191
192 void terminate ();
193
194
195 void constrain (int elit);
196
197 bool failed_constraint ();
198
199 void reset_constraint ();
200
201 int lookahead ();
202 CaDiCaL::CubesWithStatus generate_cubes (int, int);
203
204 int fixed (int elit) const; // Implemented in 'internal.hpp'.
205
206
207 void phase (int elit);
208 void unphase (int elit);
209
210
211 bool traverse_all_frozen_units_as_clauses (ClauseIterator &);
212 bool traverse_all_non_frozen_units_as_witnesses (WitnessIterator &);
213 bool traverse_witnesses_backward (WitnessIterator &);
214 bool traverse_witnesses_forward (WitnessIterator &);
215
216 void copy_flags (External &other) const;
217
218 void check_assumptions_satisfied ();
219 void check_constraint_satisfied ();
220 void check_failing ();
221
222 void check_solution_on_learned_clause ();
223 void check_solution_on_shrunken_clause (Clause *);
224 void check_solution_on_learned_unit_clause (int unit);
225 void check_no_solution_after_learning_empty_clause ();
226
227 void check_learned_empty_clause () {
228 if (solution)
229 check_no_solution_after_learning_empty_clause ();
230 }
231
232 void check_learned_unit_clause (int unit) {
233 if (solution)
234 check_solution_on_learned_unit_clause (unit);
235 }
236
237 void check_learned_clause () {
238 if (solution)
239 check_solution_on_learned_clause ();
240 }
241
242 void check_shrunken_clause (Clause *c) {
243 if (solution)
244 check_solution_on_shrunken_clause (c);
245 }
246
247 void check_assignment (int (External::*assignment) (int) const);
248
249 void check_satisfiable ();
250 void check_unsatisfiable ();
251
252 void check_solve_result (int res);
253
254 void update_molten_literals ();
255
256
257 inline int sol (int elit) const {
258 assert (solution);
259 assert (elit != INT_MIN);
260 int eidx = abs (elit);
261 if (eidx > max_var)
262 return 0;
263 int res = solution[eidx];
264 if (elit < 0)
265 res = -res;
266 return res;
267 }
268 };
|
|
标签：char,调用,const,solver,int,void,改写,bool,cadical From： https://www.cnblogs.com/yuweng1689/p/18383236