cprover
satcheck_zcore.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_ZCORE_H
11 #define CPROVER_SOLVERS_SAT_SATCHECK_ZCORE_H
12 
13 #include <set>
14 
15 #include "dimacs_cnf.h"
16 
18 {
19 public:
21  virtual ~satcheck_zcoret();
22 
23  virtual const std::string solver_text();
24  virtual resultt prop_solve();
25  virtual tvt l_get(literalt a) const;
26 
27  bool is_in_core(literalt l) const
28  {
29  return in_core.find(l.var_no())!=in_core.end();
30  }
31 
32 protected:
33  std::set<unsigned> in_core;
34 };
35 
36 #endif // CPROVER_SOLVERS_SAT_SATCHECK_ZCORE_H
virtual resultt prop_solve()
virtual const std::string solver_text()
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
std::set< unsigned > in_core
virtual ~satcheck_zcoret()
resultt
Definition: prop.h:96
virtual tvt l_get(literalt a) const
bool is_in_core(literalt l) const