diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-13 15:47:34 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-13 15:47:34 -0700 |
commit | 36512d36ad34d43277443dcbfabf02baa5ad63b4 (patch) | |
tree | cbb661bab9318f036c032d85c652997701775be0 /src/prop | |
parent | 10f091e4fc23f80c884520ff484cacb125b45172 (diff) |
Use Cryptominisat version 5.0.2 (instead of 4.2.0). (#1664)
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cryptominisat.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index 197fece17..c48a54afb 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -21,11 +21,13 @@ #include "proof/clause_id.h" #include "proof/sat_proof.h" -#include <cryptominisat4/cryptominisat.h> +#include <cryptominisat5/cryptominisat.h> namespace CVC4 { namespace prop { +using CMSatVar = unsigned; + // helper functions namespace { @@ -95,7 +97,7 @@ ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause, // ensure all sat literals have positive polarity by pushing // the negation on the result - std::vector<CMSat::Var> xor_clause; + std::vector<CMSatVar> xor_clause; for (unsigned i = 0; i < clause.size(); ++i) { xor_clause.push_back(toInternalLit(clause[i]).var()); rhs ^= clause[i].isNegated(); @@ -166,7 +168,7 @@ SatValue CryptoMinisatSolver::solve(long unsigned int& resource) { SatValue CryptoMinisatSolver::value(SatLiteral l){ const std::vector<CMSat::lbool> model = d_solver->get_model(); - CMSat::Var var = l.getSatVariable(); + CMSatVar var = l.getSatVariable(); Assert (var < model.size()); CMSat::lbool value = model[var]; return toSatLiteralValue(value); |