forked from vprover/vampire
-
Notifications
You must be signed in to change notification settings - Fork 0
/
MinisatInterfacing.hpp
167 lines (138 loc) · 5.05 KB
/
MinisatInterfacing.hpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
/*
* File MinisatInterfacing.hpp.
*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*
* In summary, you are allowed to use Vampire for non-commercial
* purposes but not allowed to distribute, modify, copy, create derivatives,
* or use in competitions.
* For other uses of Vampire please contact developers for a different
* licence, which we will make an effort to provide.
*/
/**
* @file MinisatInterfacing.hpp
* Defines class MinisatInterfacing
*/
#ifndef __MinisatInterfacing__
#define __MinisatInterfacing__
#include "SATSolver.hpp"
#include "SATLiteral.hpp"
#include "SATClause.hpp"
#include "Minisat/core/Solver.h"
namespace SAT{
class MinisatInterfacing : public PrimitiveProofRecordingSATSolver
{
public:
CLASS_NAME(MinisatInterfacing);
USE_ALLOCATOR(MinisatInterfacing);
MinisatInterfacing(const Shell::Options& opts, bool generateProofs=false);
/**
* Can be called only when all assumptions are retracted
*
* A requirement is that in a clause, each variable occurs at most once.
*/
virtual void addClause(SATClause* cl) override;
/**
* Opportunity to perform in-processing of the clause database.
*
* (Minisat deletes unconditionally satisfied clauses.)
*/
virtual void simplify() override {
CALL("MinisatInterfacing::simplify");
_solver.simplify();
}
virtual Status solve(unsigned conflictCountLimit) override;
/**
* If status is @c SATISFIABLE, return assignment of variable @c var
*/
virtual VarAssignment getAssignment(unsigned var) override;
/**
* If status is @c SATISFIABLE, return 0 if the assignment of @c var is
* implied only by unit propagation (i.e. does not depend on any decisions)
*/
virtual bool isZeroImplied(unsigned var) override;
/**
* Collect zero-implied literals.
*
* Can be used in SATISFIABLE and UNKNOWN state.
*
* @see isZeroImplied()
*/
virtual void collectZeroImplied(SATLiteralStack& acc) override;
/**
* Return a valid clause that contains the zero-implied literal
* and possibly the assumptions that implied it. Return 0 if @c var
* was an assumption itself.
* If called on a proof producing solver, the clause will have
* a proper proof history.
*/
virtual SATClause* getZeroImpliedCertificate(unsigned var) override;
virtual void ensureVarCount(unsigned newVarCnt) override;
virtual unsigned newVar() override;
virtual void suggestPolarity(unsigned var, unsigned pol) override {
// 0 -> true which means negated, e.g. false in the model
bool mpol = pol ? false : true;
_solver.suggestPolarity(vampireVar2Minisat(var),mpol);
}
/**
* Add an assumption into the solver.
*/
virtual void addAssumption(SATLiteral lit) override;
virtual void retractAllAssumptions() override {
_assumptions.clear();
_status = UNKNOWN;
};
virtual bool hasAssumptions() const override {
return (_assumptions.size() > 0);
};
/**
* Record the association between a SATLiteral var and a Literal
* In TWLSolver this is used for computing niceness values
*/
virtual void recordSource(unsigned satlitvar, Literal* lit) override {
// unsupported by minisat; intentionally no-op
};
Status solveUnderAssumptions(const SATLiteralStack& assumps, unsigned conflictCountLimit, bool) override;
/**
* Use minisat and solving under assumptions to minimize the given set of premises (= unsat core extraction).
*
* Assumes @b premises in conjunction with @b assumps unsat.
* Returns a "small" subset of premises which is still unsat under assumps.
*/
static SATClauseList* minimizePremiseList(SATClauseList* premises, SATLiteralStack& assumps);
/**
* Assuming that @b first together with @b second is inconsistent,
* produce (in @b result) a set of clauses over the signature of @b first,
* such that @b second |= @b result and
* @b first together with @b result is also inconsistent.
*/
static void interpolateViaAssumptions(unsigned maxVar, const SATClauseStack& first, const SATClauseStack& second, SATClauseStack& result);
protected:
void solveModuloAssumptionsAndSetStatus(unsigned conflictCountLimit = UINT_MAX);
Minisat::Var vampireVar2Minisat(unsigned vvar) {
ASS_G(vvar,0); ASS_LE(vvar,(unsigned)_solver.nVars());
return (vvar-1);
}
unsigned minisatVar2Vampire(Minisat::Var mvar) {
return (unsigned)(mvar+1);
}
const Minisat::Lit vampireLit2Minisat(SATLiteral vlit) {
return Minisat::mkLit(vampireVar2Minisat(vlit.var()),vlit.isNegative());
}
/* sign=true in minisat means "negated" in vampire */
const SATLiteral minisatLit2Vampire(Minisat::Lit mlit) {
return SATLiteral(minisatVar2Vampire(Minisat::var(mlit)),Minisat::sign(mlit) ? 0 : 1);
}
private:
Status _status;
Minisat::vec<Minisat::Lit> _assumptions;
Minisat::Solver _solver;
};
}//end SAT namespace
#endif /*MinisatInterfacing*/