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
satcheck_zcoret::is_in_core
bool is_in_core(literalt l) const
Definition: satcheck_zcore.h:27
literalt::var_no
var_not var_no() const
Definition: literal.h:82
satcheck_zcoret::in_core
std::set< unsigned > in_core
Definition: satcheck_zcore.h:33
satcheck_zcoret::~satcheck_zcoret
virtual ~satcheck_zcoret()
Definition: satcheck_zcore.cpp:22
satcheck_zcoret::solver_text
virtual const std::string solver_text()
Definition: satcheck_zcore.cpp:32
propt::resultt
resultt
Definition: prop.h:96
tvt
Definition: threeval.h:19
satcheck_zcoret::satcheck_zcoret
satcheck_zcoret()
Definition: satcheck_zcore.cpp:18
dimacs_cnf.h
literalt
Definition: literal.h:24
satcheck_zcoret
Definition: satcheck_zcore.h:17
satcheck_zcoret::prop_solve
virtual resultt prop_solve()
Definition: satcheck_zcore.cpp:37
satcheck_zcoret::l_get
virtual tvt l_get(literalt a) const
Definition: satcheck_zcore.cpp:26
dimacs_cnft
Definition: dimacs_cnf.h:17