cprover
satcheck_lingeling.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_LINGELING_H
11 #define CPROVER_SOLVERS_SAT_SATCHECK_LINGELING_H
12 
13 #include "cnf.h"
14 
15 // NOLINTNEXTLINE(readability/identifiers)
16 struct LGL;
17 
19 {
20 public:
22  virtual ~satcheck_lingelingt();
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 void set_assumptions(const bvt &_assumptions);
32  virtual bool has_set_assumptions() const { return true; }
33  virtual bool has_is_in_conflict() const { return true; }
34  virtual bool is_in_conflict(literalt a) const;
35  virtual void set_frozen(literalt a);
36 
37 protected:
38  // NOLINTNEXTLINE(readability/identifiers)
39  struct LGL * solver;
41 };
42 
43 #endif // CPROVER_SOLVERS_SAT_SATCHECK_LINGELING_H
satcheck_lingelingt::has_set_assumptions
virtual bool has_set_assumptions() const
Definition: satcheck_lingeling.h:32
satcheck_lingelingt::set_frozen
virtual void set_frozen(literalt a)
Definition: satcheck_lingeling.cpp:132
bvt
std::vector< literalt > bvt
Definition: literal.h:200
satcheck_lingelingt::assumptions
bvt assumptions
Definition: satcheck_lingeling.h:40
satcheck_lingelingt::set_assignment
virtual void set_assignment(literalt a, bool value)
Definition: satcheck_lingeling.cpp:104
satcheck_lingelingt::~satcheck_lingelingt
virtual ~satcheck_lingelingt()
Definition: satcheck_lingeling.cpp:114
satcheck_lingelingt::satcheck_lingelingt
satcheck_lingelingt()
Definition: satcheck_lingeling.cpp:109
cnf_solvert
Definition: cnf.h:66
satcheck_lingelingt::has_is_in_conflict
virtual bool has_is_in_conflict() const
Definition: satcheck_lingeling.h:33
satcheck_lingelingt::l_get
virtual tvt l_get(literalt a) const
Definition: satcheck_lingeling.cpp:25
propt::resultt
resultt
Definition: prop.h:96
satcheck_lingelingt::solver_text
virtual const std::string solver_text()
Definition: satcheck_lingeling.cpp:46
tvt
Definition: threeval.h:19
satcheck_lingelingt::prop_solve
virtual resultt prop_solve()
Definition: satcheck_lingeling.cpp:66
literalt
Definition: literal.h:24
satcheck_lingelingt::solver
struct LGL * solver
Definition: satcheck_lingeling.h:39
satcheck_lingelingt
Definition: satcheck_lingeling.h:18
satcheck_lingelingt::set_assumptions
virtual void set_assumptions(const bvt &_assumptions)
Definition: satcheck_lingeling.cpp:120
satcheck_lingelingt::lcnf
virtual void lcnf(const bvt &bv)
Definition: satcheck_lingeling.cpp:51
satcheck_lingelingt::is_in_conflict
virtual bool is_in_conflict(literalt a) const
Returns true if an assumed literal is in conflict if the formula is UNSAT.
Definition: satcheck_lingeling.cpp:142
cnf.h