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
#ifndef _contract_hpp_INCLUDED
#define _contract_hpp_INCLUDED
/*------------------------------------------------------------------------*/
#ifndef NCONTRACTS
/*------------------------------------------------------------------------*/
// If the user violates API contracts while calling functions declared in
// 'cadical.hpp' and implemented in 'solver.cpp' then an error is reported.
// Currently we also force aborting the program. In the future it might be
// better to allow the user to provide a call back function, which then can
// for instance throw a C++ exception or execute a 'longjmp' in 'C' etc.
#define CONTRACT_VIOLATED(...) \
do { \
fatal_message_start (); \
fprintf (stderr, \
"invalid API usage of '%s' in '%s': ", __PRETTY_FUNCTION__, \
__FILE__); \
fprintf (stderr, __VA_ARGS__); \
fputc ('\n', stderr); \
fflush (stderr); \
abort (); \
} while (0)
/*------------------------------------------------------------------------*/
namespace CaDiCaL {
// It would be much easier to just write 'REQUIRE (this, "not initialized")'
// which however produces warnings due to the '-Wnonnull' check. Note, that
// 'this' is always assumed to be non zero in modern C++. Much worse, if we
// use instead 'this != 0' or something similar like 'this != nullptr' then
// optimization silently removes this check ('gcc-7.4.0' at least) even
// though of course a zero pointer might be used as 'this' if the user did
// not initialize it. The only solution I found is to disable optimization
// for this check. It does not seem to be necessary for 'clang++' though
// ('clang++-6.0.0' at least). The alternative is to not check that the
// user forgot to initialize the solver pointer, but as long this works we
// keep this ugly hack. It also forces the function not to be inlined.
// The actual code I is in 'contract.cpp'.
//
void require_solver_pointer_to_be_non_zero (const void *ptr,
const char *function_name,
const char *file_name);
#define REQUIRE_NON_ZERO_THIS() \
do { \
require_solver_pointer_to_be_non_zero (this, __PRETTY_FUNCTION__, \
__FILE__); \
} while (0)
} // namespace CaDiCaL
/*------------------------------------------------------------------------*/
// These are common shortcuts for 'Solver' API contracts (requirements).
#define REQUIRE(COND, ...) \
do { \
if ((COND)) \
break; \
CONTRACT_VIOLATED (__VA_ARGS__); \
} while (0)
#define REQUIRE_INITIALIZED() \
do { \
REQUIRE_NON_ZERO_THIS (); \
REQUIRE (external, "external solver not initialized"); \
REQUIRE (internal, "internal solver not initialized"); \
} while (0)
#define REQUIRE_VALID_STATE() \
do { \
REQUIRE_INITIALIZED (); \
REQUIRE (this->state () & VALID, "solver in invalid state"); \
} while (0)
#define REQUIRE_READY_STATE() \
do { \
REQUIRE_VALID_STATE (); \
REQUIRE (state () != ADDING, \
"clause incomplete (terminating zero not added)"); \
} while (0)
#define REQUIRE_VALID_OR_SOLVING_STATE() \
do { \
REQUIRE_INITIALIZED (); \
REQUIRE (this->state () & (VALID | SOLVING), \
"solver neither in valid nor solving state"); \
} while (0)
#define REQUIRE_VALID_LIT(LIT) \
do { \
REQUIRE ((int) (LIT) && ((int) (LIT)) != INT_MIN, \
"invalid literal '%d'", (int) (LIT)); \
REQUIRE (external->is_valid_input ((int) (LIT)), \
"extension variable %d defined by the solver " \
"(try using `vars ()` or `set (factor, 0)`)", \
(int) (LIT)); \
} while (0)
#define REQUIRE_STEADY_STATE() \
do { \
REQUIRE_INITIALIZED (); \
REQUIRE (this->state () & STEADY, "solver is not in steady state"); \
} while (0)
/*------------------------------------------------------------------------*/
#else // NCONTRACTS
/*------------------------------------------------------------------------*/
#define REQUIRE(...) \
do { \
} while (0)
#define REQUIRE_INITIALIZED() \
do { \
} while (0)
#define REQUIRE_VALID_STATE() \
do { \
} while (0)
#define REQUIRE_READY_STATE() \
do { \
} while (0)
#define REQUIRE_VALID_OR_SOLVING_STATE() \
do { \
} while (0)
#define REQUIRE_VALID_LIT(...) \
do { \
} while (0)
#define REQUIRE_STEADY_STATE() \
do { \
} while (0)
/*------------------------------------------------------------------------*/
#endif
/*------------------------------------------------------------------------*/
#endif