cprover
satcheck_booleforce.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_BOOLEFORCE_H
11
#define CPROVER_SOLVERS_SAT_SATCHECK_BOOLEFORCE_H
12
13
#include <vector>
14
#include <set>
15
16
#include "
cnf.h
"
17
18
class
satcheck_booleforce_baset
:
public
cnf_solvert
19
{
20
public
:
21
virtual
~satcheck_booleforce_baset
();
22
23
virtual
const
std::string
solver_text
();
24
virtual
resultt
prop_solve
();
25
virtual
tvt
l_get
(
literalt
a)
const
;
26
27
virtual
void
lcnf
(
const
bvt
&bv);
28
};
29
30
class
satcheck_booleforcet
:
public
satcheck_booleforce_baset
31
{
32
public
:
33
satcheck_booleforcet
();
34
};
35
36
class
satcheck_booleforce_coret
:
public
satcheck_booleforce_baset
37
{
38
public
:
39
satcheck_booleforce_coret
();
40
41
bool
is_in_core
(
literalt
l)
const
;
42
};
43
44
#endif // CPROVER_SOLVERS_SAT_SATCHECK_BOOLEFORCE_H
bvt
std::vector< literalt > bvt
Definition:
literal.h:200
satcheck_booleforce_baset::prop_solve
virtual resultt prop_solve()
Definition:
satcheck_booleforce.cpp:82
satcheck_booleforce_baset::lcnf
virtual void lcnf(const bvt &bv)
Definition:
satcheck_booleforce.cpp:66
satcheck_booleforce_coret::is_in_core
bool is_in_core(literalt l) const
Definition:
satcheck_booleforce.cpp:126
cnf_solvert
Definition:
cnf.h:66
propt::resultt
resultt
Definition:
prop.h:96
satcheck_booleforce_baset::l_get
virtual tvt l_get(literalt a) const
Definition:
satcheck_booleforce.cpp:33
satcheck_booleforcet::satcheck_booleforcet
satcheck_booleforcet()
Definition:
satcheck_booleforce.cpp:18
tvt
Definition:
threeval.h:19
satcheck_booleforce_coret::satcheck_booleforce_coret
satcheck_booleforce_coret()
Definition:
satcheck_booleforce.cpp:23
satcheck_booleforce_coret
Definition:
satcheck_booleforce.h:36
satcheck_booleforce_baset
Definition:
satcheck_booleforce.h:18
literalt
Definition:
literal.h:24
cnf.h
satcheck_booleforcet
Definition:
satcheck_booleforce.h:30
satcheck_booleforce_baset::solver_text
virtual const std::string solver_text()
Definition:
satcheck_booleforce.cpp:61
satcheck_booleforce_baset::~satcheck_booleforce_baset
virtual ~satcheck_booleforce_baset()
Definition:
satcheck_booleforce.cpp:28
solvers
sat
satcheck_booleforce.h
Generated by
1.8.16