cprover
Loading...
Searching...
No Matches
satcheck_picosat.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6
7\*******************************************************************/
8
9#include "satcheck_picosat.h"
10
11#include <algorithm>
12
13#include <util/invariant.h>
14#include <util/threeval.h>
15
16extern "C"
17{
18#include <picosat.h>
19}
20
21#ifndef HAVE_PICOSAT
22#error "Expected HAVE_PICOSAT"
23#endif
24
26{
27 if(a.is_constant())
28 return tvt(a.sign());
29
30 tvt result;
31
32 if(static_cast<int>(a.var_no())>picosat_variables(picosat))
34
35 const int val=picosat_deref(picosat, 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 "PicoSAT";
49}
50
52{
53 bvt new_bv;
54
55 if(process_clause(bv, new_bv))
56 return;
57
59
60 for(const auto &literal : new_bv)
61 picosat_add(picosat, literal.dimacs());
62
64
66}
67
69{
71
72 {
73 std::string msg=
74 std::to_string(_no_variables-1)+" variables, "+
75 std::to_string(picosat_added_original_clauses(picosat))+" clauses";
76 log.statistics() << msg << messaget::eom;
77 }
78
79 std::string msg;
80
81 for(const auto &literal : assumptions)
83
84 const int res=picosat_sat(picosat, -1);
86 {
87 msg="SAT checker: instance is SATISFIABLE";
88 log.status() << msg << messaget::eom;
89 status=SAT;
90 return P_SATISFIABLE;
91 }
92 else
93 {
96 "picosat result should report either sat or unsat");
97 msg="SAT checker: instance is UNSATISFIABLE";
98 log.status() << msg << messaget::eom;
99 }
100
102 return P_UNSATISFIABLE;
103}
104
109
114
119
121{
122 PRECONDITION(!a.is_constant());
123
124 return picosat_failed_assumption(picosat, a.dimacs())!=0;
125}
126
128{
129 assumptions=bv;
130
131 INVARIANT(
132 std::all_of(
133 assumptions.begin(),
134 assumptions.end(),
135 [](const literalt &l) { return !l.is_constant(); }),
136 "assumptions should be non-constant");
137}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
size_t _no_variables
Definition cnf.h:57
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:98
messaget log
Definition prop.h:129
const std::string solver_text() override
resultt do_prop_solve() override
tvt l_get(literalt a) const override
void set_assignment(literalt a, bool value) override
void set_assumptions(const bvt &_assumptions) override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
void lcnf(const bvt &bv) override
Definition threeval.h:20
std::vector< literalt > bvt
Definition literal.h:201
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423