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 
19 {
20 public:
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 
31 {
32 public:
34 };
35 
37 {
38 public:
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