cprover
Loading...
Searching...
No Matches
satcheck_lingeling.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_LINGELING_H
11#define CPROVER_SOLVERS_SAT_SATCHECK_LINGELING_H
12
13#include "cnf.h"
14
15// NOLINTNEXTLINE(readability/identifiers)
16struct LGL;
17
19{
20public:
22 virtual ~satcheck_lingelingt();
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 void set_assumptions(const bvt &_assumptions) override;
31 bool has_set_assumptions() const override
32 {
33 return true;
34 }
35 bool has_is_in_conflict() const override
36 {
37 return true;
38 }
39 bool is_in_conflict(literalt a) const override;
40 void set_frozen(literalt a) override;
41
42protected:
43 resultt do_prop_solve() override;
44
45 // NOLINTNEXTLINE(readability/identifiers)
46 struct LGL * solver;
48};
49
50#endif // CPROVER_SOLVERS_SAT_SATCHECK_LINGELING_H
bool has_is_in_conflict() const override
void set_assumptions(const bvt &_assumptions) override
const std::string solver_text() override
void lcnf(const bvt &bv) override
tvt l_get(literalt a) const override
resultt do_prop_solve() override
void set_assignment(literalt a, bool value) override
bool has_set_assumptions() const override
void set_frozen(literalt a) override
bool is_in_conflict(literalt a) const override
Returns true if an assumed literal is in conflict if the formula is UNSAT.
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