cprover
Loading...
Searching...
No Matches
satcheck.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_SOLVERS_SAT_SATCHECK_H
11#define CPROVER_SOLVERS_SAT_SATCHECK_H
12
13// This sets a define for the SAT solver
14// based on set flags that come via the compiler
15// command line.
16
17// #define SATCHECK_ZCHAFF
18// #define SATCHECK_MINISAT1
19// #define SATCHECK_MINISAT2
20// #define SATCHECK_GLUCOSE
21// #define SATCHECK_BOOLEFORCE
22// #define SATCHECK_PICOSAT
23// #define SATCHECK_LINGELING
24// #define SATCHECK_CADICAL
25
26#if defined(HAVE_IPASIR) && !defined(SATCHECK_IPASIR)
27#define SATCHECK_IPASIR
28#endif
29
30#if defined(HAVE_ZCHAFF) && !defined(SATCHECK_ZCHAFF)
31#define SATCHECK_ZCHAFF
32#endif
33
34#if defined(HAVE_MINISAT1) && !defined(SATCHECK_MINISAT1)
35#define SATCHECK_MINISAT1
36#endif
37
38#if defined(HAVE_MINISAT2) && !defined(SATCHECK_MINISAT2)
39#define SATCHECK_MINISAT2
40#endif
41
42#if defined(HAVE_GLUCOSE) && !defined(SATCHECK_GLUCOSE)
43#define SATCHECK_GLUCOSE
44#endif
45
46#if defined(HAVE_BOOLEFORCE) && !defined(SATCHECK_BOOLEFORCE)
47#define SATCHECK_BOOLEFORCE
48#endif
49
50#if defined(HAVE_PICOSAT) && !defined(SATCHECK_PICOSAT)
51#define SATCHECK_PICOSAT
52#endif
53
54#if defined(HAVE_LINGELING) && !defined(SATCHECK_LINGELING)
55#define SATCHECK_LINGELING
56#endif
57
58#if defined(HAVE_CADICAL) && !defined(SATCHECK_CADICAL)
59#define SATCHECK_CADICAL
60#endif
61
62#if defined SATCHECK_ZCHAFF
63
64#include "satcheck_zchaff.h"
65
68
69#elif defined SATCHECK_BOOLEFORCE
70
71#include "satcheck_booleforce.h"
72
75
76#elif defined SATCHECK_MINISAT1
77
78#include "satcheck_minisat.h"
79
82
83#elif defined SATCHECK_MINISAT2
84
85#include "satcheck_minisat2.h"
86
89
90#elif defined SATCHECK_IPASIR
91
92#include "satcheck_ipasir.h"
93
96
97#elif defined SATCHECK_PICOSAT
98
99#include "satcheck_picosat.h"
100
103
104#elif defined SATCHECK_LINGELING
105
106#include "satcheck_lingeling.h"
107
110
111#elif defined SATCHECK_GLUCOSE
112
113#include "satcheck_glucose.h"
114
117
118#elif defined SATCHECK_CADICAL
119
120#include "satcheck_cadical.h"
121
124
125#endif
126
127#endif // CPROVER_SOLVERS_SAT_SATCHECK_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Interface for generic SAT solver interface IPASIR.