Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/prop/minisat/minisat.cpp	Lines:	143	176	81.3 %
Date:	2021-08-16	Branches:	92	284	32.4 %


/******************************************************************************
 * 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) + d_minisat->user_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	9920	MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry)
34	9920	: d_minisat(NULL), d_context(NULL), d_assumptions(), d_statistics(registry)
35	9920	{}
36
37	29760	MinisatSatSolver::~MinisatSatSolver()
38		{
39	9920	d_statistics.deinit();
40	9920	delete d_minisat;
41	19840	}
42
43	7138596	SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) {
44	7138596	if (var == var_Undef) {
45		return undefSatVariable;
46		}
47	7138596	return SatVariable(var);
48		}
49
50	44397349	Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
51	44397349	if (lit == undefSatLiteral) {
52	4401767	return Minisat::lit_Undef;
53		}
54	39995582	return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
55		}
56
57	20868823	SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
58	20868823	if (lit == Minisat::lit_Undef) {
59		return undefSatLiteral;
60		}
61
62	41737646	return SatLiteral(SatVariable(Minisat::var(lit)),
63	41737646	Minisat::sign(lit));
64		}
65
66	19854092	SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
67	19854092	if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
68	10238672	if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
69	2842153	Assert(res == (Minisat::lbool((uint8_t)1)));
70	2842153	return SAT_VALUE_FALSE;
71		}
72
73	1563290	Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val)
74		{
75	1563290	if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0);
76	1563290	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	8120712	void MinisatSatSolver::toMinisatClause(SatClause& clause,
89		Minisat::vec<Minisat::Lit>& minisat_clause) {
90	26906733	for (unsigned i = 0; i < clause.size(); ++i) {
91	18786021	minisat_clause.push(toMinisatLit(clause[i]));
92		}
93	8120712	Assert(clause.size() == (unsigned)minisat_clause.size());
94	8120712	}
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	9920	void MinisatSatSolver::initialize(context::Context* context,
105		TheoryProxy* theoryProxy,
106		context::UserContext* userContext,
107		ProofNodeManager* pnm)
108		{
109	9920	d_context = context;
110
111	9920	if (options::decisionMode() != options::DecisionMode::INTERNAL)
112		{
113	7741	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	9920	d_minisat = new Minisat::SimpSolver(
119		theoryProxy,
120		d_context,
121		userContext,
122		pnm,
123	9920	options::incrementalSolving()
124	9920	\|\| options::decisionMode() != options::DecisionMode::INTERNAL);
125
126	9920	d_statistics.init(d_minisat);
127	9920	}
128
129		// Like initialize() above, but called just before each search when in
130		// incremental mode
131	15201	void MinisatSatSolver::setupOptions() {
132		// Copy options from cvc5 options structure into minisat, as appropriate
133
134		// Set up the verbosity
135	15201	d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;
136
137		// Set up the random decision parameters
138	15201	d_minisat->random_var_freq = options::satRandomFreq();
139		// If 0, we use whatever we like (here, the Minisat default seed)
140	15201	if(options::satRandomSeed() != 0) {
141	2	d_minisat->random_seed = double(options::satRandomSeed());
142		}
143
144		// Give access to all possible options in the sat solver
145	15201	d_minisat->var_decay = options::satVarDecay();
146	15201	d_minisat->clause_decay = options::satClauseDecay();
147	15201	d_minisat->restart_first = options::satRestartFirst();
148	15201	d_minisat->restart_inc = options::satRestartInc();
149	15201	}
150
151	3823476	ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
152	7646952	Minisat::vec<Minisat::Lit> minisat_clause;
153	3823476	toMinisatClause(clause, minisat_clause);
154	3823476	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	3823476	if (!ok()) {
158	6332	return ClauseIdUndef;
159		}
160	3817144	d_minisat->addClause(minisat_clause, removable, clause_id);
161		// FIXME: to be deleted when we kill old proof code for unsat cores
162	3817144	Assert(!options::unsatCores() \|\| options::produceProofs()
163		\|\| clause_id != ClauseIdError);
164	3817144	return clause_id;
165		}
166
167	1275528	SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
168	1275528	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	11570	SatValue MinisatSatSolver::solve() {
189	11570	setupOptions();
190	11570	d_minisat->budgetOff();
191	11570	SatValue result = toSatLiteralValue(d_minisat->solve());
192	11554	d_minisat->clearInterrupt();
193	11554	return result;
194		}
195
196	3631	SatValue MinisatSatSolver::solve(const std::vector<SatLiteral>& assumptions)
197		{
198	3631	setupOptions();
199	3631	d_minisat->budgetOff();
200
201	3631	d_assumptions.clear();
202	7262	Minisat::vec<Minisat::Lit> assumps;
203
204	51936	for (const SatLiteral& lit : assumptions)
205		{
206	48305	Minisat::Lit mlit = toMinisatLit(lit);
207	48305	assumps.push(mlit);
208	48305	d_assumptions.emplace(lit);
209		}
210
211	3631	SatValue result = toSatLiteralValue(d_minisat->solve(assumps));
212	3631	d_minisat->clearInterrupt();
213	7262	return result;
214		}
215
216	1371	void MinisatSatSolver::getUnsatAssumptions(
217		std::vector<SatLiteral>& unsat_assumptions)
218		{
219	8110	for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i)
220		{
221	6739	Minisat::Lit mlit = d_minisat->d_conflict[i];
222	6739	SatLiteral lit = ~toSatLiteral(mlit);
223	6739	if (d_assumptions.find(lit) != d_assumptions.end())
224		{
225	6739	unsat_assumptions.push_back(lit);
226		}
227		}
228	1371	}
229
230	3823476	bool MinisatSatSolver::ok() const {
231	3823476	return d_minisat->okay();
232		}
233
234		void MinisatSatSolver::interrupt() {
235		d_minisat->interrupt();
236		}
237
238	19838907	SatValue MinisatSatSolver::value(SatLiteral l) {
239	19838907	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	76595	void MinisatSatSolver::requirePhase(SatLiteral lit) {
251	76595	Assert(!d_minisat->rnd_pol);
252	76595	Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl;
253	76595	SatVariable v = lit.getSatVariable();
254	76595	d_minisat->freezePolarity(v, lit.isNegated());
255	76595	}
256
257	176861	bool MinisatSatSolver::isDecision(SatVariable decn) const {
258	176861	return d_minisat->isDecision( decn );
259		}
260
261	16	int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
262		{
263	16	return d_minisat->level(v) + d_minisat->user_level(v);
264		}
265
266	8	int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const
267		{
268	8	return d_minisat->intro_level(v);
269		}
270
271	2508	SatProofManager* MinisatSatSolver::getProofManager()
272		{
273	2508	return d_minisat->getProofManager();
274		}
275
276	2811	std::shared_ptr<ProofNode> MinisatSatSolver::getProof()
277		{
278	2811	return d_minisat->getProof();
279		}
280
281		/** Incremental interface */
282
283	18877	unsigned MinisatSatSolver::getAssertionLevel() const {
284	18877	return d_minisat->getAssertionLevel();
285		}
286
287	4869	void MinisatSatSolver::push() {
288	4869	d_minisat->push();
289	4869	}
290
291	4869	void MinisatSatSolver::pop() {
292	4869	d_minisat->pop();
293	4869	}
294
295	15188	void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); }
296
297		/// Statistics for MinisatSatSolver
298
299	9920	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	9920	registry.registerReference<int64_t>("sat::tot_literals"))
315		{
316	9920	}
317
318	9920	void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
319	9920	d_statStarts.set(minisat->starts);
320	9920	d_statDecisions.set(minisat->decisions);
321	9920	d_statRndDecisions.set(minisat->rnd_decisions);
322	9920	d_statPropagations.set(minisat->propagations);
323	9920	d_statConflicts.set(minisat->conflicts);
324	9920	d_statClausesLiterals.set(minisat->clauses_literals);
325	9920	d_statLearntsLiterals.set(minisat->learnts_literals);
326	9920	d_statMaxLiterals.set(minisat->max_literals);
327	9920	d_statTotLiterals.set(minisat->tot_literals);
328	9920	}
329	9920	void MinisatSatSolver::Statistics::deinit()
330		{
331	9920	d_statStarts.reset();
332	9920	d_statDecisions.reset();
333	9920	d_statRndDecisions.reset();
334	9920	d_statPropagations.reset();
335	9920	d_statConflicts.reset();
336	9920	d_statClausesLiterals.reset();
337	9920	d_statLearntsLiterals.reset();
338	9920	d_statMaxLiterals.reset();
339	9920	d_statTotLiterals.reset();
340	9920	}
341
342		} // namespace prop
343		} // namespace cvc5
344
345		namespace cvc5 {
346		template <>
347	36462	prop::SatLiteral toSatLiteral<cvc5::Minisat::Solver>(Minisat::Solver::TLit lit)
348		{
349	36462	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	29340	} // namespace cvc5