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
satcheck_picosatt::l_get
virtual tvt l_get(literalt a) const
Definition: satcheck_picosat.cpp:25
satcheck_picosatt::is_in_conflict
virtual bool is_in_conflict(literalt a) const
Returns true if an assumption is in the final conflict.
Definition: satcheck_picosat.cpp:120
satcheck_picosatt::set_assignment
virtual void set_assignment(literalt a, bool value)
Definition: satcheck_picosat.cpp:105
bvt
std::vector< literalt > bvt
Definition: literal.h:200
satcheck_picosatt::has_set_assumptions
virtual bool has_set_assumptions() const
Definition: satcheck_picosat.h:33
satcheck_picosatt::set_assumptions
virtual void set_assumptions(const bvt &_assumptions)
Definition: satcheck_picosat.cpp:127
satcheck_picosatt::lcnf
virtual void lcnf(const bvt &bv)
Definition: satcheck_picosat.cpp:51
cnf_solvert
Definition: cnf.h:66
satcheck_picosatt::prop_solve
virtual resultt prop_solve()
Definition: satcheck_picosat.cpp:68
propt::resultt
resultt
Definition: prop.h:96
satcheck_picosatt::picosat
PicoSAT * picosat
Definition: satcheck_picosat.h:40
tvt
Definition: threeval.h:19
satcheck_picosatt::assumptions
bvt assumptions
Definition: satcheck_picosat.h:37
satcheck_picosatt::solver_text
virtual const std::string solver_text()
Definition: satcheck_picosat.cpp:46
literalt
Definition: literal.h:24
satcheck_picosatt
Definition: satcheck_picosat.h:18
satcheck_picosatt::~satcheck_picosatt
~satcheck_picosatt()
Definition: satcheck_picosat.cpp:115
cnf.h
satcheck_picosatt::satcheck_picosatt
satcheck_picosatt()
Definition: satcheck_picosat.cpp:110
satcheck_picosatt::has_is_in_conflict
virtual bool has_is_in_conflict() const
Definition: satcheck_picosat.h:34