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
CNF Generation, via Tseitin.
virtual bool has_is_in_conflict() const
virtual void lcnf(const bvt &bv)
virtual bool has_set_assumptions() const
virtual void set_frozen(literalt a)
virtual resultt prop_solve()
virtual const std::string solver_text()
Definition: threeval.h:19
virtual void set_assumptions(const bvt &_assumptions)
resultt
Definition: prop.h:96
virtual bool is_in_conflict(literalt a) const
Returns true if an assumed literal is in conflict if the formula is UNSAT.
virtual void set_assignment(literalt a, bool value)
virtual tvt l_get(literalt a) const
std::vector< literalt > bvt
Definition: literal.h:200