diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-20 16:11:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-20 16:11:15 -0700 |
commit | 614670f98a9ab2d3cfcb9f364a1b06d78f63ebb0 (patch) | |
tree | 7dbdfbbae495fed26877c51267f6775f618f5d33 /src/prop/cadical.h | |
parent | 62f58d62c6c597eeb9cae5e08d74f21c4a5c5c40 (diff) |
Add support for CaDiCaL as eager BV SAT solver. (#1675)
Diffstat (limited to 'src/prop/cadical.h')
-rw-r--r-- | src/prop/cadical.h | 90 |
1 files changed, 90 insertions, 0 deletions
diff --git a/src/prop/cadical.h b/src/prop/cadical.h new file mode 100644 index 000000000..2e2c1cc51 --- /dev/null +++ b/src/prop/cadical.h @@ -0,0 +1,90 @@ +/********************* */ +/*! \file cadical.h + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief Wrapper for CaDiCaL SAT Solver. + ** + ** Implementation of the CaDiCaL SAT solver for CVC4 (bitvectors). + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROP__CADICAL_H +#define __CVC4__PROP__CADICAL_H + +#ifdef CVC4_USE_CADICAL + +#include "prop/sat_solver.h" + +#include <cadical.hpp> + +namespace CVC4 { +namespace prop { + +class CadicalSolver : public SatSolver +{ + public: + CadicalSolver(StatisticsRegistry* registry, const std::string& name = ""); + + ~CadicalSolver() override; + + ClauseId addClause(SatClause& clause, bool removable) override; + + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override; + + SatVariable newVar(bool isTheoryAtom = false, + bool preRegister = false, + bool canErase = true) override; + + SatVariable trueVar() override; + + SatVariable falseVar() override; + + SatValue solve() override; + + SatValue solve(long unsigned int&) override; + + void interrupt() override; + + SatValue value(SatLiteral l) override; + + SatValue modelValue(SatLiteral l) override; + + unsigned getAssertionLevel() const override; + + bool ok() const override; + + private: + std::unique_ptr<CaDiCaL::Solver> d_solver; + + unsigned d_nextVarIdx; + bool d_okay; + SatVariable d_true; + SatVariable d_false; + + struct Statistics + { + StatisticsRegistry* d_registry; + IntStat d_numSatCalls; + IntStat d_numVariables; + IntStat d_numClauses; + TimerStat d_solveTime; + Statistics(StatisticsRegistry* registry, const std::string& prefix); + ~Statistics(); + }; + + Statistics d_statistics; +}; + +} // namespace prop +} // namespace CVC4 + +#endif // CVC4_USE_CADICAL +#endif // __CVC4__PROP__CADICAL_H |