1 /********************* */
2 /*! \file cryptominisat.h
4 ** Original author: lianah
6 ** Minor contributors (to current version):
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
16 ** Implementation of the cryptominisat sat solver for cvc4 (bitvectors).
19 #include "cvc4_private.h"
23 #include "prop/sat_solver.h"
25 #ifdef CVC4_USE_CRYPTOMINISAT
26 #include <cryptominisat4/cryptominisat.h>
30 class CryptoMinisatSolver
: public SatSolver
{
33 CMSat::SATSolver
* d_solver
;
34 unsigned d_numVariables
;
39 CryptoMinisatSolver(StatisticsRegistry
* registry
,
40 const std::string
& name
= "");
41 virtual ~CryptoMinisatSolver();
43 ClauseId
addClause(SatClause
& clause
, bool removable
);
44 ClauseId
addXorClause(SatClause
& clause
, bool rhs
, bool removable
);
46 bool nativeXor() { return true; }
48 SatVariable
newVar(bool isTheoryAtom
= false, bool preRegister
= false, bool canErase
= true);
50 SatVariable
trueVar();
51 SatVariable
falseVar();
53 void markUnremovable(SatLiteral lit
);
58 SatValue
solve(long unsigned int&);
60 SatValue
value(SatLiteral l
);
61 SatValue
modelValue(SatLiteral l
);
63 unsigned getAssertionLevel() const;
66 // helper methods for converting from the internal Minisat representation
68 static SatVariable
toSatVariable(CMSat::Var var
);
69 static CMSat::Lit
toInternalLit(SatLiteral lit
);
70 static SatLiteral
toSatLiteral(CMSat::Lit lit
);
71 static SatValue
toSatLiteralValue(bool res
);
72 static SatValue
toSatLiteralValue(CMSat::lbool res
);
74 static void toInternalClause(SatClause
& clause
, std::vector
<CMSat::Lit
>& internal_clause
);
75 static void toSatClause (std::vector
<CMSat::Lit
>& clause
, SatClause
& sat_clause
);
79 StatisticsRegistry
* d_registry
;
80 IntStat d_statCallsToSolve
;
81 IntStat d_xorClausesAdded
;
82 IntStat d_clausesAdded
;
83 TimerStat d_solveTime
;
85 Statistics(StatisticsRegistry
* registry
,
86 const std::string
& prefix
);
90 Statistics d_statistics
;
95 #else // CVC4_USE_CRYPTOMINISAT
100 class CryptoMinisatSolver
: public SatSolver
{
103 CryptoMinisatSolver(StatisticsRegistry
* registry
,
104 const std::string
& name
= "") { Unreachable(); }
105 /** Assert a clause in the solver. */
106 ClauseId
addClause(SatClause
& clause
, bool removable
) {
110 /** Return true if the solver supports native xor resoning */
111 bool nativeXor() { Unreachable(); }
113 /** Add a clause corresponding to rhs = l1 xor .. xor ln */
114 ClauseId
addXorClause(SatClause
& clause
, bool rhs
, bool removable
) {
118 SatVariable
newVar(bool isTheoryAtom
, bool preRegister
, bool canErase
) { Unreachable(); }
119 SatVariable
trueVar() { Unreachable(); }
120 SatVariable
falseVar() { Unreachable(); }
121 SatValue
solve() { Unreachable(); }
122 SatValue
solve(long unsigned int&) { Unreachable(); }
123 void interrupt() { Unreachable(); }
124 SatValue
value(SatLiteral l
) { Unreachable(); }
125 SatValue
modelValue(SatLiteral l
) { Unreachable(); }
126 unsigned getAssertionLevel() const { Unreachable(); }
127 bool ok() const { return false;};
130 };/* class CryptoMinisatSolver */
134 #endif // CVC4_USE_CRYPTOMINISAT