cprover
Loading...
Searching...
No Matches
satcheck_picosat.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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)
16struct PicoSAT;
17
19{
20public:
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
41protected:
42 resultt do_prop_solve() override;
43
45
46private:
48};
49
50#endif // CPROVER_SOLVERS_SAT_SATCHECK_PICOSAT_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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:45