summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/cadical.cpp165
-rw-r--r--src/prop/cadical.h90
-rw-r--r--src/prop/cryptominisat.cpp4
-rw-r--r--src/prop/cryptominisat.h2
-rw-r--r--src/prop/sat_solver_factory.cpp17
-rw-r--r--src/prop/sat_solver_factory.h25
6 files changed, 288 insertions, 15 deletions
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
new file mode 100644
index 000000000..3fd210699
--- /dev/null
+++ b/src/prop/cadical.cpp
@@ -0,0 +1,165 @@
+/********************* */
+/*! \file cadical.cpp
+ ** \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 "prop/cadical.h"
+
+#ifdef CVC4_USE_CADICAL
+
+#include "proof/sat_proof.h"
+
+namespace CVC4 {
+namespace prop {
+
+using CadicalLit = int;
+using CadicalVar = int;
+
+// helper functions
+namespace {
+
+SatValue toSatValue(int result)
+{
+ if (result == 10) return SAT_VALUE_TRUE;
+ if (result == 20) return SAT_VALUE_FALSE;
+ Assert(result == 0);
+ return SAT_VALUE_UNKNOWN;
+}
+
+SatValue toSatValueLit(int value)
+{
+ if (value == 1) return SAT_VALUE_TRUE;
+ Assert(value == -1);
+ return SAT_VALUE_FALSE;
+}
+
+CadicalLit toCadicalLit(const SatLiteral lit)
+{
+ return lit.isNegated() ? -lit.getSatVariable() : lit.getSatVariable();
+}
+
+CadicalVar toCadicalVar(SatVariable var) { return var; }
+
+} // namespace helper functions
+
+CadicalSolver::CadicalSolver(StatisticsRegistry* registry,
+ const std::string& name)
+ : d_solver(new CaDiCaL::Solver()),
+ // Note: CaDiCaL variables start with index 1 rather than 0 since negated
+ // literals are represented as the negation of the index.
+ d_nextVarIdx(1),
+ d_statistics(registry, name)
+{
+ d_true = newVar();
+ d_false = newVar();
+
+ d_solver->set("quiet", 1); // CaDiCaL is verbose by default
+ d_solver->add(toCadicalVar(d_true));
+ d_solver->add(0);
+ d_solver->add(-toCadicalVar(d_false));
+ d_solver->add(0);
+}
+
+CadicalSolver::~CadicalSolver() {}
+
+ClauseId CadicalSolver::addClause(SatClause& clause, bool removable)
+{
+ for (const SatLiteral& lit : clause)
+ {
+ d_solver->add(toCadicalLit(lit));
+ }
+ d_solver->add(0);
+ ++d_statistics.d_numClauses;
+ return ClauseIdError;
+}
+
+ClauseId CadicalSolver::addXorClause(SatClause& clause,
+ bool rhs,
+ bool removable)
+{
+ Unreachable("CaDiCaL does not support adding XOR clauses.");
+}
+
+SatVariable CadicalSolver::newVar(bool isTheoryAtom,
+ bool preRegister,
+ bool canErase)
+{
+ ++d_statistics.d_numVariables;
+ return d_nextVarIdx++;
+}
+
+SatVariable CadicalSolver::trueVar() { return d_true; }
+
+SatVariable CadicalSolver::falseVar() { return d_false; }
+
+SatValue CadicalSolver::solve()
+{
+ TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+ SatValue res = toSatValue(d_solver->solve());
+ d_okay = (res == SAT_VALUE_TRUE);
+ ++d_statistics.d_numSatCalls;
+ return res;
+}
+
+SatValue CadicalSolver::solve(long unsigned int&)
+{
+ Unimplemented("Setting limits for CaDiCaL not supported yet");
+};
+
+void CadicalSolver::interrupt() { d_solver->terminate(); }
+
+SatValue CadicalSolver::value(SatLiteral l)
+{
+ Assert(d_okay);
+ return toSatValueLit(d_solver->val(toCadicalLit(l)));
+}
+
+SatValue CadicalSolver::modelValue(SatLiteral l)
+{
+ Assert(d_okay);
+ return value(l);
+}
+
+unsigned CadicalSolver::getAssertionLevel() const
+{
+ Unreachable("CaDiCal does not support assertion levels.");
+}
+
+bool CadicalSolver::ok() const { return d_okay; }
+
+CadicalSolver::Statistics::Statistics(StatisticsRegistry* registry,
+ const std::string& prefix)
+ : d_registry(registry),
+ d_numSatCalls("theory::bv::" + prefix + "::cadical::calls_to_solve", 0),
+ d_numVariables("theory::bv::" + prefix + "::cadical::variables", 0),
+ d_numClauses("theory::bv::" + prefix + "::cadical::clauses", 0),
+ d_solveTime("theory::bv::" + prefix + "::cadical::solve_time")
+{
+ d_registry->registerStat(&d_numSatCalls);
+ d_registry->registerStat(&d_numVariables);
+ d_registry->registerStat(&d_numClauses);
+ d_registry->registerStat(&d_solveTime);
+}
+
+CadicalSolver::Statistics::~Statistics() {
+ d_registry->unregisterStat(&d_numSatCalls);
+ d_registry->unregisterStat(&d_numVariables);
+ d_registry->unregisterStat(&d_numClauses);
+ d_registry->unregisterStat(&d_solveTime);
+}
+
+} // namespace prop
+} // namespace CVC4
+
+#endif // CVC4_USE_CADICAL
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
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index c48a54afb..249a5eabb 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -79,9 +79,7 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
}
-CryptoMinisatSolver::~CryptoMinisatSolver() {
- delete d_solver;
-}
+CryptoMinisatSolver::~CryptoMinisatSolver() {}
ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
bool rhs,
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 32c05974b..c1782b6c0 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -38,7 +38,7 @@ namespace prop {
class CryptoMinisatSolver : public SatSolver {
private:
- CMSat::SATSolver* d_solver;
+ std::unique_ptr<CMSat::SATSolver> d_solver;
unsigned d_numVariables;
bool d_okay;
SatVariable d_true;
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 69fca59e1..0a8246667 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -17,6 +17,7 @@
#include "prop/sat_solver_factory.h"
#include "prop/bvminisat/bvminisat.h"
+#include "prop/cadical.h"
#include "prop/cryptominisat.h"
#include "prop/minisat/minisat.h"
@@ -31,6 +32,12 @@ BVSatSolverInterface* SatSolverFactory::createMinisat(
return new BVMinisatSatSolver(registry, mainSatContext, name);
}
+DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(
+ StatisticsRegistry* registry)
+{
+ return new MinisatSatSolver(registry);
+}
+
SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
const std::string& name)
{
@@ -41,10 +48,14 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
#endif
}
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(
- StatisticsRegistry* registry)
+SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
+ const std::string& name)
{
- return new MinisatSatSolver(registry);
+#ifdef CVC4_USE_CADICAL
+ return new CadicalSolver(registry, name);
+#else
+ Unreachable("CVC4 was not compiled with CaDiCaL support.");
+#endif
}
} // namespace prop
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index fac8c9083..8d6e405d8 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -16,7 +16,8 @@
#include "cvc4_private.h"
-#pragma once
+#ifndef __CVC4__PROP__SAT_SOLVER_FACTORY_H
+#define __CVC4__PROP__SAT_SOLVER_FACTORY_H
#include <string>
#include <vector>
@@ -28,17 +29,25 @@
namespace CVC4 {
namespace prop {
-class SatSolverFactory {
-public:
-
+class SatSolverFactory
+{
+ public:
static BVSatSolverInterface* createMinisat(context::Context* mainSatContext,
StatisticsRegistry* registry,
const std::string& name = "");
- static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry);
+
+ static DPLLSatSolverInterface* createDPLLMinisat(
+ StatisticsRegistry* registry);
+
static SatSolver* createCryptoMinisat(StatisticsRegistry* registry,
const std::string& name = "");
-};/* class SatSolverFactory */
+ static SatSolver* createCadical(StatisticsRegistry* registry,
+ const std::string& name = "");
+
+}; /* class SatSolverFactory */
+
+} // namespace prop
+} // namespace CVC4
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+#endif // __CVC4__PROP__SAT_SOLVER_FACTORY_H
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback