-
Notifications
You must be signed in to change notification settings - Fork 120
/
cadical.hpp
1223 lines (1063 loc) · 47 KB
/
cadical.hpp
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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
#ifndef _cadical_hpp_INCLUDED
#define _cadical_hpp_INCLUDED
#include <cstdint>
#include <cstdio>
#include <vector>
namespace CaDiCaL {
/*========================================================================*/
// This provides the actual API of the CaDiCaL solver, which is implemented
// in the class 'Solver' below. Beside its constructor and destructor most
// important is the IPASIR part which you can find between 'BEGIN IPASIR'
// and 'END IPASIR' comments below. The following '[Example]' below might
// also be a good starting point to understand the API.
/*========================================================================*/
// The SAT competition standardized the exit code of SAT solvers to the
// following which then is also used return code for 'solve' functions.
// In the following example we use those constants for brevity though.
enum Status {
SATISFIABLE = 10,
UNSATISFIABLE = 20,
UNKNOWN = 0,
};
/*========================================================================*/
// [Example]
//
// The internal solver state follows the IPASIR API model used in the
// incremental track of the SAT competition. State transitions are
// triggered by member function calls, declared and described below.
//
// Consider the following code (from 'test/api/example.cpp') of API usage:
//
// CaDiCaL::Solver * solver = new CaDiCaL::Solver;
//
// // ------------------------------------------------------------------
// // Encode Problem and check without assumptions.
//
// enum { TIE = 1, SHIRT = 2 };
//
// solver->add (-TIE), solver->add (SHIRT), solver->add (0);
// solver->add (TIE), solver->add (SHIRT), solver->add (0);
// solver->add (-TIE), solver->add (-SHIRT), solver->add (0);
//
// int res = solver->solve (); // Solve instance.
// assert (res == 10); // Check it is 'SATISFIABLE'.
//
// res = solver->val (TIE); // Obtain assignment of 'TIE'.
// assert (res < 0); // Check 'TIE' assigned to 'false'.
//
// res = solver->val (SHIRT); // Obtain assignment of 'SHIRT'.
// assert (res > 0); // Check 'SHIRT' assigned to 'true'.
//
// // ------------------------------------------------------------------
// // Incrementally solve again under one assumption.
//
// solver->assume (TIE); // Now force 'TIE' to true.
//
// res = solver->solve (); // Solve again incrementally.
// assert (res == 20); // Check it is 'UNSATISFIABLE'.
//
// res = solver->failed (TIE); // Check 'TIE' responsible.
// assert (res); // Yes, 'TIE' in core.
//
// res = solver->failed (SHIRT); // Check 'SHIRT' responsible.
// assert (!res); // No, 'SHIRT' not in core.
//
// // ------------------------------------------------------------------
// // Incrementally solve once more under another assumption.
//
// solver->assume (-SHIRT); // Now force 'SHIRT' to false.
//
// res = solver->solve (); // Solve again incrementally.
// assert (res == 20); // Check it is 'UNSATISFIABLE'.
//
// res = solver->failed (TIE); // Check 'TIE' responsible.
// assert (!res); // No, 'TIE' not in core.
//
// res = solver->failed (-SHIRT); // Check '!SHIRT' responsible.
// assert (res); // Yes, '!SHIRT' in core.
//
// // ------------------------------------------------------------------
//
// delete solver;
/*========================================================================*/
// [States and Transitions]
//
// Compared to IPASIR we also use an 'ADDING' state in which the solver
// stays while adding non-zero literals until the clause is completed
// through adding a zero literal. The additional 'INITIALIZING',
// 'CONFIGURING' and 'DELETING' states are also not part of IPASIR but also
// useful for testing and debugging.
//
// We have the following transitions which are all synchronous except for
// the reentrant 'terminate' call:
//
// new
// INITIALIZING --------------------------> CONFIGURING
//
// set / trace
// CONFIGURING --------------------------> CONFIGURING
//
// add (non zero literal)
// VALID --------------------------> ADDING
//
// add (zero literal)
// VALID --------------------------> STEADY
//
// assume (non zero literal)
// READY --------------------------> STEADY
//
// solve
// READY --------------------------> SOLVING
//
// (internal)
// SOLVING --------------------------> READY
//
// val (non zero literal)
// SATISFIED --------------------------> SATISFIED
//
// failed (non zero literal )
// UNSATISFIED --------------------------> UNSATISFIED
//
// delete
// VALID --------------------------> DELETING
//
// where
//
// READY = CONFIGURING | STEADY | SATISFIED | UNSATISFIED
// VALID = READY | ADDING
// INVALID = INITIALIZING | DELETING
//
// The 'SOLVING' state is only visible in different contexts, i.e., from
// another thread or from a signal handler. It is used to implement
// 'terminate'. Here is the only asynchronous transition:
//
// terminate (asynchronously)
// SOLVING -------------------------> STEADY
//
// The important behaviour to remember is that adding, assuming or
// constraining a literal (immediately) destroys the satisfying assignment
// in the 'SATISFIED' state and vice versa resets all assumptions in the
// 'UNSATISFIED' state. This is exactly the behaviour required by the IPASIR
// interface.
//
// Furthermore, the model can only be queried through 'val' in the
// 'SATISFIED' state, while extracting failed assumptions with 'failed' only
// in the 'UNSATISFIED' state. Solving can only be started in the 'STEADY '
// or 'CONFIGURING' state or after the previous call to 'solve' yielded an
// 'STEADY , 'SATISFIED' or 'UNSATISFIED' state.
//
// All literals have to be valid literals too, i.e., 32-bit integers
// different from 'INT_MIN'. If any of these requirements is violated the
// solver aborts with an 'API contract violation' message.
//
// HINT: If you do not understand why a contract is violated you can run
// 'mobical' on the failing API call trace. Point the environment variable
// 'CADICAL_API_TRACE' to the file where you want to save the trace during
// execution of your program linking against the library. You probably need
// for 'mobical' to use the option '--do-not-enforce-contracts' though to
// force running into the same contract violation.
//
// Additional API calls (like 'freeze' and 'melt') do not change the state
// of the solver and are all described below.
/*========================================================================*/
// States are represented by a bit-set in order to combine them.
enum State {
INITIALIZING = 1, // during initialization (invalid)
CONFIGURING = 2, // configure options (with 'set')
STEADY = 4, // ready to call 'solve'
ADDING = 8, // adding clause literals (zero missing)
SOLVING = 16, // while solving (within 'solve')
SATISFIED = 32, // satisfiable allows 'val'
UNSATISFIED = 64, // unsatisfiable allows 'failed'
DELETING = 128, // during and after deletion (invalid)
// These combined states are used to check contracts.
READY = CONFIGURING | STEADY | SATISFIED | UNSATISFIED,
VALID = READY | ADDING,
INVALID = INITIALIZING | DELETING
};
/*------------------------------------------------------------------------*/
// Opaque classes needed in the API and declared in the same namespace.
class File;
struct Internal;
struct External;
/*------------------------------------------------------------------------*/
// Forward declaration of call-back classes. See bottom of this file.
class Learner;
class Terminator;
class ClauseIterator;
class WitnessIterator;
class ExternalPropagator;
class Tracer;
class InternalTracer;
class FileTracer;
class StatTracer;
/*------------------------------------------------------------------------*/
class Solver {
public:
// ====== BEGIN IPASIR ===================================================
// This section implements the corresponding IPASIR functionality.
Solver ();
~Solver ();
static const char *signature (); // name of this library
// Core functionality as in the IPASIR incremental SAT solver interface.
// (recall 'READY = CONFIGURING | STEADY | SATISFIED | UNSATISFIED').
// Further note that 'lit' is required to be different from 'INT_MIN' and
// different from '0' except for 'add'.
// Add valid literal to clause or zero to terminate clause.
//
// require (VALID) // recall 'VALID = READY | ADDING'
// if (lit) ensure (ADDING) // and thus VALID but not READY
// if (!lit) ensure (STEADY ) // and thus READY
//
void add (int lit);
// Here are functions simplifying clause addition. The given literals
// should all be valid (different from 'INT_MIN' and different from '0').
//
// require (VALID)
// ensure (STEADY )
//
void clause (int); // Add unit clause.
void clause (int, int); // Add binary clause.
void clause (int, int, int); // Add ternary clause.
void clause (int, int, int, int); // Add quaternary clause.
void clause (int, int, int, int, int); // Add quinternary clause.
void clause (const std::vector<int> &); // Add literal vector as clause.
void clause (const int *, size_t); // Add literal array as clause.
// This function can be used to check if the formula is already
// inconsistent (contains the empty clause or was proven to be
// root-level unsatisfiable).
bool inconsistent ();
// Assume valid non zero literal for next call to 'solve'. These
// assumptions are reset after the call to 'solve' as well as after
// returning from 'simplify' and 'lookahead.
//
// require (READY)
// ensure (STEADY )
//
void assume (int lit);
// Try to solve the current formula. Returns
//
// 0 = UNKNOWN (limit reached or interrupted through 'terminate')
// 10 = SATISFIABLE
// 20 = UNSATISFIABLE
//
// require (READY)
// ensure (STEADY | SATISFIED | UNSATISFIED)
//
// Note, that while in this call the solver actually transitions to state
// 'SOLVING', which however is only visible from a different context,
// i.e., from a different thread or from a signal handler. Only right
// before returning from this call it goes into a 'READY' state.
//
int solve ();
// Get value (-lit=false, lit=true) of valid non-zero literal.
//
// require (SATISFIED)
// ensure (SATISFIED)
//
int val (int lit);
// Try to flip the value of the given literal without falsifying the
// formula. Returns 'true' if this was successful. Otherwise the model is
// not changed and 'false' is returned. If a literal was eliminated or
// substituted flipping will fail on that literal and in particular the
// solver will not taint it nor restore any clauses.
//
// The 'flip' function can only flip the value of a variables not acting
// as witness on the reconstruction stack.
//
// As a side effect of calling this function first all assigned variables
// are propagated again without using blocking literal. Thus the first
// call to this function after obtaining a model adds a substantial
// overhead. Subsequent calls will not need to properly propagate again.
//
// Furthermore if the reconstruction stack is non-empty and has been
// traversed to reconstruct a full extended model for eliminated
// variables (and to satisfy removed blocked clauses), the values of these
// witness variables obtained via 'val' before become invalid. The user
// thus will need to call 'val' again after calling 'flip' which will
// trigger then a traversal of the reconstruction stack.
//
// So try to avoid mixing 'flip' and 'val' (for efficiency only).
// Further, this functionality is currently not supported in the presence
// of an external propagator.
//
// require (SATISFIED)
// ensure (SATISFIED)
//
bool flip (int lit);
// Same as 'flip' without actually flipping it. This functionality is
// currently not supported in the presence of an external propagator.
//
// require (SATISFIED)
// ensure (SATISFIED)
//
bool flippable (int lit);
// Determine whether the valid non-zero literal is in the core.
// Returns 'true' if the literal is in the core and 'false' otherwise.
// Note that the core does not have to be minimal.
//
// require (UNSATISFIED)
// ensure (UNSATISFIED)
//
bool failed (int lit);
// Add call-back which is checked regularly for termination. There can
// only be one terminator connected. If a second (non-zero) one is added
// the first one is implicitly disconnected.
//
// require (VALID)
// ensure (VALID)
//
void connect_terminator (Terminator *terminator);
void disconnect_terminator ();
// Add call-back which allows to export learned clauses.
//
// require (VALID)
// ensure (VALID)
//
void connect_learner (Learner *learner);
void disconnect_learner ();
// ====== END IPASIR =====================================================
// ====== BEGIN IPASIR-UP ================================================
// Add call-back which allows to learn, propagate and backtrack based on
// external constraints. Only one external propagator can be connected
// and after connection every related variables must be 'observed' (use
// 'add_observed_var' function).
// Disconnection of the external propagator resets all the observed
// variables.
//
// require (VALID)
// ensure (VALID)
//
void connect_external_propagator (ExternalPropagator *propagator);
void disconnect_external_propagator ();
// Mark as 'observed' those variables that are relevant to the external
// propagator. External propagation, clause addition during search and
// notifications are all over these observed variabes.
// A variable can not be observed witouth having an external propagator
// connected. Observed variables are "frozen" internally, and so
// inprocessing will not consider them as candidates for elimination.
// An observed variable is allowed to be a fresh variable and it can be
// added also during solving.
//
// require (VALID_OR_SOLVING)
// ensure (VALID_OR_SOLVING)
//
void add_observed_var (int var);
// Removes the 'observed' flag from the given variable. A variable can be
// set unobserved only between solve calls, not during it (to guarantee
// that no yet unexplained external propagation involves it).
//
// require (VALID)
// ensure (VALID)
//
void remove_observed_var (int var);
// Removes all the 'observed' flags from the variables. Disconnecting the
// propagator invokes this step as well.
//
// require (VALID)
// ensure (VALID)
//
void reset_observed_vars ();
// Get reason of valid observed literal (true = it is an observed variable
// and it got assigned by a decision during the CDCL loop. Otherwise:
// false.
//
// require (VALID_OR_SOLVING)
// ensure (VALID_OR_SOLVING)
//
bool is_decision (int lit);
// ====== END IPASIR-UP ==================================================
//------------------------------------------------------------------------
// Adds a literal to the constraint clause. Same functionality as 'add'
// but the clause only exists for the next call to solve (same lifetime as
// assumptions). Only one constraint may exists at a time. A new
// constraint replaces the old. The main application of this functonality
// is the model checking algorithm IC3. See our FMCAD'21 paper
// [FroleyksBiere-FMCAD'19] for more details.
//
// Add valid literal to the constraint clause or zero to terminate it.
//
// require (VALID) // recall 'VALID = READY |
// ADDING' if (lit) ensure (ADDING) // and thus VALID but not
// READY if (!lit) && !adding_clause ensure (STEADY ) // and thus READY
//
void constrain (int lit);
// Determine whether the constraint was used to proof the
// unsatisfiability. Note that the formula might still be unsatisfiable
// without the constraint.
//
// require (UNSATISFIED)
// ensure (UNSATISFIED)
//
bool constraint_failed ();
//------------------------------------------------------------------------
// This function determines a good splitting literal. The result can be
// zero if the formula is proven to be satisfiable or unsatisfiable. This
// can then be checked by 'state ()'. If the formula is empty and
// the function is not able to determine satisfiability also zero is
// returned but the state remains steady.
//
// require (READY)
// ensure (STEADY |SATISFIED|UNSATISFIED)
//
int lookahead (void);
struct CubesWithStatus {
int status;
std::vector<std::vector<int>> cubes;
};
CubesWithStatus generate_cubes (int, int min_depth = 0);
void reset_assumptions ();
void reset_constraint ();
// Return the current state of the solver as defined above.
//
const State &state () const { return _state; }
// Similar to 'state ()' but using the staddard competition exit codes of
// '10' for 'SATISFIABLE', '20' for 'UNSATISFIABLE' and '0' otherwise.
//
int status () const {
if (_state == SATISFIED)
return 10;
else if (_state == UNSATISFIED)
return 20;
else
return 0;
}
/*----------------------------------------------------------------------*/
static const char *version (); // return version string
/*----------------------------------------------------------------------*/
// Copy 'this' into a fresh 'other'. The copy procedure is not a deep
// clone, but only copies irredundant clauses and units. It also makes
// sure that witness reconstruction works with the copy as with the
// original formula such that both solvers have the same models.
// Assumptions are not copied. Options however are copied as well as
// flags which remember the current state of variables in preprocessing.
//
// require (READY) // for 'this'
// ensure (READY) // for 'this'
//
// other.require (CONFIGURING)
// other.ensure (CONFIGURING | STEADY )
//
void copy (Solver &other) const;
/*----------------------------------------------------------------------*/
// Variables are usually added and initialized implicitly whenever a
// literal is used as an argument except for the functions 'val', 'fixed',
// 'failed' and 'frozen'. However, the library internally keeps a maximum
// variable index, which can be queried.
//
// require (VALID | SOLVING)
// ensure (VALID | SOLVING)
//
int vars ();
// Increase the maximum variable index explicitly. This function makes
// sure that at least 'min_max_var' variables are initialized. Since it
// might need to reallocate tables, it destroys a satisfying assignment
// and has the same state transition and conditions as 'assume' etc.
//
// require (READY)
// ensure (STEADY )
//
void reserve (int min_max_var);
#ifndef NTRACING
//------------------------------------------------------------------------
// This function can be used to write API calls to a file. The same
// format is used which 'mobical' can read, execute and also shrink
// through delta debugging.
//
// Tracing API calls can also be achieved by using the environment
// variable 'CADICAL_API_TRACE'. That alternative is useful if you do not
// want to change the source code using the solver, e.g., if you only have
// a binary with the solver linked in. However, that method only allows
// to trace one solver instance, while with the following function API
// tracing can be enabled for different solver instances individually.
//
// The solver will flush the file after every trace API call but does not
// close it during deletion. It remains owned by the user of the library.
//
// require (VALID)
// ensure (VALID)
//
void trace_api_calls (FILE *file);
#endif
//------------------------------------------------------------------------
// Option handling.
// Determine whether 'name' is a valid option name.
//
static bool is_valid_option (const char *name);
// Determine whether 'name' enables a specific preprocessing technique.
//
static bool is_preprocessing_option (const char *name);
// Determine whether 'arg' is a valid long option of the form '--<name>',
// '--<name>=<val>' or '--no-<name>' similar to 'set_long_option' below.
// Legal values are 'true', 'false', or '[-]<mantissa>[e<exponent>]'.
static bool is_valid_long_option (const char *arg);
// Get the current value of the option 'name'. If 'name' is invalid then
// zero is returned. Here '--...' arguments as invalid options.
//
int get (const char *name);
// Set the default verbose message prefix (default "c ").
//
void prefix (const char *verbose_message_prefix);
// Explicit version of setting an option. If the option '<name>' exists
// and '<val>' can be parsed then 'true' is returned. If the option value
// is out of range the actual value is computed as the closest (minimum or
// maximum) value possible, but still 'true' is returned.
//
// require (CONFIGURING)
// ensure (CONFIGURING)
//
// Thus options can only bet set right after initialization.
//
bool set (const char *name, int val);
// This function accepts options in command line syntax:
//
// '--<name>=<val>', '--<name>', or '--no-<name>'
//
// It actually calls the previous 'set' function after parsing 'arg'. The
// same values are expected as for 'is_valid_long_option' above and as
// with 'set' any value outside of the range of legal values for a
// particular option are set to either the minimum or maximum depending on
// which side of the valid interval they lie.
//
// require (CONFIGURING)
// ensure (CONFIGURING)
//
bool set_long_option (const char *arg);
// Determine whether 'name' is a valid configuration.
//
static bool is_valid_configuration (const char *);
// Overwrite (some) options with the forced values of the configuration.
// The result is 'true' iff the 'name' is a valid configuration.
//
// require (CONFIGURING)
// ensure (CONFIGURING)
//
bool configure (const char *);
// Increase preprocessing and inprocessing limits by '10^<val>'. Values
// below '0' are ignored and values above '9' are reduced to '9'.
//
// require (READY)
// ensure (READY)
//
void optimize (int val);
// Specify search limits, where currently 'name' can be "conflicts",
// "decisions", "preprocessing", or "localsearch". The first two limits
// are unbounded by default. Thus using a negative limit for conflicts or
// decisions switches back to the default of unlimited search (for that
// particular limit). The preprocessing limit determines the number of
// preprocessing rounds, which is zero by default. Similarly, the local
// search limit determines the number of local search rounds (also zero by
// default). As with 'set', the return value denotes whether the limit
// 'name' is valid. These limits are only valid for the next 'solve' or
// 'simplify' call and reset to their default after 'solve' returns (as
// well as overwritten and reset during calls to 'simplify' and
// 'lookahead'). We actually also have an internal "terminate" limit
// which however should only be used for testing and debugging.
//
// require (READY)
// ensure (READY)
//
bool limit (const char *arg, int val);
bool is_valid_limit (const char *arg);
// The number of currently active variables and clauses can be queried by
// these functions. Variables become active if a clause is added with it.
// They become inactive if they are eliminated or fixed at the root level
// Clauses become inactive if they are satisfied, subsumed, eliminated.
// Redundant clauses are reduced regularly and thus the 'redundant'
// function is less useful.
//
// require (VALID)
// ensure (VALID)
//
int active () const; // Number of active variables.
int64_t redundant () const; // Number of active redundant clauses.
int64_t irredundant () const; // Number of active irredundant clauses.
//------------------------------------------------------------------------
// This function executes the given number of preprocessing rounds. It is
// similar to 'solve' with 'limits ("preprocessing", rounds)' except that
// no CDCL nor local search, nor lucky phases are executed. The result
// values are also the same: 0=UNKNOWN, 10=SATISFIABLE, 20=UNSATISFIABLE.
// As 'solve' it resets current assumptions and limits before returning.
// The numbers of rounds should not be negative. If the number of rounds
// is zero only clauses are restored (if necessary) and top level unit
// propagation is performed, which both take some time.
//
// require (READY)
// ensure (STEADY | SATISFIED | UNSATISFIED)
//
int simplify (int rounds = 3);
//------------------------------------------------------------------------
// Force termination of 'solve' asynchronously.
//
// require (SOLVING | READY)
// ensure (STEADY ) // actually not immediately (synchronously)
//
void terminate ();
//------------------------------------------------------------------------
// We have the following common reference counting functions, which avoid
// to restore clauses but require substantial user guidance. This was the
// only way to use inprocessing in incremental SAT solving in Lingeling
// (and before in MiniSAT's 'freeze' / 'thaw') and which did not use
// automatic clause restoring. In general this is slower than
// restoring clauses and should not be used.
//
// In essence the user freezes variables which potentially are still
// needed in clauses added or assumptions used after the next 'solve'
// call. As in Lingeling you can freeze a variable multiple times, but
// then have to melt it the same number of times again in order to enable
// variable eliminating on it etc. The arguments can be literals
// (negative indices) but conceptually variables are frozen.
//
// In the old way of doing things without restore you should not use a
// variable incrementally (in 'add' or 'assume'), which was used before
// and potentially could have been eliminated in a previous 'solve' call.
// This can lead to spurious satisfying assignment. In order to check
// this API contract one can use the 'checkfrozen' option. This has the
// drawback that restoring clauses implicitly would fail with a fatal
// error message even if in principle the solver could just restore
// clauses. Thus this option is disabled by default.
//
// See our SAT'19 paper [FazekasBiereScholl-SAT'19] for more details.
//
// require (VALID)
// ensure (VALID)
//
bool frozen (int lit) const;
void freeze (int lit);
void melt (int lit); // Also needs 'require (frozen (lit))'.
//------------------------------------------------------------------------
// Root level assigned variables can be queried with this function.
// It returns '1' if the literal is implied by the formula, '-1' if its
// negation is implied, or '0' if this is unclear at this point.
//
// require (VALID)
// ensure (VALID)
//
int fixed (int lit) const;
//------------------------------------------------------------------------
// Force the default decision phase of a variable to a certain value.
//
void phase (int lit);
void unphase (int lit);
//------------------------------------------------------------------------
// Enables clausal proof tracing in DRAT format and returns 'true' if
// successfully opened for writing. Writing proofs has to be enabled
// before calling 'solve', 'add' and 'dimacs', that is in state
// 'CONFIGURING'. Otherwise only partial proofs would be written.
//
// require (CONFIGURING)
// ensure (CONFIGURING)
//
bool trace_proof (FILE *file, const char *name); // Write DRAT proof.
bool trace_proof (const char *path); // Open & write proof.
// Flushing the proof trace file eventually calls 'fflush' on the actual
// file or pipe and thus if this function returns all the proof steps
// should have been written (with the same guarantees as 'fflush').
//
// The additional optional argument forces to print the number of addition
// and deletion steps in the proof even if the verbosity level is zero but
// not if quiet is set as well. The default for the stand-alone solver is
// to print this information (in the 'closing proof' section) but for API
// usage of the library we want to stay silent unless explicitly requested
// or verbosity is non-zero (and as explained quiet is not set).
//
// This function can be called multiple times.
//
// require (VALID)
// ensure (VALID)
//
void flush_proof_trace (bool print = false);
// Close proof trace early. Similar to 'flush' we allow the user to
// control with 'print' in a more fine-grained way whether statistics
// about the size of the written proof file and if compressed on-the-fly
// the number of actual bytes written (including deflation percentage) are
// printed. Before actually closing (or detaching in case of writing to
// '<stdout>') we check whether 'flush_proof_trace' was called since the
// last time a proof step (addition or deletion) was traced. If this is
// not the case we would call 'flush_proof_trace' with the same 'print'
// argument.
//
// require (VALID)
// ensure (VALID)
//
void close_proof_trace (bool print = false);
// Enables clausal proof tracing with or without antecedents using
// the Tracer interface defined in 'tracer.hpp'
//
// InternalTracer, StatTracer and FileTracer for internal use
//
// require (CONFIGURING)
// ensure (CONFIGURING)
//
void connect_proof_tracer (Tracer *tracer, bool antecedents);
void connect_proof_tracer (InternalTracer *tracer, bool antecedents);
void connect_proof_tracer (StatTracer *tracer, bool antecedents);
void connect_proof_tracer (FileTracer *tracer, bool antecedents);
// Triggers the conclusion of incremental proofs.
// if the solver is SATISFIED it will trigger extend ()
// and give the model to the proof tracer through conclude_sat ()
// if the solver is UNSATISFIED it will trigger failing ()
// which will learn new clauses as explained below:
// In case of failed assumptions will provide a core negated
// as a clause through the proof tracer interface.
// With a failing contraint these can be multiple clauses.
// Then it will trigger a conclude_unsat event with the id(s)
// of the newly learnt clauses or the id of the global conflict.
//
// require (SATISFIED || UNSATISFIED)
// ensure (SATISFIED || UNSATISFIED)
//
void conclude ();
// Disconnect proof tracer. If this is not done before deleting
// the tracer will be deleted. Returns true if successful.
//
// require (VALID)
// ensure (VALID)
//
bool disconnect_proof_tracer (Tracer *tracer);
bool disconnect_proof_tracer (StatTracer *tracer);
bool disconnect_proof_tracer (FileTracer *tracer);
//------------------------------------------------------------------------
static void usage (); // print usage information for long options
static void configurations (); // print configuration usage options
// require (!DELETING)
// ensure (!DELETING)
//
void statistics (); // print statistics
void resources (); // print resource usage (time and memory)
// require (VALID)
// ensure (VALID)
//
void options (); // print current option and value list
//------------------------------------------------------------------------
// Traverse irredundant clauses or the extension stack in reverse order.
//
// The return value is false if traversal is aborted early due to one of
// the visitor functions returning false. See description of the
// iterators below for more details on how to use these functions.
//
// require (VALID)
// ensure (VALID)
//
bool traverse_clauses (ClauseIterator &) const;
bool traverse_witnesses_backward (WitnessIterator &) const;
bool traverse_witnesses_forward (WitnessIterator &) const;
//------------------------------------------------------------------------
// Files with explicit path argument support compressed input and output
// if appropriate helper functions 'gzip' etc. are available. They are
// called through opening a pipe to an external command.
//
// If the 'strict' argument is zero then the number of variables and
// clauses specified in the DIMACS headers are ignored, i.e., the header
// 'p cnf 0 0' is always legal. If the 'strict' argument is larger '1'
// strict formatting of the header is required, i.e., single spaces
// everywhere and no trailing white space.
//
// Returns zero if successful and otherwise an error message.
//
// require (VALID)
// ensure (VALID)
//
const char *read_dimacs (FILE *file, const char *name, int &vars,
int strict = 1);
const char *read_dimacs (const char *path, int &vars, int strict = 1);
// The following routines work the same way but parse both DIMACS and
// INCCNF files (with 'p inccnf' header and 'a <cube>' lines). If the
// parser finds and 'p inccnf' header or cubes then '*incremental' is set
// to true and the cubes are stored in the given vector (each cube
// terminated by a zero).
const char *read_dimacs (FILE *file, const char *name, int &vars,
int strict, bool &incremental,
std::vector<int> &cubes);
const char *read_dimacs (const char *path, int &vars, int strict,
bool &incremental, std::vector<int> &cubes);
//------------------------------------------------------------------------
// Write current irredundant clauses and all derived unit clauses
// to a file in DIMACS format. Clauses on the extension stack are
// not included, nor any redundant clauses.
//
// The 'min_max_var' parameter gives a lower bound on the number '<vars>'
// of variables used in the DIMACS 'p cnf <vars> ...' header.
//
// Returns zero if successful and otherwise an error message.
//
// require (VALID)
// ensure (VALID)
//
const char *write_dimacs (const char *path, int min_max_var = 0);
// The extension stack for reconstruction a solution can be written too.
//
const char *write_extension (const char *path);
// Print build configuration to a file with prefix 'c '. If the file
// is '<stdout>' or '<stderr>' then terminal color codes might be used.
//
static void build (FILE *file, const char *prefix = "c ");
private:
//==== start of state ====================================================
// The solver is in the state ADDING if either the current clause or the
// constraint (or both) is not yet terminated.
bool adding_clause;
bool adding_constraint;
State _state; // API states as discussed above.
/*----------------------------------------------------------------------*/
// The 'Solver' class is a 'facade' object for 'External'. It exposes the
// public API of 'External' but hides everything else (except for the some
// private functions). It is supposed to make it easier to understand the
// API and use the solver through the API.
// This approach has the benefit of decoupling this header file from all
// internal data structures, which is particularly useful if the rest of
// the source is not available. For instance if only a CaDiCaL library is
// installed in a system, then only this header file has to be installed
// too, and still allows to compile and link against the library.
/*----------------------------------------------------------------------*/
// More precisely the CaDiCaL code is split into three layers:
//
// Solver: facade object providing the actual API of the solver
// External: communication layer between 'Solver' and 'Internal'
// Internal: the actual solver code
//
// The 'External' and 'Internal' layers are declared and implemented in
// the corresponding '{external,internal}.{hpp,cpp}' files (as expected),
// while the 'Solver' facade class is defined in 'cadical.hpp' (here) but
// implemented in 'solver.cpp'. The reason for this naming mismatch is,
// that we want to use 'cadical.hpp' for the library header (this header
// file) and call the binary of the stand alone SAT also 'cadical', which
// is more naturally implemented in 'cadical.cpp'.
//
// Separating 'External' from 'Internal' also allows us to map external
// literals to internal literals, which is useful with many fixed or
// eliminated variables (during 'compact' the internal variable range is
// reduced and external variables are remapped). Such an approach is also
// necessary, if we want to use extended resolution in the future (such as
// bounded variable addition).
//
Internal *internal; // Hidden internal solver.
External *external; // Hidden API to internal solver mapping.
#ifndef NTRACING
// The API calls to the solver can be traced by setting the environment
// variable 'CADICAL_API_TRACE' to point to the path of a file to which
// API calls are written. The same format is used which 'mobical' can
// read, execute and also shrink through delta debugging.
//
// The environment variable is read in the constructor and the trace is
// opened for writing and then closed again in the destructor.
//
// Alternatively one case use 'trace_api_calls'. Both
//
bool close_trace_api_file; // Close file if owned by solver it.
FILE *trace_api_file; // Also acts as flag that we are tracing.
static bool tracing_api_through_environment;
//===== end of state ====================================================
void trace_api_call (const char *) const;
void trace_api_call (const char *, int) const;
void trace_api_call (const char *, const char *) const;
void trace_api_call (const char *, const char *, int) const;
#endif
void transition_to_steady_state ();
//------------------------------------------------------------------------
// Used in the stand alone solver application 'App' and the model based
// tester 'Mobical'. So only these two classes need direct access to the
// otherwise more application specific functions listed here together with
// the internal DIMACS parser.
friend class App;
friend class Mobical;
friend class Parser;
// Read solution in competition format for debugging and testing.
//
// require (VALID)
// ensure (VALID)
//
const char *read_solution (const char *path);
// Cross-compilation with 'MinGW' needs some work-around for 'printf'
// style printing of 64-bit numbers including warning messages. The
// followings lines are copies of similar code in 'inttypes.hpp' but we
// want to keep the 'cadical.hpp' header file stand-alone.
#ifndef PRINTF_FORMAT
#ifdef __MINGW32__
#define __USE_MINGW_ANSI_STDIO 1