cprover
satcheck_lingeling.cpp
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 #include "satcheck_lingeling.h"
10 
11 #include <cassert>
12 
13 #include <util/threeval.h>
14 
15 extern "C"
16 {
17 #include <lglib.h>
18 }
19 
20 #ifndef HAVE_LINGELING
21 #error "Expected HAVE_LINGELING"
22 #endif
23 
25 {
26  if(a.is_constant())
27  return tvt(a.sign());
28 
29  tvt result;
30 
31  if(a.var_no()>lglmaxvar(solver))
33 
34  const int val=lglderef(solver, a.dimacs());
35  if(val>0)
36  result=tvt(true);
37  else if(val<0)
38  result=tvt(false);
39  else
41 
42  return result;
43 }
44 
46 {
47  return "Lingeling";
48 }
49 
51 {
52  bvt new_bv;
53 
54  if(process_clause(bv, new_bv))
55  return;
56 
57  forall_literals(it, new_bv)
58  lgladd(solver, it->dimacs());
59 
60  lgladd(solver, 0);
61 
63 }
64 
66 {
67  assert(status!=ERROR);
68 
69  // We start counting at 1, thus there is one variable fewer.
70  {
71  std::string msg=
72  std::to_string(no_variables()-1)+" variables, "+
73  std::to_string(clause_counter)+" clauses";
74  messaget::status() << msg << messaget::eom;
75  }
76 
77  std::string msg;
78 
80  lglassume(solver, it->dimacs());
81 
82  const int res=lglsat(solver);
83  if(res==10)
84  {
85  msg="SAT checker: instance is SATISFIABLE";
86  messaget::status() << msg << messaget::eom;
87  status=SAT;
88  return P_SATISFIABLE;
89  }
90  else
91  {
92  assert(res==20);
93  msg="SAT checker: instance is UNSATISFIABLE";
94  messaget::status() << msg << messaget::eom;
95  }
96 
97  status=UNSAT;
98  return P_UNSATISFIABLE;
99 }
100 
102 {
103  assert(false);
104 }
105 
107  solver(lglinit())
108 {
109 }
110 
112 {
113  lglrelease(solver);
114  solver=0;
115 }
116 
118 {
119  assumptions=bv;
120 
122  assert(!it->is_constant());
123 }
124 
126 {
127  if(!a.is_constant())
128  lglfreeze(solver, a.dimacs());
129 }
130 
136 {
137  assert(!a.is_constant());
138  return lglfailed(solver, a.dimacs())!=0;
139 }
mstreamt & result()
Definition: message.h:233
size_t clause_counter
Definition: cnf.h:81
mstreamt & status()
Definition: message.h:238
bool process_clause(const bvt &bv, bvt &dest)
filter &#39;true&#39; from clause, eliminate duplicates, recognise trivially satisfied clauses ...
Definition: cnf.cpp:416
int dimacs() const
Definition: literal.h:116
virtual void lcnf(const bvt &bv)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
#define forall_literals(it, bv)
Definition: literal.h:199
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)
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
virtual bool is_in_conflict(literalt a) const
Returns true if an assumed literal is in conflict if the formula is UNSAT.
bool is_constant() const
Definition: literal.h:165
bool sign() const
Definition: literal.h:87
virtual void set_assignment(literalt a, bool value)
virtual tvt l_get(literalt a) const
virtual size_t no_variables() const override
Definition: cnf.h:38
std::vector< literalt > bvt
Definition: literal.h:197