cprover
qbf_skizzo_core.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 {
18 public:
20  virtual ~qbf_skizzo_coret();
21 
22  virtual const std::string solver_text();
23  virtual resultt prop_solve();
24 
25  virtual bool is_in_core(literalt l) const;
26  virtual modeltypet m_get(literalt a) const;
27 
28 protected:
29  std::string qbf_tmp_file;
30 
31  bool get_certificate(void);
32 };
33 
34 #endif // CPROVER_SOLVERS_QBF_QBF_SKIZZO_CORE_H
resultt
Definition: prop.h:99
bool get_certificate(void)
virtual const std::string solver_text()
std::string qbf_tmp_file
virtual modeltypet m_get(literalt a) const
virtual bool is_in_core(literalt l) const
virtual resultt prop_solve()
virtual ~qbf_skizzo_coret()