Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/prop/minisat/minisat.cpp	Lines:	138	176	78.4 %
Date:	2021-05-21	Branches:	100	314	31.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Dejan Jovanovic, Liana Hadarean, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * SAT Solver.
 *
 * Implementation of the minisat interface for cvc5.
 */

#include "prop/minisat/minisat.h"

#include "options/base_options.h"
#include "options/decision_options.h"
#include "options/prop_options.h"
#include "options/smt_options.h"
#include "proof/clause_id.h"
#include "prop/minisat/simp/SimpSolver.h"
#include "util/statistics_stats.h"

namespace cvc5 {
namespace prop {

//// DPllMinisatSatSolver

MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry)
    : d_minisat(NULL), d_context(NULL), d_assumptions(), d_statistics(registry)
{}

MinisatSatSolver::~MinisatSatSolver()
{
  d_statistics.deinit();
  delete d_minisat;
}

SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) {
  if (var == var_Undef) {
    return undefSatVariable;
  }
  return SatVariable(var);
}

Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
  if (lit == undefSatLiteral) {
    return Minisat::lit_Undef;
  }
  return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
}

SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
  if (lit == Minisat::lit_Undef) {
    return undefSatLiteral;
  }

  return SatLiteral(SatVariable(Minisat::var(lit)),
                    Minisat::sign(lit));
}

SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
  if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
  if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
  Assert(res == (Minisat::lbool((uint8_t)1)));
  return SAT_VALUE_FALSE;
}

Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val)
{
  if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0);
  if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2);
  Assert(val == SAT_VALUE_FALSE);
  return Minisat::lbool((uint8_t)1);
}

/*bool MinisatSatSolver::tobool(SatValue val)
{
  if(val == SAT_VALUE_TRUE) return true;
  Assert(val == SAT_VALUE_FALSE);
  return false;
  }*/

void MinisatSatSolver::toMinisatClause(SatClause& clause,
                                           Minisat::vec<Minisat::Lit>& minisat_clause) {
  for (unsigned i = 0; i < clause.size(); ++i) {
    minisat_clause.push(toMinisatLit(clause[i]));
  }
  Assert(clause.size() == (unsigned)minisat_clause.size());
}

void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
                                       SatClause& sat_clause) {
  for (int i = 0; i < clause.size(); ++i) {
    sat_clause.push_back(toSatLiteral(clause[i]));
  }
  Assert((unsigned)clause.size() == sat_clause.size());
}

void MinisatSatSolver::initialize(context::Context* context,
                                  TheoryProxy* theoryProxy,
                                  context::UserContext* userContext,
                                  ProofNodeManager* pnm)
{
  d_context = context;

  if (options::decisionMode() != options::DecisionMode::INTERNAL)
  {
    Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)"
             << " unless using internal decision strategy." << std::endl;
  }

  // Create the solver
  d_minisat = new Minisat::SimpSolver(
      theoryProxy,
      d_context,
      userContext,
      pnm,
      options::incrementalSolving()
          || options::decisionMode() != options::DecisionMode::INTERNAL);

  d_statistics.init(d_minisat);
}

// Like initialize() above, but called just before each search when in
// incremental mode
void MinisatSatSolver::setupOptions() {
  // Copy options from cvc5 options structure into minisat, as appropriate

  // Set up the verbosity
  d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;

  // Set up the random decision parameters
  d_minisat->random_var_freq = options::satRandomFreq();
  // If 0, we use whatever we like (here, the Minisat default seed)
  if(options::satRandomSeed() != 0) {
    d_minisat->random_seed = double(options::satRandomSeed());
  }

  // Give access to all possible options in the sat solver
  d_minisat->var_decay = options::satVarDecay();
  d_minisat->clause_decay = options::satClauseDecay();
  d_minisat->restart_first = options::satRestartFirst();
  d_minisat->restart_inc = options::satRestartInc();
}

ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
  Minisat::vec<Minisat::Lit> minisat_clause;
  toMinisatClause(clause, minisat_clause);
  ClauseId clause_id = ClauseIdError;
  // FIXME: This relies on the invariant that when ok() is false
  // the SAT solver does not add the clause (which is what Minisat currently does)
  if (!ok()) {
    return ClauseIdUndef;
  }
  d_minisat->addClause(minisat_clause, removable, clause_id);
  // FIXME: to be deleted when we kill old proof code for unsat cores
  Assert(!options::unsatCores() || options::produceProofs()
         || clause_id != ClauseIdError);
  return clause_id;
}

SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
  return d_minisat->newVar(true, true, isTheoryAtom, preRegister, canErase);
}

SatValue MinisatSatSolver::solve(unsigned long& resource) {
  Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
  setupOptions();
  if(resource == 0) {
    d_minisat->budgetOff();
  } else {
    d_minisat->setConfBudget(resource);
  }
  Minisat::vec<Minisat::Lit> empty;
  unsigned long conflictsBefore = d_minisat->conflicts + d_minisat->resources_consumed;
  SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
  d_minisat->clearInterrupt();
  resource = d_minisat->conflicts + d_minisat->resources_consumed - conflictsBefore;
  Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
  return result;
}

SatValue MinisatSatSolver::solve() {
  setupOptions();
  d_minisat->budgetOff();
  SatValue result = toSatLiteralValue(d_minisat->solve());
  d_minisat->clearInterrupt();
  return result;
}

SatValue MinisatSatSolver::solve(const std::vector<SatLiteral>& assumptions)
{
  setupOptions();
  d_minisat->budgetOff();

  d_assumptions.clear();
  Minisat::vec<Minisat::Lit> assumps;

  for (const SatLiteral& lit : assumptions)
  {
    Minisat::Lit mlit = toMinisatLit(lit);
    assumps.push(mlit);
    d_assumptions.emplace(lit);
  }

  SatValue result = toSatLiteralValue(d_minisat->solve(assumps));
  d_minisat->clearInterrupt();
  return result;
}

void MinisatSatSolver::getUnsatAssumptions(
    std::vector<SatLiteral>& unsat_assumptions)
{
  for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i)
  {
    Minisat::Lit mlit = d_minisat->d_conflict[i];
    SatLiteral lit = ~toSatLiteral(mlit);
    if (d_assumptions.find(lit) != d_assumptions.end())
    {
      unsat_assumptions.push_back(lit);
    }
  }
}

bool MinisatSatSolver::ok() const {
  return d_minisat->okay();
}

void MinisatSatSolver::interrupt() {
  d_minisat->interrupt();
}

SatValue MinisatSatSolver::value(SatLiteral l) {
  return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
}

SatValue MinisatSatSolver::modelValue(SatLiteral l){
  return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
}

bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
  return true;
}

void MinisatSatSolver::requirePhase(SatLiteral lit) {
  Assert(!d_minisat->rnd_pol);
  Debug("minisat") << "requirePhase(" << lit << ")" << " " <<  lit.getSatVariable() << " " << lit.isNegated() << std::endl;
  SatVariable v = lit.getSatVariable();
  d_minisat->freezePolarity(v, lit.isNegated());
}

bool MinisatSatSolver::isDecision(SatVariable decn) const {
  return d_minisat->isDecision( decn );
}

int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
{
  return d_minisat->level(v);
}

int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const
{
  return d_minisat->intro_level(v);
}

SatProofManager* MinisatSatSolver::getProofManager()
{
  return d_minisat->getProofManager();
}

std::shared_ptr<ProofNode> MinisatSatSolver::getProof()
{
  return d_minisat->getProof();
}

/** Incremental interface */

unsigned MinisatSatSolver::getAssertionLevel() const {
  return d_minisat->getAssertionLevel();
}

void MinisatSatSolver::push() {
  d_minisat->push();
}

void MinisatSatSolver::pop() {
  d_minisat->pop();
}

void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); }

/// Statistics for MinisatSatSolver

MinisatSatSolver::Statistics::Statistics(StatisticsRegistry& registry)
    : d_statStarts(registry.registerReference<int64_t>("sat::starts")),
      d_statDecisions(registry.registerReference<int64_t>("sat::decisions")),
      d_statRndDecisions(
          registry.registerReference<int64_t>("sat::rnd_decisions")),
      d_statPropagations(
          registry.registerReference<int64_t>("sat::propagations")),
      d_statConflicts(registry.registerReference<int64_t>("sat::conflicts")),
      d_statClausesLiterals(
          registry.registerReference<int64_t>("sat::clauses_literals")),
      d_statLearntsLiterals(
          registry.registerReference<int64_t>("sat::learnts_literals")),
      d_statMaxLiterals(
          registry.registerReference<int64_t>("sat::max_literals")),
      d_statTotLiterals(
          registry.registerReference<int64_t>("sat::tot_literals"))
{
}

