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
|
/******************************************************************************
* Top contributors (to current version):
* Mathias Preiner, Haniel Barbosa, Liana Hadarean
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* SAT Solver.
*
* Implementation of the minisat interface for cvc5.
*/
#pragma once
#include "prop/sat_solver.h"
#include "prop/minisat/simp/SimpSolver.h"
#include "util/statistics_registry.h"
namespace cvc5 {
template <class Solver>
prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
template <class Solver>
void toSatClause(const typename Solver::TClause& minisat_cl,
prop::SatClause& sat_cl);
namespace prop {
class MinisatSatSolver : public CDCLTSatSolverInterface
{
public:
MinisatSatSolver(StatisticsRegistry& registry);
~MinisatSatSolver() override;
static SatVariable toSatVariable(Minisat::Var var);
static Minisat::Lit toMinisatLit(SatLiteral lit);
static SatLiteral toSatLiteral(Minisat::Lit lit);
static SatValue toSatLiteralValue(Minisat::lbool res);
static Minisat::lbool toMinisatlbool(SatValue val);
//(Commented because not in use) static bool tobool(SatValue val);
static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause);
void initialize(context::Context* context,
TheoryProxy* theoryProxy,
cvc5::context::UserContext* userContext,
ProofNodeManager* pnm) override;
ClauseId addClause(SatClause& clause, bool removable) override;
ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
{
Unreachable() << "Minisat does not support native XOR reasoning";
}
SatVariable newVar(bool isTheoryAtom,
bool preRegister,
bool canErase) override;
SatVariable trueVar() override { return d_minisat->trueVar(); }
SatVariable falseVar() override { return d_minisat->falseVar(); }
SatValue solve() override;
SatValue solve(long unsigned int&) override;
SatValue solve(const std::vector<SatLiteral>& assumptions) override;
void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions) override;
bool ok() const override;
void interrupt() override;
SatValue value(SatLiteral l) override;
SatValue modelValue(SatLiteral l) override;
bool properExplanation(SatLiteral lit, SatLiteral expl) const override;
/** Incremental interface */
unsigned getAssertionLevel() const override;
void push() override;
void pop() override;
void resetTrail() override;
void requirePhase(SatLiteral lit) override;
bool isDecision(SatVariable decn) const override;
int32_t getDecisionLevel(SatVariable v) const override;
int32_t getIntroLevel(SatVariable v) const override;
/** Retrieve a pointer to the unerlying solver. */
Minisat::SimpSolver* getSolver() { return d_minisat; }
/** Retrieve the proof manager of this SAT solver. */
SatProofManager* getProofManager();
/** Retrieve the refutation proof of this SAT solver. */
std::shared_ptr<ProofNode> getProof() override;
private:
/** The SatSolver used */
Minisat::SimpSolver* d_minisat;
/** Context we will be using to synchronize the sat solver */
context::Context* d_context;
/**
* Stores assumptions passed via last solve() call.
*
* It is used in getUnsatAssumptions() to determine which of the literals in
* the final conflict clause are assumptions.
*/
std::unordered_set<SatLiteral, SatLiteralHashFunction> d_assumptions;
void setupOptions();
class Statistics {
private:
ReferenceStat<int64_t> d_statStarts, d_statDecisions;
ReferenceStat<int64_t> d_statRndDecisions, d_statPropagations;
ReferenceStat<int64_t> d_statConflicts, d_statClausesLiterals;
ReferenceStat<int64_t> d_statLearntsLiterals, d_statMaxLiterals;
ReferenceStat<int64_t> d_statTotLiterals;
public:
Statistics(StatisticsRegistry& registry);
void init(Minisat::SimpSolver* d_minisat);
void deinit();
};/* class MinisatSatSolver::Statistics */
Statistics d_statistics;
}; /* class MinisatSatSolver */
} // namespace prop
} // namespace cvc5
|
