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 <algorithm>
12 
13 #include <util/invariant.h>
14 #include <util/threeval.h>
15 
16 extern "C"
17 {
18 #include <lglib.h>
19 }
20 
21 #ifndef HAVE_LINGELING
22 #error "Expected HAVE_LINGELING"
23 #endif
24 
26 {
27  if(a.is_constant())
28  return tvt(a.sign());
29 
30  tvt result;
31 
32  if(a.var_no()>lglmaxvar(solver))
34 
35  const int val=lglderef(solver, a.dimacs());
36  if(val>0)
37  result=tvt(true);
38  else if(val<0)
39  result=tvt(false);
40  else
42 
43  return result;
44 }
45 
47 {
48  return "Lingeling";
49 }
50 
52 {
53  bvt new_bv;
54 
55  if(process_clause(bv, new_bv))
56  return;
57 
58  forall_literals(it, new_bv)
59  lgladd(solver, it->dimacs());
60 
61  lgladd(solver, 0);
62 
64 }
65 
67 {
68  PRECONDITION(status != ERROR);
69 
70  // We start counting at 1, thus there is one variable fewer.
71  {
72  std::string msg=
73  std::to_string(no_variables()-1)+" variables, "+
74  std::to_string(clause_counter)+" clauses";
75  messaget::status() << msg << messaget::eom;
76  }
77 
78  std::string msg;
79 
81  lglassume(solver, it->dimacs());
82 
83  const int res=lglsat(solver);
84  CHECK_RETURN(res == 10 || res == 20);
85 
86  if(res==10)
87  {
88  msg="SAT checker: instance is SATISFIABLE";
89  messaget::status() << msg << messaget::eom;
90  status=SAT;
91  return P_SATISFIABLE;
92  }
93  else
94  {
95  INVARIANT(res == 20, "result value is either 10 or 20");
96  msg="SAT checker: instance is UNSATISFIABLE";
97  messaget::status() << msg << messaget::eom;
98  }
99 
100  status=UNSAT;
101  return P_UNSATISFIABLE;
102 }
103 
105 {
106  UNREACHABLE;
107 }
108 
110  solver(lglinit())
111 {
112 }
113 
115 {
116  lglrelease(solver);
117  solver=0;
118 }
119 
121 {
122  assumptions=bv;
123 
124  INVARIANT(
125  std::all_of(
126  assumptions.begin(),
127  assumptions.end(),
128  [](const literalt &l) { return !l.is_constant(); }),
129  "assumptions should be non-constant");
130 }
131 
133 {
134  if(!a.is_constant())
135  lglfreeze(solver, a.dimacs());
136 }
137 
143 {
145  return lglfailed(solver, a.dimacs())!=0;
146 }
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
satcheck_lingelingt::set_frozen
virtual void set_frozen(literalt a)
Definition: satcheck_lingeling.cpp:132
cnft::process_clause
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:416
bvt
std::vector< literalt > bvt
Definition: literal.h:200
threeval.h
messaget::status
mstreamt & status() const
Definition: message.h:401
literalt::dimacs
int dimacs() const
Definition: literal.h:116
satcheck_lingelingt::assumptions
bvt assumptions
Definition: satcheck_lingeling.h:40
invariant.h
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
messaget::eom
static eomt eom
Definition: message.h:284
literalt::var_no
var_not var_no() const
Definition: literal.h:82
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
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:202
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
messaget::result
mstreamt & result() const
Definition: message.h:396
cnf_solvert::status
statust status
Definition: cnf.h:80
satcheck_lingeling.h
satcheck_lingelingt::l_get
virtual tvt l_get(literalt a) const
Definition: satcheck_lingeling.cpp:25
cnf_solvert::clause_counter
size_t clause_counter
Definition: cnf.h:81
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
literalt::sign
bool sign() const
Definition: literal.h:87
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:360
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
tvt::tv_enumt::TV_UNKNOWN
@ TV_UNKNOWN
satcheck_lingelingt::set_assumptions
virtual void set_assumptions(const bvt &_assumptions)
Definition: satcheck_lingeling.cpp:120
literalt::is_constant
bool is_constant() const
Definition: literal.h:165
cnft::no_variables
virtual size_t no_variables() const override
Definition: cnf.h:38
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
validation_modet::INVARIANT
@ INVARIANT
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470