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  const std::string solver_text() override;
25  tvt l_get(literalt a) const override;
26 
27  void lcnf(const bvt &bv) override;
28  void set_assignment(literalt a, bool value) override;
29 
30  bool is_in_conflict(literalt a) const override;
31  void set_assumptions(const bvt &_assumptions) override;
32  bool has_set_assumptions() const override
33  {
34  return true;
35  }
36  bool has_is_in_conflict() const override
37  {
38  return true;
39  }
40 
41 protected:
42  resultt do_prop_solve() override;
43 
45 
46 private:
47  PicoSAT *picosat;
48 };
49 
50 #endif // CPROVER_SOLVERS_SAT_SATCHECK_PICOSAT_H
const std::string solver_text() override
resultt do_prop_solve() override
tvt l_get(literalt a) const override
void set_assignment(literalt a, bool value) override
void set_assumptions(const bvt &_assumptions) override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
void lcnf(const bvt &bv) override
bool has_is_in_conflict() const override
bool has_set_assumptions() const override
Definition: threeval.h:20
CNF Generation, via Tseitin.
std::vector< literalt > bvt
Definition: literal.h:201
resultt
The result of goto verifying.
Definition: properties.h:44