CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
qbf_core.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com,
6 CM Wintersteiger
7
8\*******************************************************************/
9
10
11#ifndef CPROVER_SOLVERS_QBF_QBF_CORE_H
12#define CPROVER_SOLVERS_QBF_QBF_CORE_H
13
14#ifdef HAVE_QBF_CORE
15#define QBF_CORE_SKIZZO
16#else
17#define QBF_CORE_NONE
18#endif
19
20#ifdef QBF_CORE_SQUOLEM
21
22#include "qbf_squolem_core.h"
24
25#else
26#ifdef QBF_CORE_SKIZZO
27
28#include "qbf_skizzo_core.h"
30
31#else
32#ifdef QBF_CORE_BDD
33
34#include "qbf_bdd_core.h"
36
37#else
38
39#error NO QBF SOLVER WITH CORE EXTRACTOR
40#endif
41#endif
42#endif
43
44#endif // CPROVER_SOLVERS_QBF_QBF_CORE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Squolem Backend (with Proofs)