CBMC
qbf_core.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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"
23 typedef qbf_squolem_coret qbf_coret;
24 
25 #else
26 #ifdef QBF_CORE_SKIZZO
27 
28 #include "qbf_skizzo_core.h"
29 typedef qbf_skizzo_coret qbf_coret;
30 
31 #else
32 #ifdef QBF_CORE_BDD
33 
34 #include "qbf_bdd_core.h"
35 typedef qbf_bdd_coret qbf_coret;
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
Squolem Backend (with Proofs)