1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
14 ** Implementation of the minisat for cvc4 (bitvectors).
17 #include "cvc4_private.h"
21 #include "context/cdo.h"
22 #include "proof/clause_id.h"
23 #include "prop/bvminisat/simp/SimpSolver.h"
24 #include "prop/sat_solver.h"
25 #include "util/statistics_registry.h"
30 class BVMinisatSatSolver
: public BVSatSolverInterface
, public context::ContextNotifyObj
{
34 class MinisatNotify
: public BVMinisat::Notify
{
35 BVSatSolverInterface::Notify
* d_notify
;
37 MinisatNotify(BVSatSolverInterface::Notify
* notify
)
40 bool notify(BVMinisat::Lit lit
) {
41 return d_notify
->notify(toSatLiteral(lit
));
43 void notify(BVMinisat::vec
<BVMinisat::Lit
>& clause
) {
45 for (int i
= 0; i
< clause
.size(); ++i
) {
46 satClause
.push_back(toSatLiteral(clause
[i
]));
48 d_notify
->notify(satClause
);
51 void spendResource(unsigned ammount
) {
52 d_notify
->spendResource(ammount
);
54 void safePoint(unsigned ammount
) {
55 d_notify
->safePoint(ammount
);
59 BVMinisat::SimpSolver
* d_minisat
;
60 MinisatNotify
* d_minisatNotify
;
62 unsigned d_assertionsCount
;
63 context::CDO
<unsigned> d_assertionsRealCount
;
64 context::CDO
<unsigned> d_lastPropagation
;
68 void contextNotifyPop();
72 BVMinisatSatSolver(StatisticsRegistry
* registry
, context::Context
* mainSatContext
, const std::string
& name
= "");
73 virtual ~BVMinisatSatSolver();
75 void setNotify(Notify
* notify
);
77 ClauseId
addClause(SatClause
& clause
, bool removable
);
79 ClauseId
addXorClause(SatClause
& clause
, bool rhs
, bool removable
) {
80 Unreachable("Minisat does not support native XOR reasoning");
85 SatVariable
newVar(bool isTheoryAtom
= false, bool preRegister
= false, bool canErase
= true);
87 SatVariable
trueVar() { return d_minisat
->trueVar(); }
88 SatVariable
falseVar() { return d_minisat
->falseVar(); }
90 void markUnremovable(SatLiteral lit
);
95 SatValue
solve(long unsigned int&);
97 void getUnsatCore(SatClause
& unsatCore
);
99 SatValue
value(SatLiteral l
);
100 SatValue
modelValue(SatLiteral l
);
102 void unregisterVar(SatLiteral lit
);
103 void renewVar(SatLiteral lit
, int level
= -1);
104 unsigned getAssertionLevel() const;
107 // helper methods for converting from the internal Minisat representation
109 static SatVariable
toSatVariable(BVMinisat::Var var
);
110 static BVMinisat::Lit
toMinisatLit(SatLiteral lit
);
111 static SatLiteral
toSatLiteral(BVMinisat::Lit lit
);
112 static SatValue
toSatLiteralValue(BVMinisat::lbool res
);
114 static void toMinisatClause(SatClause
& clause
, BVMinisat::vec
<BVMinisat::Lit
>& minisat_clause
);
115 static void toSatClause (const BVMinisat::Clause
& clause
, SatClause
& sat_clause
);
116 void addMarkerLiteral(SatLiteral lit
);
118 void explain(SatLiteral lit
, std::vector
<SatLiteral
>& explanation
);
120 SatValue
assertAssumption(SatLiteral lit
, bool propagate
);
122 void popAssumption();
124 void setProofLog( BitVectorProof
* bvp
);
127 /* Disable the default constructor. */
128 BVMinisatSatSolver() CVC4_UNDEFINED
;
132 StatisticsRegistry
* d_registry
;
133 ReferenceStat
<uint64_t> d_statStarts
, d_statDecisions
;
134 ReferenceStat
<uint64_t> d_statRndDecisions
, d_statPropagations
;
135 ReferenceStat
<uint64_t> d_statConflicts
, d_statClausesLiterals
;
136 ReferenceStat
<uint64_t> d_statLearntsLiterals
, d_statMaxLiterals
;
137 ReferenceStat
<uint64_t> d_statTotLiterals
;
138 ReferenceStat
<int> d_statEliminatedVars
;
139 IntStat d_statCallsToSolve
;
140 BackedStat
<double> d_statSolveTime
;
141 bool d_registerStats
;
142 Statistics(StatisticsRegistry
* registry
, const std::string
& prefix
);
144 void init(BVMinisat::SimpSolver
* minisat
);
147 Statistics d_statistics
;
150 } /* CVC4::prop namespace */
151 } /* CVC4 namespace */