cprover
Loading...
Searching...
No Matches
satcheck_zcore.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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{
19public:
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
31protected:
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