cprover
satcheck_picosat.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_PICOSAT_H
11 #define CPROVER_SOLVERS_SAT_SATCHECK_PICOSAT_H
12 
13 #include "cnf.h"
14 
15 // NOLINTNEXTLINE(readability/identifiers)
16 struct PicoSAT;
17 
19 {
20 public:
23 
24  virtual const std::string solver_text();
25  virtual resultt prop_solve();
26  virtual tvt l_get(literalt a) const;
27 
28  virtual void lcnf(const bvt &bv);
29  virtual void set_assignment(literalt a, bool value);
30 
31  virtual bool is_in_conflict(literalt a) const;
32  virtual void set_assumptions(const bvt &_assumptions);
33  virtual bool has_set_assumptions() const { return true; }
34  virtual bool has_is_in_conflict() const { return true; }
35 
36 protected:
38 
39 private:
40  PicoSAT *picosat;
41 };
42 
43 #endif // CPROVER_SOLVERS_SAT_SATCHECK_PICOSAT_H
CNF Generation, via Tseitin.
virtual void set_assumptions(const bvt &_assumptions)
virtual bool has_is_in_conflict() const
virtual const std::string solver_text()
Definition: threeval.h:19
resultt
Definition: prop.h:96
virtual tvt l_get(literalt a) const
virtual resultt prop_solve()
virtual bool is_in_conflict(literalt a) const
virtual void lcnf(const bvt &bv)
virtual bool has_set_assumptions() const
virtual void set_assignment(literalt a, bool value)
std::vector< literalt > bvt
Definition: literal.h:200