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  const std::string solver_text() override;
24  tvt l_get(literalt a) const override;
25 
26  bool is_in_core(literalt l) const
27  {
28  return in_core.find(l.var_no())!=in_core.end();
29  }
30 
31 protected:
32  resultt do_prop_solve() override;
33 
34  std::set<unsigned> in_core;
35 };
36 
37 #endif // CPROVER_SOLVERS_SAT_SATCHECK_ZCORE_H
var_not var_no() const
Definition: literal.h:83
tvt l_get(literalt a) const override
virtual ~satcheck_zcoret()
resultt do_prop_solve() override
bool is_in_core(literalt l) const
std::set< unsigned > in_core
const std::string solver_text() override
Definition: threeval.h:20
resultt
The result of goto verifying.
Definition: properties.h:45