cadical_sys/bridge.rs
1#[cxx::bridge]
2pub mod ffi {
3 unsafe extern "C++" {
4 include!("cadical-sys/src/cadical_bridge.hpp");
5
6 type Solver;
7
8 /// The SAT competition standardized the exit code of SAT solvers to the
9 /// following which then is also used return code for 'solve' functions.
10 /// In the following example we use those constants for brevity though.
11 type Status;
12
13 /// Solver State
14 type State;
15 type ClauseIterator;
16 type WitnessIterator;
17 type Terminator;
18 type Learner;
19 type FixedAssignmentListener;
20 type ExternalPropagator;
21 type Tracer;
22 type InternalTracer;
23 type StatTracer;
24 type FileTracer;
25
26 /// Constructor and basic operations
27 #[must_use]
28 pub fn constructor() -> UniquePtr<Solver>;
29
30 #[must_use]
31 pub fn signature() -> String;
32
33 /// Core functionality as in the IPASIR incremental SAT solver interface.
34 /// (recall 'READY = CONFIGURING | STEADY | SATISFIED | UNSATISFIED').
35 /// Further note that 'lit' is required to be different from 'INT_MIN' and
36 /// different from '0' except for 'add'.
37 ///
38 /// Add valid literal to clause or zero to terminate clause.
39 ///
40 /// require (VALID) // recall 'VALID = READY | ADDING'
41 /// if (lit) ensure (ADDING) // and thus VALID but not READY
42 /// if (!lit) ensure (STEADY ) // and thus READY
43 ///
44 pub fn add(solver: &mut UniquePtr<Solver>, literal: i32);
45
46 /// Here are functions simplifying clause addition. The given literals
47 /// should all be valid (different from 'INT_MIN' and different from '0').
48 ///
49 /// require (VALID)
50 /// ensure (STEADY )
51 ///
52 pub fn clause1(solver: &mut UniquePtr<Solver>, l1: i32);
53 pub fn clause2(solver: &mut UniquePtr<Solver>, l1: i32, l2: i32);
54 pub fn clause3(solver: &mut UniquePtr<Solver>, l1: i32, l2: i32, l3: i32);
55 pub fn clause4(solver: &mut UniquePtr<Solver>, l1: i32, l2: i32, l3: i32, l4: i32);
56 pub fn clause5(solver: &mut UniquePtr<Solver>, l1: i32, l2: i32, l3: i32, l4: i32, l5: i32);
57 pub fn clause6(solver: &mut UniquePtr<Solver>, v: &[i32]);
58
59 /// Function that makes clause from any slice of integers.
60 ///
61 /// # Safety
62 ///
63 /// This function must be called with a valid pointer to a slice of integers.
64 #[allow(clippy::missing_safety_doc)]
65 pub unsafe fn clause7(solver: &mut UniquePtr<Solver>, ptr: *const i32, n: usize);
66
67 /// This function can be used to check if the formula is already
68 /// inconsistent (contains the empty clause or was proven to be
69 /// root-level unsatisfiable).
70 pub fn inconsistent(solver: &mut UniquePtr<Solver>) -> bool;
71
72 /// Assume valid non zero literal for next call to 'solve'. These
73 /// assumptions are reset after the call to 'solve' as well as after
74 /// returning from 'simplify' and 'lookahead.
75 ///
76 /// require (READY)
77 /// ensure (STEADY )
78 ///
79 pub fn assume(solver: &mut UniquePtr<Solver>, lit: i32);
80
81 /// Try to solve the current formula. Returns
82 ///
83 /// 0 = UNKNOWN (limit reached or interrupted through 'terminate')
84 /// 10 = SATISFIABLE
85 /// 20 = UNSATISFIABLE
86 ///
87 /// require (READY)
88 /// ensure (STEADY | SATISFIED | UNSATISFIED)
89 ///
90 /// Note, that while in this call the solver actually transitions to state
91 /// 'SOLVING', which however is only visible from a different context,
92 /// i.e., from a different thread or from a signal handler. Only right
93 /// before returning from this call it goes into a 'READY' state.
94 ///
95 pub fn solve(solver: &mut UniquePtr<Solver>) -> i32;
96
97 /// Get value (-lit=false, lit=true) of valid non-zero literal.
98 ///
99 /// require (SATISFIED)
100 /// ensure (SATISFIED)
101 ///
102 pub fn val(solver: &mut UniquePtr<Solver>, lit: i32) -> i32;
103
104 /// Try to flip the value of the given literal without falsifying the
105 /// formula. Returns 'true' if this was successful. Otherwise the model is
106 /// not changed and 'false' is returned. If a literal was eliminated or
107 /// substituted flipping will fail on that literal and in particular the
108 /// solver will not taint it nor restore any clauses.
109 ///
110 /// The 'flip' function can only flip the value of a variables not acting
111 /// as witness on the reconstruction stack.
112 ///
113 /// As a side effect of calling this function first all assigned variables
114 /// are propagated again without using blocking literal. Thus the first
115 /// call to this function after obtaining a model adds a substantial
116 /// overhead. Subsequent calls will not need to properly propagate again.
117 ///
118 /// Furthermore if the reconstruction stack is non-empty and has been
119 /// traversed to reconstruct a full extended model for eliminated
120 /// variables (and to satisfy removed blocked clauses), the values of these
121 /// witness variables obtained via 'val' before become invalid. The user
122 /// thus will need to call 'val' again after calling 'flip' which will
123 /// trigger then a traversal of the reconstruction stack.
124 ///
125 /// So try to avoid mixing 'flip' and 'val' (for efficiency only).
126 /// Further, this functionality is currently not supported in the presence
127 /// of an external propagator.
128 ///
129 /// require (SATISFIED)
130 /// ensure (SATISFIED)
131 ///
132 pub fn flip(solver: &mut UniquePtr<Solver>, lit: i32) -> bool;
133
134 /// Same as 'flip' without actually flipping it. This functionality is
135 /// currently not supported in the presence of an external propagator.
136 ///
137 /// require (SATISFIED)
138 /// ensure (SATISFIED)
139 ///
140 pub fn flippable(solver: &mut UniquePtr<Solver>, lit: i32) -> bool;
141
142 /// Determine whether the valid non-zero literal is in the core.
143 /// Returns 'true' if the literal is in the core and 'false' otherwise.
144 /// Note that the core does not have to be minimal.
145 ///
146 /// require (UNSATISFIED)
147 /// ensure (UNSATISFIED)
148 ///
149 pub fn failed(solver: &mut UniquePtr<Solver>, lit: i32) -> bool;
150
151 /// Add call-back which is checked regularly for termination. There can
152 /// only be one terminator connected. If a second (non-zero) one is added
153 /// the first one is implicitly disconnected.
154 ///
155 /// require (VALID)
156 /// ensure (VALID)
157 ///
158 pub fn connect_terminator(
159 solver: &mut UniquePtr<Solver>,
160 terminator: &mut UniquePtr<Terminator>,
161 );
162 pub fn disconnect_terminator(solver: &mut UniquePtr<Solver>);
163
164 /// Add call-back which allows to export learned clauses.
165 ///
166 /// require (VALID)
167 /// ensure (VALID)
168 ///
169 pub fn connect_learner(solver: &mut UniquePtr<Solver>, learner: &mut UniquePtr<Learner>);
170 pub fn disconnect_learner(solver: &mut UniquePtr<Solver>);
171
172 /// Add call-back which allows to observe when a variable is fixed.
173 ///
174 /// require (VALID)
175 /// ensure (VALID)
176 ///
177 pub fn connect_fixed_listener(
178 solver: &mut UniquePtr<Solver>,
179 fixed_listener: &mut UniquePtr<FixedAssignmentListener>,
180 );
181 pub fn disconnect_fixed_listener(solver: &mut UniquePtr<Solver>);
182
183 /// Add call-back which allows to learn, propagate and backtrack based on
184 /// external constraints. Only one external propagator can be connected
185 /// and after connection every related variables must be 'observed' (use
186 /// 'add_observed_var' function).
187 /// Disconnection of the external propagator resets all the observed
188 /// variables.
189 ///
190 /// require (VALID)
191 /// ensure (VALID)
192 ///
193 pub fn connect_external_propagator(
194 solver: &mut UniquePtr<Solver>,
195 propagator: &mut UniquePtr<ExternalPropagator>,
196 );
197 pub fn disconnect_external_propagator(solver: &mut UniquePtr<Solver>);
198
199 /// Mark as 'observed' those variables that are relevant to the external
200 /// propagator. External propagation, clause addition during search and
201 /// notifications are all over these observed variabes.
202 /// A variable can not be observed witouth having an external propagator
203 /// connected. Observed variables are "frozen" internally, and so
204 /// inprocessing will not consider them as candidates for elimination.
205 /// An observed variable is allowed to be a fresh variable and it can be
206 /// added also during solving.
207 ///
208 /// require (VALID_OR_SOLVING)
209 /// ensure (VALID_OR_SOLVING)
210 ///
211 pub fn add_observed_var(solver: &mut UniquePtr<Solver>, var: i32);
212
213 /// Removes the 'observed' flag from the given variable. A variable can be
214 /// set unobserved only between solve calls, not during it (to guarantee
215 /// that no yet unexplained external propagation involves it).
216 ///
217 /// require (VALID)
218 /// ensure (VALID)
219 ///
220 pub fn remove_observed_var(solver: &mut UniquePtr<Solver>, var: i32);
221
222 /// Removes all the 'observed' flags from the variables. Disconnecting the
223 /// propagator invokes this step as well.
224 ///
225 /// require (VALID)
226 /// ensure (VALID)
227 ///
228 pub fn reset_observed_vars(solver: &mut UniquePtr<Solver>);
229
230 /// Get reason of valid observed literal (true = it is an observed variable
231 /// and it got assigned by a decision during the CDCL loop. Otherwise:
232 /// false.
233 ///
234 /// require (VALID_OR_SOLVING)
235 /// ensure (VALID_OR_SOLVING)
236 ///
237 pub fn is_decision(solver: &mut UniquePtr<Solver>, lit: i32) -> bool;
238
239 /// Force solve to backtrack to certain decision level. Can be called only
240 /// during 'cb_decide' of a connected External Propagator.
241 /// Invoking in any other time will not have an effect.
242 /// If the call had an effect, the External Propagator will be notified about
243 /// the backtrack via 'notify_backtrack'.
244 ///
245 /// require (SOLVING)
246 /// ensure (SOLVING)
247 ///
248 pub fn force_backtrack(solver: &mut UniquePtr<Solver>, new_level: usize);
249
250 //------------------------------------------------------------------------
251 /// Adds a literal to the constraint clause. Same functionality as 'add'
252 /// but the clause only exists for the next call to solve (same lifetime as
253 /// assumptions). Only one constraint may exists at a time. A new
254 /// constraint replaces the old. The main application of this functonality
255 /// is the model checking algorithm IC3. See our FMCAD'21 paper
256 /// [FroleyksBiere-FMCAD'19] for more details.
257 ///
258 /// Add valid literal to the constraint clause or zero to terminate it.
259 ///
260 /// require (VALID) /// recall 'VALID = READY |
261 /// ADDING' if (lit) ensure (ADDING) /// and thus VALID but not
262 /// READY if (!lit) && !adding_clause ensure (STEADY ) // and thus READY
263 ///
264 pub fn constrain(solver: &mut UniquePtr<Solver>, lit: i32);
265
266 /// Determine whether the constraint was used to proof the
267 /// unsatisfiability. Note that the formula might still be unsatisfiable
268 /// without the constraint.
269 ///
270 /// require (UNSATISFIED)
271 /// ensure (UNSATISFIED)
272 ///
273 pub fn constraint_failed(solver: &mut UniquePtr<Solver>) -> bool;
274
275 //------------------------------------------------------------------------
276 /// This function determines a good splitting literal. The result can be
277 /// zero if the formula is proven to be satisfiable or unsatisfiable. This
278 /// can then be checked by 'state ()'. If the formula is empty and
279 /// the function is not able to determine satisfiability also zero is
280 /// returned but the state remains steady.
281 ///
282 /// require (READY)
283 /// ensure (STEADY |SATISFIED|UNSATISFIED)
284 ///
285 pub fn lookahead(solver: &mut UniquePtr<Solver>) -> i32;
286
287 pub fn generate_cubes(
288 solver: &mut UniquePtr<Solver>,
289 x: i32,
290 min_depth: i32,
291 result_cubes: &mut Vec<i32>,
292 ) -> i32;
293
294 pub fn reset_assumptions(solver: &mut UniquePtr<Solver>);
295
296 pub fn reset_constraint(solver: &mut UniquePtr<Solver>);
297
298 /// Return the current state of the solver as defined above.
299 ///
300 #[must_use]
301 pub fn state(solver: &UniquePtr<Solver>) -> i32;
302
303 /// Similar to 'state ()' but using the staddard competition exit codes of
304 /// '10' for 'SATISFIABLE', '20' for 'UNSATISFIABLE' and '0' otherwise.
305 ///
306 #[must_use]
307 pub fn status(solver: &UniquePtr<Solver>) -> i32;
308
309 /// return version string
310 #[must_use]
311 pub fn version() -> String;
312
313 /*----------------------------------------------------------------------*/
314 /// Copy 'this' into a fresh 'other'. The copy procedure is not a deep
315 /// clone, but only copies irredundant clauses and units. It also makes
316 /// sure that witness reconstruction works with the copy as with the
317 /// original formula such that both solvers have the same models.
318 /// Assumptions are not copied. Options however are copied as well as
319 /// flags which remember the current state of variables in preprocessing.
320 ///
321 /// require (READY) /// for 'this'
322 /// ensure (READY) /// for 'this'
323 ///
324 /// other.require (CONFIGURING)
325 /// other.ensure (CONFIGURING | STEADY )
326 ///
327 pub fn copy(source: &UniquePtr<Solver>, destination: &mut UniquePtr<Solver>);
328
329 /*----------------------------------------------------------------------*/
330 /// Variables are usually added and initialized implicitly whenever a
331 /// literal is used as an argument except for the functions 'val', 'fixed',
332 /// 'failed' and 'frozen'. However, the library internally keeps a maximum
333 /// variable index, which can be queried.
334 ///
335 /// require (VALID | SOLVING)
336 /// ensure (VALID | SOLVING)
337 ///
338 pub fn vars(solver: &mut UniquePtr<Solver>) -> i32;
339
340 /// Increase the maximum variable index explicitly. This function makes
341 /// sure that at least 'min_max_var' variables are initialized. Since it
342 /// might need to reallocate tables, it destroys a satisfying assignment
343 /// and has the same state transition and conditions as 'assume' etc.
344 ///
345 /// require (READY)
346 /// ensure (STEADY )
347 ///
348 pub fn reserve(solver: &mut UniquePtr<Solver>, min_max_var: i32);
349
350 /// pub fn trace_api_calls(solver: &mut UniquePtr<Solver>, file: String);
351
352 //------------------------------------------------------------------------
353 /// Option handling.
354 /// Determine whether 'name' is a valid option name.
355 ///
356 #[must_use]
357 pub fn is_valid_option(name: String) -> bool;
358
359 /// Determine whether 'name' enables a specific preprocessing technique.
360 ///
361 #[must_use]
362 pub fn is_preprocessing_option(name: String) -> bool;
363
364 /// Determine whether 'arg' is a valid long option of the form '--<name>',
365 /// '--<name>=<val>' or '--no-<name>' similar to 'set_long_option' below.
366 /// Legal values are 'true', 'false', or '[-]<mantissa>[e<exponent>]'.
367 #[must_use]
368 pub fn is_valid_long_option(arg: String) -> bool;
369
370 /// Get the current value of the option 'name'. If 'name' is invalid then
371 /// zero is returned. Here '--...' arguments as invalid options.
372 ///
373 pub fn get(solver: &mut UniquePtr<Solver>, name: String) -> i32;
374
375 /// Set the default verbose message prefix (default "c ").
376 ///
377 pub fn prefix(solver: &mut UniquePtr<Solver>, verbose_message_prefix: String);
378
379 /// Explicit version of setting an option. If the option '<name>' exists
380 /// and '<val>' can be parsed then 'true' is returned. If the option value
381 /// is out of range the actual value is computed as the closest (minimum or
382 /// maximum) value possible, but still 'true' is returned.
383 ///
384 /// require (CONFIGURING)
385 /// ensure (CONFIGURING)
386 ///
387 /// Thus options can only bet set right after initialization.
388 ///
389 pub fn set(solver: &mut UniquePtr<Solver>, name: String, val: i32) -> bool;
390
391 /// This function accepts options in command line syntax:
392 ///
393 /// '--<name>=<val>', '--<name>', or '--no-<name>'
394 ///
395 /// It actually calls the previous 'set' function after parsing 'arg'. The
396 /// same values are expected as for 'is_valid_long_option' above and as
397 /// with 'set' any value outside of the range of legal values for a
398 /// particular option are set to either the minimum or maximum depending on
399 /// which side of the valid interval they lie.
400 ///
401 /// require (CONFIGURING)
402 /// ensure (CONFIGURING)
403 ///
404 pub fn set_long_option(solver: &mut UniquePtr<Solver>, arg: String) -> bool;
405
406 /// Determine whether 'name' is a valid configuration.
407 ///
408 #[must_use]
409 pub fn is_valid_configuration(name: String) -> bool;
410
411 /// Overwrite (some) options with the forced values of the configuration.
412 /// The result is 'true' iff the 'name' is a valid configuration.
413 ///
414 /// require (CONFIGURING)
415 /// ensure (CONFIGURING)
416 ///
417 pub fn configure(solver: &mut UniquePtr<Solver>, name: String) -> bool;
418
419 /// Increase preprocessing and inprocessing limits by '10^<val>'. Values
420 /// below '0' are ignored and values above '9' are reduced to '9'.
421 ///
422 /// require (READY)
423 /// ensure (READY)
424 ///
425 pub fn optimize(solver: &mut UniquePtr<Solver>, val: i32);
426
427 /// Specify search limits, where currently 'name' can be "conflicts",
428 /// "decisions", "preprocessing", or "localsearch". The first two limits
429 /// are unbounded by default. Thus using a negative limit for conflicts or
430 /// decisions switches back to the default of unlimited search (for that
431 /// particular limit). The preprocessing limit determines the number of
432 /// preprocessing rounds, which is zero by default. Similarly, the local
433 /// search limit determines the number of local search rounds (also zero by
434 /// default). As with 'set', the return value denotes whether the limit
435 /// 'name' is valid. These limits are only valid for the next 'solve' or
436 /// 'simplify' call and reset to their default after 'solve' returns (as
437 /// well as overwritten and reset during calls to 'simplify' and
438 /// 'lookahead'). We actually also have an internal "terminate" limit
439 /// which however should only be used for testing and debugging.
440 ///
441 /// require (READY)
442 /// ensure (READY)
443 ///
444 pub fn limit(solver: &mut UniquePtr<Solver>, arg: String, val: i32) -> bool;
445 pub fn is_valid_limit(solver: &mut UniquePtr<Solver>, arg: String) -> bool;
446
447 /// The number of currently active variables and clauses can be queried by
448 /// these functions. Variables become active if a clause is added with it.
449 /// They become inactive if they are eliminated or fixed at the root level
450 /// Clauses become inactive if they are satisfied, subsumed, eliminated.
451 /// Redundant clauses are reduced regularly and thus the 'redundant'
452 /// function is less useful.
453 ///
454 /// require (VALID)
455 /// ensure (VALID)
456 ///
457 /// Number of active variables.
458 #[must_use]
459 pub fn active(solver: &UniquePtr<Solver>) -> i32;
460
461 /// Number of active redundant clauses.
462 #[must_use]
463 pub fn redundant(solver: &UniquePtr<Solver>) -> i64;
464
465 /// Number of active irredundant clauses.
466 #[must_use]
467 pub fn irredundant(solver: &UniquePtr<Solver>) -> i64;
468
469 //------------------------------------------------------------------------
470 /// This function executes the given number of preprocessing rounds. It is
471 /// similar to 'solve' with 'limits ("preprocessing", rounds)' except that
472 /// no CDCL nor local search, nor lucky phases are executed. The result
473 /// values are also the same: 0=UNKNOWN, 10=SATISFIABLE, 20=UNSATISFIABLE.
474 /// As 'solve' it resets current assumptions and limits before returning.
475 /// The numbers of rounds should not be negative. If the number of rounds
476 /// is zero only clauses are restored (if necessary) and top level unit
477 /// propagation is performed, which both take some time.
478 ///
479 /// require (READY)
480 /// ensure (STEADY | SATISFIED | UNSATISFIED)
481 ///
482 pub fn simplify(solver: &mut UniquePtr<Solver>, rounds: i32) -> i32;
483
484 //------------------------------------------------------------------------
485 /// Force termination of 'solve' asynchronously.
486 ///
487 /// require (SOLVING | READY)
488 /// ensure (STEADY ) /// actually not immediately (synchronously)
489 ///
490 pub fn terminate(solver: &mut UniquePtr<Solver>);
491
492 //------------------------------------------------------------------------
493
494 /// We have the following common reference counting functions, which avoid
495 /// to restore clauses but require substantial user guidance. This was the
496 /// only way to use inprocessing in incremental SAT solving in Lingeling
497 /// (and before in MiniSAT's 'freeze' / 'thaw') and which did not use
498 /// automatic clause restoring. In general this is slower than
499 /// restoring clauses and should not be used.
500 ///
501 /// In essence the user freezes variables which potentially are still
502 /// needed in clauses added or assumptions used after the next 'solve'
503 /// call. As in Lingeling you can freeze a variable multiple times, but
504 /// then have to melt it the same number of times again in order to enable
505 /// variable eliminating on it etc. The arguments can be literals
506 /// (negative indices) but conceptually variables are frozen.
507 ///
508 /// In the old way of doing things without restore you should not use a
509 /// variable incrementally (in 'add' or 'assume'), which was used before
510 /// and potentially could have been eliminated in a previous 'solve' call.
511 /// This can lead to spurious satisfying assignment. In order to check
512 /// this API contract one can use the 'checkfrozen' option. This has the
513 /// drawback that restoring clauses implicitly would fail with a fatal
514 /// error message even if in principle the solver could just restore
515 /// clauses. Thus this option is disabled by default.
516 ///
517 /// See our SAT'19 paper [FazekasBiereScholl-SAT'19] for more details.
518 ///
519 /// require (VALID)
520 /// ensure (VALID)
521 ///
522 #[must_use]
523 pub fn frozen(solver: &UniquePtr<Solver>, lit: i32) -> bool;
524 pub fn freeze(solver: &mut UniquePtr<Solver>, lit: i32);
525 pub fn melt(solver: &mut UniquePtr<Solver>, lit: i32);
526
527 //------------------------------------------------------------------------
528 /// Root level assigned variables can be queried with this function.
529 /// It returns '1' if the literal is implied by the formula, '-1' if its
530 /// negation is implied, or '0' if this is unclear at this point.
531 ///
532 /// require (VALID)
533 /// ensure (VALID)
534 ///
535 #[must_use]
536 pub fn fixed(solver: &UniquePtr<Solver>, lit: i32) -> i32;
537
538 //------------------------------------------------------------------------
539 /// Force the default decision phase of a variable to a certain value.
540 ///
541 pub fn phase(solver: &mut UniquePtr<Solver>, lit: i32);
542 pub fn unphase(solver: &mut UniquePtr<Solver>, lit: i32);
543
544 //------------------------------------------------------------------------
545 /// Enables clausal proof tracing in DRAT format and returns 'true' if
546 /// successfully opened for writing. Writing proofs has to be enabled
547 /// before calling 'solve', 'add' and 'dimacs', that is in state
548 /// 'CONFIGURING'. Otherwise only partial proofs would be written.
549 ///
550 /// require (CONFIGURING)
551 /// ensure (CONFIGURING)
552 ///
553 /// Write DRAT proof.
554 pub fn trace_proof1(solver: &mut UniquePtr<Solver>, file: String, name: String) -> bool;
555
556 /// Open & write proof.
557 pub fn trace_proof2(solver: &mut UniquePtr<Solver>, path: String) -> bool;
558
559 /// Flushing the proof trace file eventually calls 'fflush' on the actual
560 /// file or pipe and thus if this function returns all the proof steps
561 /// should have been written (with the same guarantees as 'fflush').
562 ///
563 /// The additional optional argument forces to print the number of addition
564 /// and deletion steps in the proof even if the verbosity level is zero but
565 /// not if quiet is set as well. The default for the stand-alone solver is
566 /// to print this information (in the 'closing proof' section) but for API
567 /// usage of the library we want to stay silent unless explicitly requested
568 /// or verbosity is non-zero (and as explained quiet is not set).
569 ///
570 /// This function can be called multiple times.
571 ///
572 /// require (VALID)
573 /// ensure (VALID)
574 ///
575 pub fn flush_proof_trace(solver: &mut UniquePtr<Solver>, print: bool);
576
577 /// Close proof trace early. Similar to 'flush' we allow the user to
578 /// control with 'print' in a more fine-grained way whether statistics
579 /// about the size of the written proof file and if compressed on-the-fly
580 /// the number of actual bytes written (including deflation percentage) are
581 /// printed. Before actually closing (or detaching in case of writing to
582 /// '<stdout>') we check whether 'flush_proof_trace' was called since the
583 /// last time a proof step (addition or deletion) was traced. If this is
584 /// not the case we would call 'flush_proof_trace' with the same 'print'
585 /// argument.
586 ///
587 /// require (VALID)
588 /// ensure (VALID)
589 ///
590 pub fn close_proof_trace(solver: &mut UniquePtr<Solver>, print: bool);
591
592 /// Enables clausal proof tracing with or without antecedents using
593 /// the Tracer interface defined in 'tracer.hpp'
594 ///
595 /// InternalTracer, StatTracer and FileTracer for internal use
596 ///
597 /// require (CONFIGURING)
598 /// ensure (CONFIGURING)
599 ///
600 pub fn connect_proof_tracer1(
601 solver: &mut UniquePtr<Solver>,
602 tracer: &mut UniquePtr<Tracer>,
603 antecedents: bool,
604 );
605 pub fn connect_proof_tracer2(
606 solver: &mut UniquePtr<Solver>,
607 tracer: &mut UniquePtr<InternalTracer>,
608 antecedents: bool,
609 );
610 pub fn connect_proof_tracer3(
611 solver: &mut UniquePtr<Solver>,
612 tracer: &mut UniquePtr<StatTracer>,
613 antecedents: bool,
614 );
615 pub fn connect_proof_tracer4(
616 solver: &mut UniquePtr<Solver>,
617 tracer: &mut UniquePtr<FileTracer>,
618 antecedents: bool,
619 );
620
621 /// Triggers the conclusion of incremental proofs.
622 /// if the solver is SATISFIED it will trigger extend ()
623 /// and give the model to the proof tracer through conclude_sat ()
624 /// if the solver is UNSATISFIED it will trigger failing ()
625 /// which will learn new clauses as explained below:
626 /// In case of failed assumptions will provide a core negated
627 /// as a clause through the proof tracer interface.
628 /// With a failing contraint these can be multiple clauses.
629 /// Then it will trigger a conclude_unsat event with the id(s)
630 /// of the newly learnt clauses or the id of the global conflict.
631 ///
632 /// require (SATISFIED || UNSATISFIED)
633 /// ensure (SATISFIED || UNSATISFIED)
634 ///
635 pub fn conclude(solver: &mut UniquePtr<Solver>);
636
637 /// Disconnect proof tracer. If this is not done before deleting
638 /// the tracer will be deleted. Returns true if successful.
639 ///
640 /// require (VALID)
641 /// ensure (VALID)
642 ///
643 pub fn disconnect_proof_tracer1(
644 solver: &mut UniquePtr<Solver>,
645 tracer: &mut UniquePtr<Tracer>,
646 ) -> bool;
647 pub fn disconnect_proof_tracer2(
648 solver: &mut UniquePtr<Solver>,
649 tracer: &mut UniquePtr<StatTracer>,
650 ) -> bool;
651 pub fn disconnect_proof_tracer3(
652 solver: &mut UniquePtr<Solver>,
653 tracer: &mut UniquePtr<FileTracer>,
654 ) -> bool;
655
656 /// print usage information for long options
657 pub fn usage();
658
659 /// print configuration usage options
660 pub fn configurations();
661
662 /// require (!DELETING)
663 /// ensure (!DELETING)
664 ///
665 /// print statistics
666 pub fn statistics(solver: &mut UniquePtr<Solver>);
667
668 /// print resource usage (time and memory)
669 pub fn resources(solver: &mut UniquePtr<Solver>);
670
671 /// require (VALID)
672 /// ensure (VALID)
673 ///
674 /// print current option and value list
675 pub fn options(solver: &mut UniquePtr<Solver>);
676
677 //------------------------------------------------------------------------
678 /// Traverse irredundant clauses or the extension stack in reverse order.
679 ///
680 /// The return value is false if traversal is aborted early due to one of
681 /// the visitor functions returning false. See description of the
682 /// iterators below for more details on how to use these functions.
683 ///
684 /// require (VALID)
685 /// ensure (VALID)
686 ///
687 pub fn traverse_clauses(
688 solver: &UniquePtr<Solver>,
689 i: &mut UniquePtr<ClauseIterator>,
690 ) -> bool;
691 pub fn traverse_witnesses_backward(
692 solver: &UniquePtr<Solver>,
693 i: &mut UniquePtr<WitnessIterator>,
694 ) -> bool;
695 pub fn traverse_witnesses_forward(
696 solver: &UniquePtr<Solver>,
697 i: &mut UniquePtr<WitnessIterator>,
698 ) -> bool;
699
700 //------------------------------------------------------------------------
701 /// Files with explicit path argument support compressed input and output
702 /// if appropriate helper functions 'gzip' etc. are available. They are
703 /// called through opening a pipe to an external command.
704 ///
705 /// If the 'strict' argument is zero then the number of variables and
706 /// clauses specified in the DIMACS headers are ignored, i.e., the header
707 /// 'p cnf 0 0' is always legal. If the 'strict' argument is larger '1'
708 /// strict formatting of the header is required, i.e., single spaces
709 /// everywhere and no trailing white space.
710 ///
711 /// Returns zero if successful and otherwise an error message.
712 ///
713 /// require (VALID)
714 /// ensure (VALID)
715 ///
716 pub fn read_dimacs1(
717 solver: &mut UniquePtr<Solver>,
718 file: String,
719 name: String,
720 vars: &mut i32,
721 strict: i32,
722 ) -> String;
723
724 pub fn read_dimacs2(
725 solver: &mut UniquePtr<Solver>,
726 path: String,
727 vars: &mut i32,
728 strict: i32,
729 ) -> String;
730
731 /// The following routines work the same way but parse both DIMACS and
732 /// INCCNF files (with 'p inccnf' header and 'a <cube>' lines). If the
733 /// parser finds and 'p inccnf' header or cubes then '*incremental' is set
734 /// to true and the cubes are stored in the given vector (each cube
735 /// terminated by a zero).
736 pub fn read_dimacs3(
737 solver: &mut UniquePtr<Solver>,
738 file: String,
739 name: String,
740 vars: &mut i32,
741 strict: i32,
742 incremental: &mut bool,
743 cubes: &mut Vec<i32>,
744 ) -> String;
745
746 pub fn read_dimacs4(
747 solver: &mut UniquePtr<Solver>,
748 path: String,
749 vars: &mut i32,
750 strict: i32,
751 incremental: &mut bool,
752 cubes: &mut Vec<i32>,
753 ) -> String;
754
755 //------------------------------------------------------------------------
756 /// Write current irredundant clauses and all derived unit clauses
757 /// to a file in DIMACS format. Clauses on the extension stack are
758 /// not included, nor any redundant clauses.
759 ///
760 /// The 'min_max_var' parameter gives a lower bound on the number '<vars>'
761 /// of variables used in the DIMACS 'p cnf <vars> ...' header.
762 ///
763 /// Returns zero if successful and otherwise an error message.
764 ///
765 /// require (VALID)
766 /// ensure (VALID)
767 ///
768 pub fn write_dimacs(
769 solver: &mut UniquePtr<Solver>,
770 path: String,
771 min_max_var: i32,
772 ) -> String;
773
774 /// The extension stack for reconstruction a solution can be written too.
775 ///
776 pub fn write_extension(solver: &mut UniquePtr<Solver>, path: String) -> String;
777
778 /// Print build configuration to a file with prefix 'c '. If the file
779 /// is '<stdout>' or '<stderr>' then terminal color codes might be used.
780 ///
781 pub fn build(file: String, prefix: String);
782
783 // ****************************************************************************************
784 // API for connected objects
785 // ****************************************************************************************
786
787 /// Connected terminators are checked for termination regularly. If the
788 /// 'terminate' function of the terminator returns true the solver is
789 /// terminated synchronously as soon it calls this function.
790 ///
791 /// # Safety
792 ///
793 /// The pointers in this function and in the function passed to it are
794 /// there to allow the state changes. Where the pointer points to a
795 /// generic state that the user of this function wants. This pointer must
796 /// remain valid throughout the run.
797 #[allow(clippy::missing_safety_doc)]
798 pub unsafe fn new_terminator(
799 s: *mut u8,
800 terminate: unsafe fn(*mut u8) -> bool,
801 ) -> UniquePtr<Terminator>;
802
803 /// Connected learners which can be used to export learned clauses.
804 /// The 'learning' can check the size of the learn clause and only if it
805 /// returns true then the individual literals of the learned clause are given
806 /// to the learn through 'learn' one by one terminated by a zero literal.
807 ///
808 /// # Safety
809 ///
810 /// The pointers in this function and in the function passed to it are
811 /// there to allow the state changes. Where the pointer points to a
812 /// generic state that the user of this function wants. This pointer must
813 /// remain valid throughout the run.
814 #[allow(clippy::missing_safety_doc)]
815 pub unsafe fn new_learner(
816 s: *mut u8,
817 learning: unsafe fn(*mut u8, i32) -> bool,
818 learn: unsafe fn(*mut u8, i32),
819 ) -> UniquePtr<Learner>;
820
821 /// Connected listener gets notified whenever the truth value of a variable is
822 /// fixed (for example during inprocessing or due to some derived unit clauses).
823 ///
824 /// # Safety
825 ///
826 /// The pointers in this function and in the function passed to it are
827 /// there to allow the state changes. Where the pointer points to a
828 /// generic state that the user of this function wants. This pointer must
829 /// remain valid throughout the run.
830 #[allow(clippy::missing_safety_doc)]
831 pub unsafe fn new_fixed_assignment_listener(
832 s: *mut u8,
833 fixed: unsafe fn(*mut u8, i32),
834 ) -> UniquePtr<FixedAssignmentListener>;
835
836 /// Allows to traverse all remaining irredundant clauses. Satisfied and
837 /// eliminated clauses are not included, nor any derived units unless such
838 /// a unit literal is frozen. Falsified literals are skipped. If the solver
839 /// is inconsistent only the empty clause is traversed.
840 ///
841 /// If 'clause' returns false traversal aborts early.
842 ///
843 /// # Safety
844 ///
845 /// The pointers in this function and in the function passed to it are
846 /// there to allow the state changes. Where the pointer points to a
847 /// generic state that the user of this function wants. This pointer must
848 /// remain valid throughout the run.
849 #[allow(clippy::missing_safety_doc)]
850 pub unsafe fn new_clause_iterator(
851 s: *mut u8,
852 clause: unsafe fn(*mut u8, &[i32]) -> bool,
853 ) -> UniquePtr<ClauseIterator>;
854
855 /// Allows to traverse all clauses on the extension stack together with their
856 /// witness cubes. If the solver is inconsistent, i.e., an empty clause is
857 /// found and the formula is unsatisfiable, then nothing is traversed.
858 ///
859 /// The clauses traversed in 'traverse_clauses' together with the clauses on
860 /// the extension stack are logically equivalent to the original clauses.
861 /// See our SAT'19 paper for more details.
862 ///
863 /// The witness literals can be used to extend and fix an assignment on the
864 /// remaining clauses to satisfy the clauses on the extension stack too.
865 ///
866 /// All derived units of non-frozen variables are included too.
867 ///
868 /// If 'witness' returns false traversal aborts early.
869 ///
870 /// # Safety
871 ///
872 /// The pointers in this function and in the function passed to it are
873 /// there to allow the state changes. Where the pointer points to a
874 /// generic state that the user of this function wants. This pointer must
875 /// remain valid throughout the run.
876 #[allow(clippy::missing_safety_doc)]
877 pub unsafe fn new_witness_iterator(
878 s: *mut u8,
879 witness: unsafe fn(*mut u8, &[i32], &[i32], u64) -> bool,
880 ) -> UniquePtr<WitnessIterator>;
881
882 #[allow(clippy::missing_safety_doc, clippy::too_many_arguments)]
883 pub unsafe fn new_external_propagator(
884 s: *mut u8,
885 is_lazy: bool,
886 are_reasons_forgettable: bool,
887 notify_assignment: unsafe fn(*mut u8, &[i32]),
888 notify_new_decision_level: unsafe fn(*mut u8),
889 notify_backtrack: unsafe fn(*mut u8, usize),
890 cb_check_found_model: unsafe fn(*mut u8, &[i32]) -> bool,
891 cb_decide: unsafe fn(*mut u8) -> i32,
892 cb_propagate: unsafe fn(*mut u8) -> i32,
893 cb_add_reason_clause_lit: unsafe fn(*mut u8, i32) -> i32,
894 cb_has_external_clause: unsafe fn(*mut u8, *mut bool) -> bool,
895 cb_add_external_clause_lit: unsafe fn(*mut u8) -> i32,
896 ) -> UniquePtr<ExternalPropagator>;
897
898 #[allow(clippy::missing_safety_doc, clippy::too_many_arguments)]
899 pub unsafe fn new_tracer(
900 initial_state: *mut u8,
901 add_original_clause: unsafe fn(*mut u8, u64, bool, &[i32], bool),
902 add_derived_clause: unsafe fn(*mut u8, u64, bool, &[i32], &[u64]),
903 delete_clause: unsafe fn(*mut u8, u64, bool, &[i32]),
904 weaken_minus: unsafe fn(*mut u8, u64, &[i32]),
905 strengthen: unsafe fn(*mut u8, u64),
906 finalize_clause: unsafe fn(*mut u8, u64, &[i32]),
907 add_assumption: unsafe fn(*mut u8, i32),
908 add_constraint: unsafe fn(*mut u8, &[i32]),
909 reset_assumptions: unsafe fn(*mut u8),
910 add_assumption_clause: unsafe fn(*mut u8, u64, &[i32], &[u64]),
911 conclude_sat: unsafe fn(*mut u8, i32, &[i32]),
912 conclude_unsat: unsafe fn(*mut u8, i32, &[u64]),
913 conclude_unknown: unsafe fn(*mut u8, &[i32]),
914 ) -> UniquePtr<Tracer>;
915 }
916}