cprover
satcheck_lingeling.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6
7\*******************************************************************/
8
10
11#include <algorithm>
12
13#include <util/invariant.h>
14#include <util/threeval.h>
15
16extern "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 for(const auto &literal : new_bv)
59 lgladd(solver, literal.dimacs());
60
61 lgladd(solver, 0);
62
64}
65
67{
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, "+
75 log.statistics() << msg << messaget::eom;
76 }
77
78 std::string msg;
79
80 for(const auto &literal : assumptions)
81 lglassume(solver, literal.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 log.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 log.status() << msg << messaget::eom;
98 }
99
100 status=UNSAT;
101 return P_UNSATISFIABLE;
102}
103
105{
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}
statust status
Definition: cnf.h:87
size_t clause_counter
Definition: cnf.h:88
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:425
virtual size_t no_variables() const override
Definition: cnf.h:42
bool sign() const
Definition: literal.h:88
bool is_constant() const
Definition: literal.h:166
int dimacs() const
Definition: literal.h:117
var_not var_no() const
Definition: literal.h:83
mstreamt & statistics() const
Definition: message.h:419
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
resultt
Definition: prop.h:97
messaget log
Definition: prop.h:128
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
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
std::vector< literalt > bvt
Definition: literal.h:201
@ ERROR
An error occurred during goto checking.
int solver(std::istream &in)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.