Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_solver_bitblast.cpp	Lines:	157	165	95.2 %
Date:	2021-08-14	Branches:	293	606	48.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner, Gereon Kremer, Andres Noetzli
 *
 * 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.
 * ****************************************************************************
 *
 * Bit-blasting solver that supports multiple SAT backends.
 */

#include "theory/bv/bv_solver_bitblast.h"

#include "options/bv_options.h"
#include "prop/sat_solver_factory.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"

namespace cvc5 {
namespace theory {
namespace bv {

/**
 * Notifies the BV solver when assertions were reset.
 *
 * This class is notified after every user-context pop and maintains a flag
 * that indicates whether assertions have been reset. If the user-context level
 * reaches level 0 it means that the assertions were reset.
 */
class NotifyResetAssertions : public context::ContextNotifyObj
{
 public:
  NotifyResetAssertions(context::Context* c)
      : context::ContextNotifyObj(c, false),
        d_context(c),
        d_doneResetAssertions(false)
  {
  }

  bool doneResetAssertions() { return d_doneResetAssertions; }

  void reset() { d_doneResetAssertions = false; }

 protected:
  void contextNotifyPop() override
  {
    // If the user-context level reaches 0 it means that reset-assertions was
    // called.
    if (d_context->getLevel() == 0)
    {
      d_doneResetAssertions = true;
    }
  }

 private:
  /** The user-context. */
  context::Context* d_context;

  /** Flag to notify whether reset assertions was called. */
  bool d_doneResetAssertions;
};

/**
 * Bit-blasting registrar.
 *
 * The CnfStream calls preRegister() if it encounters a theory atom.
 * This registrar bit-blasts given atom and remembers which bit-vector atoms
 * were bit-blasted.
 *
 * This registrar is needed when --bitblast=eager is enabled.
 */
class BBRegistrar : public prop::Registrar
{
 public:
  BBRegistrar(NodeBitblaster* bb) : d_bitblaster(bb) {}

  void preRegister(Node n) override
  {
    if (d_registeredAtoms.find(n) != d_registeredAtoms.end())
    {
      return;
    }
    /* We are only interested in bit-vector atoms. */
    if ((n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
        || n.getKind() == kind::BITVECTOR_ULT
        || n.getKind() == kind::BITVECTOR_ULE
        || n.getKind() == kind::BITVECTOR_SLT
        || n.getKind() == kind::BITVECTOR_SLE)
    {
      d_registeredAtoms.insert(n);
      d_bitblaster->bbAtom(n);
    }
  }

  std::unordered_set<TNode>& getRegisteredAtoms() { return d_registeredAtoms; }

 private:
  /** The bitblaster used. */
  NodeBitblaster* d_bitblaster;

  /** Stores bit-vector atoms encounterd on preRegister(). */
  std::unordered_set<TNode> d_registeredAtoms;
};

BVSolverBitblast::BVSolverBitblast(TheoryState* s,
                                   TheoryInferenceManager& inferMgr,
                                   ProofNodeManager* pnm)
    : BVSolver(*s, inferMgr),
      d_bitblaster(new NodeBitblaster(s)),
      d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
      d_nullContext(new context::Context()),
      d_bbFacts(s->getSatContext()),
      d_bbInputFacts(s->getSatContext()),
      d_assumptions(s->getSatContext()),
      d_assertions(s->getSatContext()),
      d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
                : nullptr),
      d_factLiteralCache(s->getSatContext()),
      d_literalFactCache(s->getSatContext()),
      d_propagate(options::bitvectorPropagate()),
      d_resetNotify(new NotifyResetAssertions(s->getUserContext()))
{
  if (pnm != nullptr)
  {
    d_bvProofChecker.registerTo(pnm->getChecker());
  }

  initSatSolver();
}

void BVSolverBitblast::postCheck(Theory::Effort level)
{
  if (level != Theory::Effort::EFFORT_FULL)
  {
    /* Do bit-level propagation only if the SAT solver supports it. */
    if (!d_propagate || !d_satSolver->setPropagateOnly())
    {
      return;
    }
  }

  // If we permanently added assertions to the SAT solver and the assertions
  // were reset, we have to reset the SAT solver and the CNF stream.
  if (options::bvAssertInput() && d_resetNotify->doneResetAssertions())
  {
    d_satSolver.reset(nullptr);
    d_cnfStream.reset(nullptr);
    initSatSolver();
    d_resetNotify->reset();
  }

  NodeManager* nm = NodeManager::currentNM();

  /* Process input assertions bit-blast queue. */
  while (!d_bbInputFacts.empty())
  {
    Node fact = d_bbInputFacts.front();
    d_bbInputFacts.pop();
    /* Bit-blast fact and cache literal. */
    if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
    {
      if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
      {
        handleEagerAtom(fact, true);
      }
      else
      {
        d_bitblaster->bbAtom(fact);
        Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
        d_cnfStream->convertAndAssert(bb_fact, false, false);
      }
    }
    d_assertions.push_back(fact);
  }

  /* Process bit-blast queue and store SAT literals. */
  while (!d_bbFacts.empty())
  {
    Node fact = d_bbFacts.front();
    d_bbFacts.pop();
    /* Bit-blast fact and cache literal. */
    if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
    {
      prop::SatLiteral lit;
      if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
      {
        handleEagerAtom(fact, false);
        lit = d_cnfStream->getLiteral(fact[0]);
      }
      else
      {
        d_bitblaster->bbAtom(fact);
        Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
        d_cnfStream->ensureLiteral(bb_fact);
        lit = d_cnfStream->getLiteral(bb_fact);
      }
      d_factLiteralCache[fact] = lit;
      d_literalFactCache[lit] = fact;
    }
    d_assumptions.push_back(d_factLiteralCache[fact]);
  }

  std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
                                            d_assumptions.end());
  prop::SatValue val = d_satSolver->solve(assumptions);

