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
virtual const std::string solver_text()
satcheck_zchaff_baset(CSolver *_solver)
CNF Generation.
virtual void set_assignment(literalt a, bool value)
Definition: threeval.h:19
resultt
Definition: prop.h:94
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
virtual ~satcheck_zchafft()