Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/prop/minisat/minisat.cpp	Lines:	145	177	81.9 %
Date:	2021-11-06	Branches:	92	278	33.1 %


/******************************************************************************
 * 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(Env& env, StatisticsRegistry& registry)
    : EnvObj(env),
      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().decision.decisionMode != options::DecisionMode::INTERNAL)
  {
    verbose(1) << "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().base.incrementalSolving
                                  || options().decision.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().base.verbosity > 0) ? 1 : -1;

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

  // Give access to all possible options in the sat solver
  d_minisat->var_decay = options().prop.satVarDecay;
  d_minisat->clause_decay = options().prop.satClauseDecay;
  d_minisat->restart_first = options().prop.satRestartFirst;
  d_minisat->restart_inc = options().prop.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().smt.unsatCores || options().smt.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	15339	MinisatSatSolver::MinisatSatSolver(Env& env, StatisticsRegistry& registry)
34		: EnvObj(env),
35		d_minisat(NULL),
36		d_context(NULL),
37		d_assumptions(),
38	15339	d_statistics(registry)
39	15339	{}
40
41	46002	MinisatSatSolver::~MinisatSatSolver()
42		{
43	15334	d_statistics.deinit();
44	15334	delete d_minisat;
45	30668	}
46
47	8722158	SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) {
48	8722158	if (var == var_Undef) {
49		return undefSatVariable;
50		}
51	8722158	return SatVariable(var);
52		}
53
54	53908529	Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
55	53908529	if (lit == undefSatLiteral) {
56	5365466	return Minisat::lit_Undef;
57		}
58	48543063	return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
59		}
60
61	23945539	SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
62	23945539	if (lit == Minisat::lit_Undef) {
63		return undefSatLiteral;
64		}
65
66	47891078	return SatLiteral(SatVariable(Minisat::var(lit)),
67	47891078	Minisat::sign(lit));
68		}
69
70	25552478	SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
71	25552478	if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
72	13358639	if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
73	3550570	Assert(res == (Minisat::lbool((uint8_t)1)));
74	3550570	return SAT_VALUE_FALSE;
75		}
76
77	1939049	Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val)
78		{
79	1939049	if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0);
80	1939049	if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2);
81		Assert(val == SAT_VALUE_FALSE);
82		return Minisat::lbool((uint8_t)1);
83		}
84
85		/*bool MinisatSatSolver::tobool(SatValue val)
86		{
87		if(val == SAT_VALUE_TRUE) return true;
88		Assert(val == SAT_VALUE_FALSE);
89		return false;
90		}*/
91
92	8953698	void MinisatSatSolver::toMinisatClause(SatClause& clause,
93		Minisat::vec<Minisat::Lit>& minisat_clause) {
94	30400052	for (unsigned i = 0; i < clause.size(); ++i) {
95	21446354	minisat_clause.push(toMinisatLit(clause[i]));
96		}
97	8953698	Assert(clause.size() == (unsigned)minisat_clause.size());
98	8953698	}
99
100		void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
101		SatClause& sat_clause) {
102		for (int i = 0; i < clause.size(); ++i) {
103		sat_clause.push_back(toSatLiteral(clause[i]));
104		}
105		Assert((unsigned)clause.size() == sat_clause.size());
106		}
107
108	15339	void MinisatSatSolver::initialize(context::Context* context,
109		TheoryProxy* theoryProxy,
110		context::UserContext* userContext,
111		ProofNodeManager* pnm)
112		{
113	15339	d_context = context;
114
115	15339	if (options().decision.decisionMode != options::DecisionMode::INTERNAL)
116		{
117	12758	verbose(1) << "minisat: Incremental solving is forced on (to avoid "
118		"variable elimination)"
119	12758	<< " unless using internal decision strategy." << std::endl;
120		}
121
122		// Create the solver
123	15339	d_minisat =
124		new Minisat::SimpSolver(theoryProxy,
125		d_context,
126		userContext,
127		pnm,
128	15339	options().base.incrementalSolving
129	15339	\|\| options().decision.decisionMode
130	15339	!= options::DecisionMode::INTERNAL);
131
132	15339	d_statistics.init(d_minisat);
133	15339	}
134
135		// Like initialize() above, but called just before each search when in
136		// incremental mode
137	20559	void MinisatSatSolver::setupOptions() {
138		// Copy options from cvc5 options structure into minisat, as appropriate
139
140		// Set up the verbosity
141	20559	d_minisat->verbosity = (options().base.verbosity > 0) ? 1 : -1;
142
143		// Set up the random decision parameters
144	20559	d_minisat->random_var_freq = options().prop.satRandomFreq;
145		// If 0, we use whatever we like (here, the Minisat default seed)
146	20559	if (options().prop.satRandomSeed != 0)
147		{
148	2	d_minisat->random_seed = double(options().prop.satRandomSeed);
149		}
150
151		// Give access to all possible options in the sat solver
152	20559	d_minisat->var_decay = options().prop.satVarDecay;
153	20559	d_minisat->clause_decay = options().prop.satClauseDecay;
154	20559	d_minisat->restart_first = options().prop.satRestartFirst;
155	20559	d_minisat->restart_inc = options().prop.satRestartInc;
156	20559	}
157
158	3720247	ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
159	7440494	Minisat::vec<Minisat::Lit> minisat_clause;
160	3720247	toMinisatClause(clause, minisat_clause);
161	3720247	ClauseId clause_id = ClauseIdError;
162		// FIXME: This relies on the invariant that when ok() is false
163		// the SAT solver does not add the clause (which is what Minisat currently does)
164	3720247	if (!ok()) {
165	6854	return ClauseIdUndef;
166		}
167	3713393	d_minisat->addClause(minisat_clause, removable, clause_id);
168		// FIXME: to be deleted when we kill old proof code for unsat cores
169	3713393	Assert(!options().smt.unsatCores \|\| options().smt.produceProofs
170		\|\| clause_id != ClauseIdError);
171	3713393	return clause_id;
172		}
173
174	1327051	SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
175	1327051	return d_minisat->newVar(true, true, isTheoryAtom, preRegister, canErase);
176		}
177
178		SatValue MinisatSatSolver::solve(unsigned long& resource) {
179		Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
180		setupOptions();
181		if(resource == 0) {
182		d_minisat->budgetOff();
183		} else {
184		d_minisat->setConfBudget(resource);
185		}
186		Minisat::vec<Minisat::Lit> empty;
187		unsigned long conflictsBefore = d_minisat->conflicts + d_minisat->resources_consumed;
188		SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
189		d_minisat->clearInterrupt();
190		resource = d_minisat->conflicts + d_minisat->resources_consumed - conflictsBefore;
191		Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
192		return result;
193		}
194
195	16846	SatValue MinisatSatSolver::solve() {
196	16846	setupOptions();
197	16846	d_minisat->budgetOff();
198	16846	SatValue result = toSatLiteralValue(d_minisat->solve());
199	16823	d_minisat->clearInterrupt();
200	16823	return result;
201		}
202
203	3713	SatValue MinisatSatSolver::solve(const std::vector<SatLiteral>& assumptions)
204		{
205	3713	setupOptions();
206	3713	d_minisat->budgetOff();
207
208	3713	d_assumptions.clear();
209	7426	Minisat::vec<Minisat::Lit> assumps;
210
211	53954	for (const SatLiteral& lit : assumptions)
212		{
213	50241	Minisat::Lit mlit = toMinisatLit(lit);
214	50241	assumps.push(mlit);
215	50241	d_assumptions.emplace(lit);
216		}
217
218	3713	SatValue result = toSatLiteralValue(d_minisat->solve(assumps));
219	3713	d_minisat->clearInterrupt();
220	7426	return result;
221		}
222
223	1409	void MinisatSatSolver::getUnsatAssumptions(
224		std::vector<SatLiteral>& unsat_assumptions)
225		{
226	8361	for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i)
227		{
228	6952	Minisat::Lit mlit = d_minisat->d_conflict[i];
229	6952	SatLiteral lit = ~toSatLiteral(mlit);
230	6952	if (d_assumptions.find(lit) != d_assumptions.end())
231		{
232	6952	unsat_assumptions.push_back(lit);
233		}
234		}
235	1409	}
236
237	3720247	bool MinisatSatSolver::ok() const {
238	3720247	return d_minisat->okay();
239		}
240
241		void MinisatSatSolver::interrupt() {
242		d_minisat->interrupt();
243		}
244
245	25531942	SatValue MinisatSatSolver::value(SatLiteral l) {
246	25531942	return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
247		}
248
249		SatValue MinisatSatSolver::modelValue(SatLiteral l){
250		return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
251		}
252
253		bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
254		return true;
255		}
256
257	72648	void MinisatSatSolver::requirePhase(SatLiteral lit) {
258	72648	Assert(!d_minisat->rnd_pol);
259	72648	Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl;
260	72648	SatVariable v = lit.getSatVariable();
261	72648	d_minisat->freezePolarity(v, lit.isNegated());
262	72648	}
263
264	171751	bool MinisatSatSolver::isDecision(SatVariable decn) const {
265	171751	return d_minisat->isDecision( decn );
266		}
267
268	8	int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
269		{
270	8	return d_minisat->level(v) + d_minisat->user_level(v);
271		}
272
273	8	int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const
274		{
275	8	return d_minisat->intro_level(v);
276		}
277
278	10762	SatProofManager* MinisatSatSolver::getProofManager()
279		{
280	10762	return d_minisat->getProofManager();
281		}
282
283	10064	std::shared_ptr<ProofNode> MinisatSatSolver::getProof()
284		{
285	10064	return d_minisat->getProof();
286		}
287
288		/** Incremental interface */
289
290	24391	unsigned MinisatSatSolver::getAssertionLevel() const {
291	24391	return d_minisat->getAssertionLevel();
292		}
293
294	4941	void MinisatSatSolver::push() {
295	4941	d_minisat->push();
296	4941	}
297
298	4941	void MinisatSatSolver::pop() {
299	4941	d_minisat->pop();
300	4941	}
301
302	20539	void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); }
303
304		/// Statistics for MinisatSatSolver
305
306	15339	MinisatSatSolver::Statistics::Statistics(StatisticsRegistry& registry)
307		: d_statStarts(registry.registerReference<int64_t>("sat::starts")),
308		d_statDecisions(registry.registerReference<int64_t>("sat::decisions")),
309		d_statRndDecisions(
310		registry.registerReference<int64_t>("sat::rnd_decisions")),
311		d_statPropagations(
312		registry.registerReference<int64_t>("sat::propagations")),
313		d_statConflicts(registry.registerReference<int64_t>("sat::conflicts")),
314		d_statClausesLiterals(
315		registry.registerReference<int64_t>("sat::clauses_literals")),
316		d_statLearntsLiterals(
317		registry.registerReference<int64_t>("sat::learnts_literals")),
318		d_statMaxLiterals(
319		registry.registerReference<int64_t>("sat::max_literals")),
320		d_statTotLiterals(
321	15339	registry.registerReference<int64_t>("sat::tot_literals"))
322		{
323	15339	}
324
325	15339	void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
326	15339	d_statStarts.set(minisat->starts);
327	15339	d_statDecisions.set(minisat->decisions);
328	15339	d_statRndDecisions.set(minisat->rnd_decisions);
329	15339	d_statPropagations.set(minisat->propagations);
330	15339	d_statConflicts.set(minisat->conflicts);
331	15339	d_statClausesLiterals.set(minisat->clauses_literals);
332	15339	d_statLearntsLiterals.set(minisat->learnts_literals);
333	15339	d_statMaxLiterals.set(minisat->max_literals);
334	15339	d_statTotLiterals.set(minisat->tot_literals);
335	15339	}
336	15334	void MinisatSatSolver::Statistics::deinit()
337		{
338	15334	d_statStarts.reset();
339	15334	d_statDecisions.reset();
340	15334	d_statRndDecisions.reset();
341	15334	d_statPropagations.reset();
342	15334	d_statConflicts.reset();
343	15334	d_statClausesLiterals.reset();
344	15334	d_statLearntsLiterals.reset();
345	15334	d_statMaxLiterals.reset();
346	15334	d_statTotLiterals.reset();
347	15334	}
348
349		} // namespace prop
350		} // namespace cvc5
351
352		namespace cvc5 {
353		template <>
354	28697	prop::SatLiteral toSatLiteral<cvc5::Minisat::Solver>(Minisat::Solver::TLit lit)
355		{
356	28697	return prop::MinisatSatSolver::toSatLiteral(lit);
357		}
358
359		template <>
360		void toSatClause<cvc5::Minisat::Solver>(
361		const cvc5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
362		{
363		prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
364		}
365
366	31137	} // namespace cvc5