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
CNF Generation, via Tseitin.
bool is_in_core(literalt l) const
virtual void lcnf(const bvt &bv)
virtual const std::string solver_text()
Definition: threeval.h:19
resultt
Definition: prop.h:94
virtual tvt l_get(literalt a) const
std::vector< literalt > bvt
Definition: literal.h:197