cprover
satcheck_zchaff.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_ZCHAFF_H
11 #define CPROVER_SOLVERS_SAT_SATCHECK_ZCHAFF_H
12 
13 #include "cnf_clause_list.h"
14 
15 // use this only if you want to have something
16 // derived from CSolver
17 // otherwise, use satcheck_zchafft
18 // NOLINTNEXTLINE(readability/identifiers)
19 class CSolver;
20 
22 {
23 public:
24  explicit satcheck_zchaff_baset(CSolver *_solver);
25  virtual ~satcheck_zchaff_baset();
26 
27  virtual const std::string solver_text();
28  virtual resultt prop_solve();
29  virtual tvt l_get(literalt a) const;
30  virtual void set_assignment(literalt a, bool value);
31  virtual void copy_cnf();
32 
33  CSolver *zchaff_solver()
34  {
35  return solver;
36  }
37 
38 protected:
39  CSolver *solver;
40 
41  enum statust { INIT, SAT, UNSAT, ERROR };
43 };
44 
46 {
47  public:
49  virtual ~satcheck_zchafft();
50 };
51 
52 #endif // CPROVER_SOLVERS_SAT_SATCHECK_ZCHAFF_H
satcheck_zchafft::satcheck_zchafft
satcheck_zchafft()
Definition: satcheck_zchaff.cpp:169
satcheck_zchaff_baset::copy_cnf
virtual void copy_cnf()
Definition: satcheck_zchaff.cpp:59
satcheck_zchaff_baset::INIT
Definition: satcheck_zchaff.h:41
cnf_clause_listt
Definition: cnf_clause_list.h:23
satcheck_zchaff_baset::UNSAT
Definition: satcheck_zchaff.h:41
cnf_clause_list.h
satcheck_zchaff_baset::satcheck_zchaff_baset
satcheck_zchaff_baset(CSolver *_solver)
Definition: satcheck_zchaff.cpp:15
satcheck_zchaff_baset::set_assignment
virtual void set_assignment(literalt a, bool value)
Definition: satcheck_zchaff.cpp:161
satcheck_zchaff_baset::~satcheck_zchaff_baset
virtual ~satcheck_zchaff_baset()
Definition: satcheck_zchaff.cpp:22
satcheck_zchaff_baset::prop_solve
virtual resultt prop_solve()
Definition: satcheck_zchaff.cpp:73
propt::resultt
resultt
Definition: prop.h:96
satcheck_zchafft::~satcheck_zchafft
virtual ~satcheck_zchafft()
Definition: satcheck_zchaff.cpp:174
satcheck_zchaff_baset::status
statust status
Definition: satcheck_zchaff.h:42
satcheck_zchaff_baset::statust
statust
Definition: satcheck_zchaff.h:41
tvt
Definition: threeval.h:19
satcheck_zchaff_baset::l_get
virtual tvt l_get(literalt a) const
Definition: satcheck_zchaff.cpp:26
satcheck_zchaff_baset
Definition: satcheck_zchaff.h:21
literalt
Definition: literal.h:24
satcheck_zchafft
Definition: satcheck_zchaff.h:45
satcheck_zchaff_baset::ERROR
Definition: satcheck_zchaff.h:41
satcheck_zchaff_baset::solver_text
virtual const std::string solver_text()
Definition: satcheck_zchaff.cpp:54
satcheck_zchaff_baset::zchaff_solver
CSolver * zchaff_solver()
Definition: satcheck_zchaff.h:33
satcheck_zchaff_baset::SAT
Definition: satcheck_zchaff.h:41
satcheck_zchaff_baset::solver
CSolver * solver
Definition: satcheck_zchaff.h:39