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
17
class
satcheck_zcoret
:
public
dimacs_cnft
18
{
19
public
:
20
satcheck_zcoret
();
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
solvers
sat
satcheck_zcore.h
Generated by
1.8.16