CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
qbf_skizzo_core.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: CM Wintersteiger
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_SOLVERS_QBF_QBF_SKIZZO_CORE_H
11#define CPROVER_SOLVERS_QBF_QBF_SKIZZO_CORE_H
12
13#include "qbf_bdd_core.h"
14
15// a qdimacs_coret with f_get from BDDs
17{
18public:
20 ~qbf_skizzo_coret() override;
21
22 std::string solver_text() const override;
23 resultt prop_solve() override;
24
25 bool is_in_core(literalt l) const override;
26 modeltypet m_get(literalt a) const override;
27
28protected:
29 std::string qbf_tmp_file;
30
31 bool get_certificate(void);
32};
33
34#endif // CPROVER_SOLVERS_QBF_QBF_SKIZZO_CORE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::string qbf_tmp_file
resultt prop_solve() override
std::string solver_text() const override
bool is_in_core(literalt l) const override
modeltypet m_get(literalt a) const override
~qbf_skizzo_coret() override
resultt
The result of goto verifying.
Definition properties.h:45