  if (val == prop::SatValue::SAT_VALUE_FALSE)
  {
    std::vector<prop::SatLiteral> unsat_assumptions;
    d_satSolver->getUnsatAssumptions(unsat_assumptions);

    Node conflict;
    // Unsat assumptions produce conflict.
    if (unsat_assumptions.size() > 0)
    {
      std::vector<Node> conf;
      for (const prop::SatLiteral& lit : unsat_assumptions)
      {
        conf.push_back(d_literalFactCache[lit]);
        Debug("bv-bitblast")
            << "unsat assumption (" << lit << "): " << conf.back() << std::endl;
      }
      conflict = nm->mkAnd(conf);
    }
    else  // Input assertions produce conflict.
    {
      std::vector<Node> assertions(d_assertions.begin(), d_assertions.end());
      conflict = nm->mkAnd(assertions);
    }
    d_im.conflict(conflict, InferenceId::BV_BITBLAST_CONFLICT);
  }
}

bool BVSolverBitblast::preNotifyFact(
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
{
  Valuation& val = d_state.getValuation();

  /**
   * Check whether `fact` is an input assertion on user-level 0.
   *
   * If this is the case we can assert `fact` to the SAT solver instead of
   * using assumptions.
   */
  if (options::bvAssertInput() && val.isSatLiteral(fact)
      && val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0)
  {
    Assert(!val.isDecision(fact));
    d_bbInputFacts.push_back(fact);
  }
  else
  {
    d_bbFacts.push_back(fact);
  }

  return false;  // Return false to enable equality engine reasoning in Theory.
}

TrustNode BVSolverBitblast::explain(TNode n)
{
  Debug("bv-bitblast") << "explain called on " << n << std::endl;
  return d_im.explainLit(n);
}

void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet)
{
  /* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain
   * equalities. As a result, these equalities are not handled by the equality
   * engine and terms below these equalities do not appear in `termSet`.
   * We need to make sure that we compute model values for all relevant terms
   * in BitblastMode::EAGER and therefore add all variables from the
   * bit-blaster to `termSet`.
   */
  if (options::bitblastMode() == options::BitblastMode::EAGER)
  {
    d_bitblaster->computeRelevantTerms(termSet);
  }
}

bool BVSolverBitblast::collectModelValues(TheoryModel* m,
                                          const std::set<Node>& termSet)
{
  for (const auto& term : termSet)
  {
    if (!d_bitblaster->isVariable(term))
    {
      continue;
    }

    Node value = getValue(term, true);
    Assert(value.isConst());
    if (!m->assertEquality(term, value, true))
    {
      return false;
    }
  }

  // In eager bitblast mode we also have to collect the model values for
  // Boolean variables in the CNF stream.
  if (options::bitblastMode() == options::BitblastMode::EAGER)
  {
    NodeManager* nm = NodeManager::currentNM();
    std::vector<TNode> vars;
    d_cnfStream->getBooleanVariables(vars);
    for (TNode var : vars)
    {
      Assert(d_cnfStream->hasLiteral(var));
      prop::SatLiteral bit = d_cnfStream->getLiteral(var);
      prop::SatValue value = d_satSolver->value(bit);
      Assert(value != prop::SAT_VALUE_UNKNOWN);
      if (!m->assertEquality(
              var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true))
      {
        return false;
      }
    }
  }

  return true;
}

void BVSolverBitblast::initSatSolver()
{
  switch (options::bvSatSolver())
  {
    case options::SatSolverMode::CRYPTOMINISAT:
      d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
      break;
    default:
      d_satSolver.reset(prop::SatSolverFactory::createCadical(
          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
  }
  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
                                        d_bbRegistrar.get(),
                                        d_nullContext.get(),
                                        nullptr,
                                        smt::currentResourceManager(),
                                        prop::FormulaLitPolicy::INTERNAL,
                                        "theory::bv::BVSolverBitblast"));
}

Node BVSolverBitblast::getValue(TNode node, bool initialize)
{
  if (node.isConst())
  {
    return node;
  }

  if (!d_bitblaster->hasBBTerm(node))
  {
    return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
  }

  std::vector<Node> bits;
  d_bitblaster->getBBTerm(node, bits);
  Integer value(0), one(1), zero(0), bit;
  for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
  {
    if (d_cnfStream->hasLiteral(bits[j]))
    {
      prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
      prop::SatValue val = d_satSolver->modelValue(lit);
      bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
    }
    else
    {
      if (!initialize) return Node();
      bit = zero;
    }
    value = value * 2 + bit;
  }
  return utils::mkConst(bits.size(), value);
}

void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact)
{
  Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);