void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
  d_statStarts.set(minisat->starts);
  d_statDecisions.set(minisat->decisions);
  d_statRndDecisions.set(minisat->rnd_decisions);
  d_statPropagations.set(minisat->propagations);
  d_statConflicts.set(minisat->conflicts);
  d_statClausesLiterals.set(minisat->clauses_literals);
  d_statLearntsLiterals.set(minisat->learnts_literals);
  d_statMaxLiterals.set(minisat->max_literals);
  d_statTotLiterals.set(minisat->tot_literals);
}
void MinisatSatSolver::Statistics::deinit()
{
  d_statStarts.reset();
  d_statDecisions.reset();
  d_statRndDecisions.reset();
  d_statPropagations.reset();
  d_statConflicts.reset();
  d_statClausesLiterals.reset();
  d_statLearntsLiterals.reset();
  d_statMaxLiterals.reset();
  d_statTotLiterals.reset();
}

}  // namespace prop
}  // namespace cvc5

namespace cvc5 {
template <>
prop::SatLiteral toSatLiteral<cvc5::Minisat::Solver>(Minisat::Solver::TLit lit)
{
  return prop::MinisatSatSolver::toSatLiteral(lit);
}

template <>
void toSatClause<cvc5::Minisat::Solver>(
    const cvc5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
{
  prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Dejan Jovanovic, Liana Hadarean, Morgan Deters
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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.
11		* ****************************************************************************
12		*
13		* SAT Solver.
14		*
15		* Implementation of the minisat interface for cvc5.
16		*/
17
18		#include "prop/minisat/minisat.h"
19
20		#include "options/base_options.h"
21		#include "options/decision_options.h"
22		#include "options/prop_options.h"
23		#include "options/smt_options.h"
24		#include "proof/clause_id.h"
25		#include "prop/minisat/simp/SimpSolver.h"
26		#include "util/statistics_stats.h"
27
28		namespace cvc5 {
29		namespace prop {
30
31		//// DPllMinisatSatSolver
32
33	8988	MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry)
34	8988	: d_minisat(NULL), d_context(NULL), d_assumptions(), d_statistics(registry)
35	8988	{}
36
37	26964	MinisatSatSolver::~MinisatSatSolver()
38		{
39	8988	d_statistics.deinit();
40	8988	delete d_minisat;
41	17976	}
42
43	5921844	SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) {
44	5921844	if (var == var_Undef) {
45		return undefSatVariable;
46		}
47	5921844	return SatVariable(var);
48		}
49
50	65360539	Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
51	65360539	if (lit == undefSatLiteral) {
52	3297482	return Minisat::lit_Undef;
53		}
54	62063057	return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
55		}
56
57	20175015	SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
58	20175015	if (lit == Minisat::lit_Undef) {
59		return undefSatLiteral;
60		}
61
62	40350030	return SatLiteral(SatVariable(Minisat::var(lit)),
63	40350030	Minisat::sign(lit));
64		}
65
66	47029249	SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
67	47029249	if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
68	19864228	if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
69	12707805	Assert(res == (Minisat::lbool((uint8_t)1)));
70	12707805	return SAT_VALUE_FALSE;
71		}
72
73	1299960	Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val)
74		{
75	1299960	if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0);
76	1299960	if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2);
77		Assert(val == SAT_VALUE_FALSE);
78		return Minisat::lbool((uint8_t)1);
79		}
80
81		/*bool MinisatSatSolver::tobool(SatValue val)
82		{
83		if(val == SAT_VALUE_TRUE) return true;
84		Assert(val == SAT_VALUE_FALSE);
85		return false;
86		}*/
87
88	5433007	void MinisatSatSolver::toMinisatClause(SatClause& clause,
89		Minisat::vec<Minisat::Lit>& minisat_clause) {
90	19602778	for (unsigned i = 0; i < clause.size(); ++i) {
91	14169771	minisat_clause.push(toMinisatLit(clause[i]));
92		}
93	5433007	Assert(clause.size() == (unsigned)minisat_clause.size());
94	5433007	}
95
96		void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
97		SatClause& sat_clause) {
98		for (int i = 0; i < clause.size(); ++i) {
99		sat_clause.push_back(toSatLiteral(clause[i]));
100		}
101		Assert((unsigned)clause.size() == sat_clause.size());
102		}
103
104	8988	void MinisatSatSolver::initialize(context::Context* context,
105		TheoryProxy* theoryProxy,
106		context::UserContext* userContext,
107		ProofNodeManager* pnm)
108		{
109	8988	d_context = context;
110
111	8988	if (options::decisionMode() != options::DecisionMode::INTERNAL)
112		{
113	6916	Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)"
114		<< " unless using internal decision strategy." << std::endl;
115		}
116
117		// Create the solver
118	8988	d_minisat = new Minisat::SimpSolver(
119		theoryProxy,
120		d_context,
121		userContext,
122		pnm,
123	8988	options::incrementalSolving()
124	8988	\|\| options::decisionMode() != options::DecisionMode::INTERNAL);
125
126	8988	d_statistics.init(d_minisat);
127	8988	}
128
129		// Like initialize() above, but called just before each search when in
130		// incremental mode
131	12745	void MinisatSatSolver::setupOptions() {
132		// Copy options from cvc5 options structure into minisat, as appropriate
133
134		// Set up the verbosity
135	615438	d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;
136
137		// Set up the random decision parameters
138	25490	d_minisat->random_var_freq = options::satRandomFreq();
139		// If 0, we use whatever we like (here, the Minisat default seed)
140	25490	if(options::satRandomSeed() != 0) {
141		d_minisat->random_seed = double(options::satRandomSeed());
142		}
143
144		// Give access to all possible options in the sat solver
145	25490	d_minisat->var_decay = options::satVarDecay();
146	25490	d_minisat->clause_decay = options::satClauseDecay();
147	25490	d_minisat->restart_first = options::satRestartFirst();
148	25490	d_minisat->restart_inc = options::satRestartInc();
149	12745	}
150
151	2288139	ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
152	4576278	Minisat::vec<Minisat::Lit> minisat_clause;
153	2288139	toMinisatClause(clause, minisat_clause);
154	2288139	ClauseId clause_id = ClauseIdError;
155		// FIXME: This relies on the invariant that when ok() is false
156		// the SAT solver does not add the clause (which is what Minisat currently does)
157	2288139	if (!ok()) {
158	6219	return ClauseIdUndef;
159		}
160	2281920	d_minisat->addClause(minisat_clause, removable, clause_id);
161		// FIXME: to be deleted when we kill old proof code for unsat cores
162	2281920	Assert(!options::unsatCores() \|\| options::produceProofs()
163		\|\| clause_id != ClauseIdError);
164	2281920	return clause_id;
165		}
166
167	838187	SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
168	838187	return d_minisat->newVar(true, true, isTheoryAtom, preRegister, canErase);
169		}
170
171		SatValue MinisatSatSolver::solve(unsigned long& resource) {
172		Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
173		setupOptions();
174		if(resource == 0) {
175		d_minisat->budgetOff();
176		} else {
177		d_minisat->setConfBudget(resource);
178		}
179		Minisat::vec<Minisat::Lit> empty;
180		unsigned long conflictsBefore = d_minisat->conflicts + d_minisat->resources_consumed;
181		SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
182		d_minisat->clearInterrupt();
183		resource = d_minisat->conflicts + d_minisat->resources_consumed - conflictsBefore;
184		Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
185		return result;
186		}
187
188	10739	SatValue MinisatSatSolver::solve() {
189	10739	setupOptions();
190	10739	d_minisat->budgetOff();
191	10739	SatValue result = toSatLiteralValue(d_minisat->solve());
192	10723	d_minisat->clearInterrupt();
193	10723	return result;
194		}
195
196	2006	SatValue MinisatSatSolver::solve(const std::vector<SatLiteral>& assumptions)
197		{
198	2006	setupOptions();
199	2006	d_minisat->budgetOff();
200
201	2006	d_assumptions.clear();
202	4012	Minisat::vec<Minisat::Lit> assumps;
203
204	36258	for (const SatLiteral& lit : assumptions)
205		{
206	34252	Minisat::Lit mlit = toMinisatLit(lit);
207	34252	assumps.push(mlit);
208	34252	d_assumptions.emplace(lit);
209		}
210
211	2006	SatValue result = toSatLiteralValue(d_minisat->solve(assumps));
212	2006	d_minisat->clearInterrupt();
213	4012	return result;
214		}
215
216	963	void MinisatSatSolver::getUnsatAssumptions(
217		std::vector<SatLiteral>& unsat_assumptions)
218		{
219	6267	for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i)
220		{
221	5304	Minisat::Lit mlit = d_minisat->d_conflict[i];
222	5304	SatLiteral lit = ~toSatLiteral(mlit);
223	5304	if (d_assumptions.find(lit) != d_assumptions.end())
224		{
225	5304	unsat_assumptions.push_back(lit);
226		}
227		}
228	963	}
229
230	2288139	bool MinisatSatSolver::ok() const {
231	2288139	return d_minisat->okay();
232		}
233
234		void MinisatSatSolver::interrupt() {
235		d_minisat->interrupt();
236		}
237
238	47016520	SatValue MinisatSatSolver::value(SatLiteral l) {
239	47016520	return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
240		}
241
242		SatValue MinisatSatSolver::modelValue(SatLiteral l){
243		return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
244		}
245
246		bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
247		return true;
248		}
249
250	59017	void MinisatSatSolver::requirePhase(SatLiteral lit) {
251	59017	Assert(!d_minisat->rnd_pol);
252	59017	Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl;
253	59017	SatVariable v = lit.getSatVariable();
254	59017	d_minisat->freezePolarity(v, lit.isNegated());
255	59017	}
256
257	225678	bool MinisatSatSolver::isDecision(SatVariable decn) const {
258	225678	return d_minisat->isDecision( decn );
259		}
260
261		int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
262		{
263		return d_minisat->level(v);
264		}
265
266		int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const
267		{
268		return d_minisat->intro_level(v);
269		}
270
271	2438	SatProofManager* MinisatSatSolver::getProofManager()
272		{
273	2438	return d_minisat->getProofManager();
274		}
275
276	2709	std::shared_ptr<ProofNode> MinisatSatSolver::getProof()
277		{
278	2709	return d_minisat->getProof();
279		}
280
281		/** Incremental interface */
282
283	18073	unsigned MinisatSatSolver::getAssertionLevel() const {
284	18073	return d_minisat->getAssertionLevel();
285		}
286
287	3596	void MinisatSatSolver::push() {
288	3596	d_minisat->push();
289	3596	}
290
291	3596	void MinisatSatSolver::pop() {
292	3596	d_minisat->pop();
293	3596	}
294
295	12732	void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); }
296
297		/// Statistics for MinisatSatSolver
298
299	8988	MinisatSatSolver::Statistics::Statistics(StatisticsRegistry& registry)
300		: d_statStarts(registry.registerReference<int64_t>("sat::starts")),
301		d_statDecisions(registry.registerReference<int64_t>("sat::decisions")),
302		d_statRndDecisions(
303		registry.registerReference<int64_t>("sat::rnd_decisions")),
304		d_statPropagations(
305		registry.registerReference<int64_t>("sat::propagations")),
306		d_statConflicts(registry.registerReference<int64_t>("sat::conflicts")),
307		d_statClausesLiterals(
308		registry.registerReference<int64_t>("sat::clauses_literals")),
309		d_statLearntsLiterals(
310		registry.registerReference<int64_t>("sat::learnts_literals")),
311		d_statMaxLiterals(
312		registry.registerReference<int64_t>("sat::max_literals")),
313		d_statTotLiterals(
314	8988	registry.registerReference<int64_t>("sat::tot_literals"))
315		{
316	8988	}
317
318	8988	void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
319	8988	d_statStarts.set(minisat->starts);
320	8988	d_statDecisions.set(minisat->decisions);
321	8988	d_statRndDecisions.set(minisat->rnd_decisions);
322	8988	d_statPropagations.set(minisat->propagations);
323	8988	d_statConflicts.set(minisat->conflicts);
324	8988	d_statClausesLiterals.set(minisat->clauses_literals);
325	8988	d_statLearntsLiterals.set(minisat->learnts_literals);
326	8988	d_statMaxLiterals.set(minisat->max_literals);
327	8988	d_statTotLiterals.set(minisat->tot_literals);
328	8988	}
329	8988	void MinisatSatSolver::Statistics::deinit()
330		{
331	8988	d_statStarts.reset();
332	8988	d_statDecisions.reset();
333	8988	d_statRndDecisions.reset();
334	8988	d_statPropagations.reset();
335	8988	d_statConflicts.reset();
336	8988	d_statClausesLiterals.reset();
337	8988	d_statLearntsLiterals.reset();
338	8988	d_statMaxLiterals.reset();
339	8988	d_statTotLiterals.reset();
340	8988	}
341
342		} // namespace prop
343		} // namespace cvc5
344
345		namespace cvc5 {
346		template <>
347	61716	prop::SatLiteral toSatLiteral<cvc5::Minisat::Solver>(Minisat::Solver::TLit lit)
348		{
349	61716	return prop::MinisatSatSolver::toSatLiteral(lit);
350		}
351
352		template <>
353		void toSatClause<cvc5::Minisat::Solver>(
354		const cvc5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
355		{
356		prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
357		}
358
359	706898	} // namespace cvc5