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 interface for cvc4.
19 #include "prop/sat_solver.h"
20 #include "prop/minisat/simp/SimpSolver.h"
21 #include "util/statistics_registry.h"
26 class MinisatSatSolver
: public DPLLSatSolverInterface
{
29 MinisatSatSolver(StatisticsRegistry
* registry
);
30 virtual ~MinisatSatSolver();
33 static SatVariable
toSatVariable(Minisat::Var var
);
34 static Minisat::Lit
toMinisatLit(SatLiteral lit
);
35 static SatLiteral
toSatLiteral(Minisat::Lit lit
);
36 static SatValue
toSatLiteralValue(Minisat::lbool res
);
37 static Minisat::lbool
toMinisatlbool(SatValue val
);
38 //(Commented because not in use) static bool tobool(SatValue val);
40 static void toMinisatClause(SatClause
& clause
, Minisat::vec
<Minisat::Lit
>& minisat_clause
);
41 static void toSatClause (const Minisat::Clause
& clause
, SatClause
& sat_clause
);
42 void initialize(context::Context
* context
, TheoryProxy
* theoryProxy
);
44 ClauseId
addClause(SatClause
& clause
, bool removable
);
45 ClauseId
addXorClause(SatClause
& clause
, bool rhs
, bool removable
) {
46 Unreachable("Minisat does not support native XOR reasoning");
49 SatVariable
newVar(bool isTheoryAtom
, bool preRegister
, bool canErase
);
50 SatVariable
trueVar() { return d_minisat
->trueVar(); }
51 SatVariable
falseVar() { return d_minisat
->falseVar(); }
54 SatValue
solve(long unsigned int&);
60 SatValue
value(SatLiteral l
);
62 SatValue
modelValue(SatLiteral l
);
64 bool properExplanation(SatLiteral lit
, SatLiteral expl
) const;
66 /** Incremental interface */
68 unsigned getAssertionLevel() const;
74 void requirePhase(SatLiteral lit
);
78 bool isDecision(SatVariable decn
) const;
82 /** The SatSolver used */
83 Minisat::SimpSolver
* d_minisat
;
85 /** Context we will be using to synchronize the sat solver */
86 context::Context
* d_context
;
92 StatisticsRegistry
* d_registry
;
93 ReferenceStat
<uint64_t> d_statStarts
, d_statDecisions
;
94 ReferenceStat
<uint64_t> d_statRndDecisions
, d_statPropagations
;
95 ReferenceStat
<uint64_t> d_statConflicts
, d_statClausesLiterals
;
96 ReferenceStat
<uint64_t> d_statLearntsLiterals
, d_statMaxLiterals
;
97 ReferenceStat
<uint64_t> d_statTotLiterals
;
99 Statistics(StatisticsRegistry
* registry
);
101 void init(Minisat::SimpSolver
* d_minisat
);
102 };/* class MinisatSatSolver::Statistics */
103 Statistics d_statistics
;
105 };/* class MinisatSatSolver */
107 }/* CVC4::prop namespace */
108 }/* CVC4 namespace */