  if (assertFact)
  {
    d_cnfStream->convertAndAssert(fact[0], false, false);
  }
  else
  {
    d_cnfStream->ensureLiteral(fact[0]);
  }

  /* convertAndAssert() does not make the connection between the bit-vector
   * atom and it's bit-blasted form (it only calls preRegister() from the
   * registrar). Thus, we add the equalities now. */
  auto& registeredAtoms = d_bbRegistrar->getRegisteredAtoms();
  for (auto atom : registeredAtoms)
  {
    Node bb_atom = d_bitblaster->getStoredBBAtom(atom);
    d_cnfStream->convertAndAssert(atom.eqNode(bb_atom), false, false);
  }
  // Clear cache since we only need to do this once per bit-blasted atom.
  registeredAtoms.clear();
}

}  // namespace bv
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mathias Preiner, Gereon Kremer, Andres Noetzli
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		* Bit-blasting solver that supports multiple SAT backends.
14		*/
15
16		#include "theory/bv/bv_solver_bitblast.h"
17
18		#include "options/bv_options.h"
19		#include "prop/sat_solver_factory.h"
20		#include "smt/smt_statistics_registry.h"
21		#include "theory/bv/theory_bv.h"
22		#include "theory/bv/theory_bv_utils.h"
23		#include "theory/theory_model.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace bv {
28
29		/**
30		* Notifies the BV solver when assertions were reset.
31		*
32		* This class is notified after every user-context pop and maintains a flag
33		* that indicates whether assertions have been reset. If the user-context level
34		* reaches level 0 it means that the assertions were reset.
35		*/
36	12200	class NotifyResetAssertions : public context::ContextNotifyObj
37		{
38		public:
39	6100	NotifyResetAssertions(context::Context* c)
40	6100	: context::ContextNotifyObj(c, false),
41		d_context(c),
42	6100	d_doneResetAssertions(false)
43		{
44	6100	}
45
46	8	bool doneResetAssertions() { return d_doneResetAssertions; }
47
48	2	void reset() { d_doneResetAssertions = false; }
49
50		protected:
51	9307	void contextNotifyPop() override
52		{
53		// If the user-context level reaches 0 it means that reset-assertions was
54		// called.
55	9307	if (d_context->getLevel() == 0)
56		{
57	6145	d_doneResetAssertions = true;
58		}
59	9307	}
60
61		private:
62		/** The user-context. */
63		context::Context* d_context;
64
65		/** Flag to notify whether reset assertions was called. */
66		bool d_doneResetAssertions;
67		};
68
69		/**
70		* Bit-blasting registrar.
71		*
72		* The CnfStream calls preRegister() if it encounters a theory atom.
73		* This registrar bit-blasts given atom and remembers which bit-vector atoms
74		* were bit-blasted.
75		*
76		* This registrar is needed when --bitblast=eager is enabled.
77		*/
78	12200	class BBRegistrar : public prop::Registrar
79		{
80		public:
81	6100	BBRegistrar(NodeBitblaster* bb) : d_bitblaster(bb) {}
82
83	149451	void preRegister(Node n) override
84		{
85	149451	if (d_registeredAtoms.find(n) != d_registeredAtoms.end())
86		{
87		return;
88		}
89		/* We are only interested in bit-vector atoms. */
90	299087	if ((n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
91	149266	\|\| n.getKind() == kind::BITVECTOR_ULT
92	149211	\|\| n.getKind() == kind::BITVECTOR_ULE
93	149211	\|\| n.getKind() == kind::BITVECTOR_SLT
94	448113	\|\| n.getKind() == kind::BITVECTOR_SLE)
95		{
96	240	d_registeredAtoms.insert(n);
97	240	d_bitblaster->bbAtom(n);
98		}
99		}
100
101	141	std::unordered_set<TNode>& getRegisteredAtoms() { return d_registeredAtoms; }
102
103		private:
104		/** The bitblaster used. */
105		NodeBitblaster* d_bitblaster;
106
107		/** Stores bit-vector atoms encounterd on preRegister(). */
108		std::unordered_set<TNode> d_registeredAtoms;
109		};
110
111	6100	BVSolverBitblast::BVSolverBitblast(TheoryState* s,
112		TheoryInferenceManager& inferMgr,
113	6100	ProofNodeManager* pnm)
114		: BVSolver(*s, inferMgr),
115	6100	d_bitblaster(new NodeBitblaster(s)),
116	6100	d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
117	6100	d_nullContext(new context::Context()),
118		d_bbFacts(s->getSatContext()),
119		d_bbInputFacts(s->getSatContext()),
120		d_assumptions(s->getSatContext()),
121		d_assertions(s->getSatContext()),
122	20	d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
123		: nullptr),
124		d_factLiteralCache(s->getSatContext()),
125		d_literalFactCache(s->getSatContext()),
126	6100	d_propagate(options::bitvectorPropagate()),
127	30520	d_resetNotify(new NotifyResetAssertions(s->getUserContext()))
128		{
129	6100	if (pnm != nullptr)
130		{
131	10	d_bvProofChecker.registerTo(pnm->getChecker());
132		}
133
134	6100	initSatSolver();
135	6100	}
136
137	728880	void BVSolverBitblast::postCheck(Theory::Effort level)
138		{
139	728880	if (level != Theory::Effort::EFFORT_FULL)
140		{
141		/* Do bit-level propagation only if the SAT solver supports it. */
142	695592	if (!d_propagate \|\| !d_satSolver->setPropagateOnly())
143		{
144	695592	return;
145		}
146		}
147
148		// If we permanently added assertions to the SAT solver and the assertions
149		// were reset, we have to reset the SAT solver and the CNF stream.
150	33288	if (options::bvAssertInput() && d_resetNotify->doneResetAssertions())
151		{
152	2	d_satSolver.reset(nullptr);
153	2	d_cnfStream.reset(nullptr);
154	2	initSatSolver();
155	2	d_resetNotify->reset();
156		}
157
158	33288	NodeManager* nm = NodeManager::currentNM();
159
160		/* Process input assertions bit-blast queue. */
161	33304	while (!d_bbInputFacts.empty())
162		{
163	16	Node fact = d_bbInputFacts.front();
164	8	d_bbInputFacts.pop();
165		/* Bit-blast fact and cache literal. */
166	8	if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
167		{
168	8	if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
169		{
170		handleEagerAtom(fact, true);
171		}
172		else
173		{
174	8	d_bitblaster->bbAtom(fact);
175	16	Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
176	8	d_cnfStream->convertAndAssert(bb_fact, false, false);
177		}
178		}
179	8	d_assertions.push_back(fact);
180		}
181
182		/* Process bit-blast queue and store SAT literals. */
183	5073588	while (!d_bbFacts.empty())
184		{
185	5040300	Node fact = d_bbFacts.front();
186	2520150	d_bbFacts.pop();
187		/* Bit-blast fact and cache literal. */
188	2520150	if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
189		{
190	2520150	prop::SatLiteral lit;
191	2520150	if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
192		{
193	141	handleEagerAtom(fact, false);
194	141	lit = d_cnfStream->getLiteral(fact[0]);
195		}
196		else
197		{
198	2520009	d_bitblaster->bbAtom(fact);
199	5040018	Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
200	2520009	d_cnfStream->ensureLiteral(bb_fact);
201	2520009	lit = d_cnfStream->getLiteral(bb_fact);
202		}
203	2520150	d_factLiteralCache[fact] = lit;
204	2520150	d_literalFactCache[lit] = fact;
205		}
206	2520150	d_assumptions.push_back(d_factLiteralCache[fact]);
207		}
208
209		std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
210	66576	d_assumptions.end());
211	33288	prop::SatValue val = d_satSolver->solve(assumptions);
212
213	33288	if (val == prop::SatValue::SAT_VALUE_FALSE)
214		{
215	28456	std::vector<prop::SatLiteral> unsat_assumptions;
216	14228	d_satSolver->getUnsatAssumptions(unsat_assumptions);
217
218	28456	Node conflict;
219		// Unsat assumptions produce conflict.
220	14228	if (unsat_assumptions.size() > 0)
221		{
222	28456	std::vector<Node> conf;
223	123845	for (const prop::SatLiteral& lit : unsat_assumptions)
224		{
225	109617	conf.push_back(d_literalFactCache[lit]);
226	219234	Debug("bv-bitblast")
227	109617	<< "unsat assumption (" << lit << "): " << conf.back() << std::endl;
228		}
229	14228	conflict = nm->mkAnd(conf);
230		}
231		else // Input assertions produce conflict.
232		{
233		std::vector<Node> assertions(d_assertions.begin(), d_assertions.end());
234		conflict = nm->mkAnd(assertions);
235		}
236	14228	d_im.conflict(conflict, InferenceId::BV_BITBLAST_CONFLICT);
237		}
238		}
239
240	1210725	bool BVSolverBitblast::preNotifyFact(
241		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
242		{
243	1210725	Valuation& val = d_state.getValuation();
244
245		/**
246		* Check whether `fact` is an input assertion on user-level 0.
247		*
248		* If this is the case we can assert `fact` to the SAT solver instead of
249		* using assumptions.
250		*/
251	2421466	if (options::bvAssertInput() && val.isSatLiteral(fact)
252	2421466	&& val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0)
253		{
254	8	Assert(!val.isDecision(fact));
255	8	d_bbInputFacts.push_back(fact);
256		}
257		else
258		{
259	1210717	d_bbFacts.push_back(fact);
260		}
261
262	1210725	return false; // Return false to enable equality engine reasoning in Theory.
263		}
264
265	4785	TrustNode BVSolverBitblast::explain(TNode n)
266		{
267	4785	Debug("bv-bitblast") << "explain called on " << n << std::endl;
268	4785	return d_im.explainLit(n);
269		}
270
271	6183	void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet)
272		{
273		/* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain
274		* equalities. As a result, these equalities are not handled by the equality
275		* engine and terms below these equalities do not appear in `termSet`.
276		* We need to make sure that we compute model values for all relevant terms
277		* in BitblastMode::EAGER and therefore add all variables from the
278		* bit-blaster to `termSet`.
279		*/
280	6183	if (options::bitblastMode() == options::BitblastMode::EAGER)
281		{
282	11	d_bitblaster->computeRelevantTerms(termSet);
283		}
284	6183	}
285
286	6183	bool BVSolverBitblast::collectModelValues(TheoryModel* m,
287		const std::set<Node>& termSet)
288		{
289	183159	for (const auto& term : termSet)
290		{
291	176976	if (!d_bitblaster->isVariable(term))
292		{
293	149912	continue;
294		}
295
296	54128	Node value = getValue(term, true);
297	27064	Assert(value.isConst());
298	27064	if (!m->assertEquality(term, value, true))
299		{
300		return false;
301		}
302		}
303
304		// In eager bitblast mode we also have to collect the model values for
305		// Boolean variables in the CNF stream.
306	6183	if (options::bitblastMode() == options::BitblastMode::EAGER)
307		{
308	11	NodeManager* nm = NodeManager::currentNM();
309	22	std::vector<TNode> vars;
310	11	d_cnfStream->getBooleanVariables(vars);
311	17	for (TNode var : vars)
312		{
313	6	Assert(d_cnfStream->hasLiteral(var));
314	6	prop::SatLiteral bit = d_cnfStream->getLiteral(var);
315	6	prop::SatValue value = d_satSolver->value(bit);
316	6	Assert(value != prop::SAT_VALUE_UNKNOWN);
317	12	if (!m->assertEquality(
318	12	var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true))
319		{
320		return false;
321		}
322		}
323		}
324
325	6183	return true;
326		}
327
328	6102	void BVSolverBitblast::initSatSolver()
329		{
330	6102	switch (options::bvSatSolver())
331		{
332	13	case options::SatSolverMode::CRYPTOMINISAT:
333	13	d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
334		smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
335	13	break;
336	6089	default:
337	6089	d_satSolver.reset(prop::SatSolverFactory::createCadical(
338		smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
339		}
340	18306	d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
341	6102	d_bbRegistrar.get(),
342	6102	d_nullContext.get(),
343		nullptr,
344	6102	smt::currentResourceManager(),
345		prop::FormulaLitPolicy::INTERNAL,
346	6102	"theory::bv::BVSolverBitblast"));
347	6102	}
348
349	28162	Node BVSolverBitblast::getValue(TNode node, bool initialize)
350		{
351	28162	if (node.isConst())
352		{
353		return node;
354		}
355
356	28162	if (!d_bitblaster->hasBBTerm(node))
357		{
358	634	return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
359		}
360
361	55056	std::vector<Node> bits;
362	27528	d_bitblaster->getBBTerm(node, bits);
363	55056	Integer value(0), one(1), zero(0), bit;
364	608077	for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
365		{
366	580641	if (d_cnfStream->hasLiteral(bits[j]))
367		{
368	574408	prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
369	574408	prop::SatValue val = d_satSolver->modelValue(lit);
370	574408	bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
371		}
372		else
373		{
374	6233	if (!initialize) return Node();
375	6141	bit = zero;
376		}
377	580549	value = value * 2 + bit;
378		}
379	27436	return utils::mkConst(bits.size(), value);
380		}
381
382	141	void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact)
383		{
384	141	Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
385
386	141	if (assertFact)
387		{
388		d_cnfStream->convertAndAssert(fact[0], false, false);
389		}
390		else
391		{
392	141	d_cnfStream->ensureLiteral(fact[0]);
393		}
394
395		/* convertAndAssert() does not make the connection between the bit-vector
396		* atom and it's bit-blasted form (it only calls preRegister() from the
397		* registrar). Thus, we add the equalities now. */
398	141	auto& registeredAtoms = d_bbRegistrar->getRegisteredAtoms();
399	381	for (auto atom : registeredAtoms)
400		{
401	480	Node bb_atom = d_bitblaster->getStoredBBAtom(atom);
402	240	d_cnfStream->convertAndAssert(atom.eqNode(bb_atom), false, false);
403		}
404		// Clear cache since we only need to do this once per bit-blasted atom.
405	141	registeredAtoms.clear();
406	141	}
407
408		} // namespace bv
409		} // namespace theory
410	29340	} // namespace cvc5