Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_solver_bitblast.cpp	Lines:	1	185	0.5 %
Date:	2021-05-21	Branches:	2	778	0.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 {

/**
 * 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(BBSimple* 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. */
  BBSimple* 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 BBSimple(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_invalidateModelCache(s->getSatContext(), true),
      d_inSatMode(s->getSatContext(), false),
      d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
                : nullptr),
      d_factLiteralCache(s->getSatContext()),
      d_literalFactCache(s->getSatContext()),
      d_propagate(options::bitvectorPropagate())
{
  if (pnm != nullptr)
  {
    d_bvProofChecker.registerTo(pnm->getChecker());
  }

  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()));
}

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;
    }
  }

  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]);
  }

  d_invalidateModelCache.set(true);
  std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
                                            d_assumptions.end());
  prop::SatValue val = d_satSolver->solve(assumptions);
  d_inSatMode = val == prop::SatValue::SAT_VALUE_TRUE;
  Debug("bv-bitblast") << "d_inSatMode: " << d_inSatMode << std::endl;

  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.isDecision(fact) && val.getDecisionLevel(fact) == 0
      && val.getIntroLevel(fact) == 0)
  {
    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);
}

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

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

EqualityStatus BVSolverBitblast::getEqualityStatus(TNode a, TNode b)
{
  Debug("bv-bitblast") << "getEqualityStatus on " << a << " and " << b
                       << std::endl;
  if (!d_inSatMode)
  {
    Debug("bv-bitblast") << EQUALITY_UNKNOWN << std::endl;
    return EQUALITY_UNKNOWN;
  }
  Node value_a = getValue(a);
  Node value_b = getValue(b);

  if (value_a == value_b)
  {
    Debug("bv-bitblast") << EQUALITY_TRUE_IN_MODEL << std::endl;
    return EQUALITY_TRUE_IN_MODEL;
  }
  Debug("bv-bitblast") << EQUALITY_FALSE_IN_MODEL << std::endl;
  return EQUALITY_FALSE_IN_MODEL;
}

Node BVSolverBitblast::getValueFromSatSolver(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);
}

Node BVSolverBitblast::getValue(TNode node)
{
  if (d_invalidateModelCache.get())
  {
    d_modelCache.clear();
  }
  d_invalidateModelCache.set(false);

  std::vector<TNode> visit;

  TNode cur;
  visit.push_back(node);
  do
  {
    cur = visit.back();
    visit.pop_back();

    auto it = d_modelCache.find(cur);
    if (it != d_modelCache.end() && !it->second.isNull())
    {
      continue;
    }

    if (d_bitblaster->hasBBTerm(cur))
    {
      Node value = getValueFromSatSolver(cur, false);
      if (value.isConst())
      {
        d_modelCache[cur] = value;
        continue;
      }
    }
    if (Theory::isLeafOf(cur, theory::THEORY_BV))
    {
      Node value = getValueFromSatSolver(cur, true);
      d_modelCache[cur] = value;
      continue;
    }

    if (it == d_modelCache.end())
    {
      visit.push_back(cur);
      d_modelCache.emplace(cur, Node());
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
    else if (it->second.isNull())
    {
      NodeBuilder nb(cur.getKind());
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        nb << cur.getOperator();
      }

      std::unordered_map<Node, Node>::iterator iit;
      for (const TNode& child : cur)
      {
        iit = d_modelCache.find(child);
        Assert(iit != d_modelCache.end());
        Assert(iit->second.isConst());
        nb << iit->second;
      }
      it->second = Rewriter::rewrite(nb.constructNode());
    }
  } while (!visit.empty());

  auto it = d_modelCache.find(node);
  Assert(it != d_modelCache.end());
  return it->second;
}

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		* Bit-blasting registrar.
31		*
32		* The CnfStream calls preRegister() if it encounters a theory atom.
33		* This registrar bit-blasts given atom and remembers which bit-vector atoms
34		* were bit-blasted.
35		*
36		* This registrar is needed when --bitblast=eager is enabled.
37		*/
38		class BBRegistrar : public prop::Registrar
39		{
40		public:
41		BBRegistrar(BBSimple* bb) : d_bitblaster(bb) {}
42
43		void preRegister(Node n) override
44		{
45		if (d_registeredAtoms.find(n) != d_registeredAtoms.end())
46		{
47		return;
48		}
49		/* We are only interested in bit-vector atoms. */
50		if ((n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
51		\|\| n.getKind() == kind::BITVECTOR_ULT
52		\|\| n.getKind() == kind::BITVECTOR_ULE
53		\|\| n.getKind() == kind::BITVECTOR_SLT
54		\|\| n.getKind() == kind::BITVECTOR_SLE)
55		{
56		d_registeredAtoms.insert(n);
57		d_bitblaster->bbAtom(n);
58		}
59		}
60
61		std::unordered_set<TNode>& getRegisteredAtoms() { return d_registeredAtoms; }
62
63		private:
64		/** The bitblaster used. */
65		BBSimple* d_bitblaster;
66
67		/** Stores bit-vector atoms encounterd on preRegister(). */
68		std::unordered_set<TNode> d_registeredAtoms;
69		};
70
71		BVSolverBitblast::BVSolverBitblast(TheoryState* s,
72		TheoryInferenceManager& inferMgr,
73		ProofNodeManager* pnm)
74		: BVSolver(*s, inferMgr),
75		d_bitblaster(new BBSimple(s)),
76		d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
77		d_nullContext(new context::Context()),
78		d_bbFacts(s->getSatContext()),
79		d_bbInputFacts(s->getSatContext()),
80		d_assumptions(s->getSatContext()),
81		d_assertions(s->getSatContext()),
82		d_invalidateModelCache(s->getSatContext(), true),
83		d_inSatMode(s->getSatContext(), false),
84		d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
85		: nullptr),
86		d_factLiteralCache(s->getSatContext()),
87		d_literalFactCache(s->getSatContext()),
88		d_propagate(options::bitvectorPropagate())
89		{
90		if (pnm != nullptr)
91		{
92		d_bvProofChecker.registerTo(pnm->getChecker());
93		}
94
95		switch (options::bvSatSolver())
96		{
97		case options::SatSolverMode::CRYPTOMINISAT:
98		d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
99		smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
100		break;
101		default:
102		d_satSolver.reset(prop::SatSolverFactory::createCadical(
103		smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
104		}
105		d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
106		d_bbRegistrar.get(),
107		d_nullContext.get(),
108		nullptr,
109		smt::currentResourceManager()));
110		}
111
112		void BVSolverBitblast::postCheck(Theory::Effort level)
113		{
114		if (level != Theory::Effort::EFFORT_FULL)
115		{
116		/* Do bit-level propagation only if the SAT solver supports it. */
117		if (!d_propagate \|\| !d_satSolver->setPropagateOnly())
118		{
119		return;
120		}
121		}
122
123		NodeManager* nm = NodeManager::currentNM();
124
125		/* Process input assertions bit-blast queue. */
126		while (!d_bbInputFacts.empty())
127		{
128		Node fact = d_bbInputFacts.front();
129		d_bbInputFacts.pop();
130		/* Bit-blast fact and cache literal. */
131		if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
132		{
133		if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
134		{
135		handleEagerAtom(fact, true);
136		}
137		else
138		{
139		d_bitblaster->bbAtom(fact);
140		Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
141		d_cnfStream->convertAndAssert(bb_fact, false, false);
142		}
143		}
144		d_assertions.push_back(fact);
145		}
146
147		/* Process bit-blast queue and store SAT literals. */
148		while (!d_bbFacts.empty())
149		{
150		Node fact = d_bbFacts.front();
151		d_bbFacts.pop();
152		/* Bit-blast fact and cache literal. */
153		if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
154		{
155		prop::SatLiteral lit;
156		if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
157		{
158		handleEagerAtom(fact, false);
159		lit = d_cnfStream->getLiteral(fact[0]);
160		}
161		else
162		{
163		d_bitblaster->bbAtom(fact);
164		Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
165		d_cnfStream->ensureLiteral(bb_fact);
166		lit = d_cnfStream->getLiteral(bb_fact);
167		}
168		d_factLiteralCache[fact] = lit;
169		d_literalFactCache[lit] = fact;
170		}
171		d_assumptions.push_back(d_factLiteralCache[fact]);
172		}
173
174		d_invalidateModelCache.set(true);
175		std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
176		d_assumptions.end());
177		prop::SatValue val = d_satSolver->solve(assumptions);
178		d_inSatMode = val == prop::SatValue::SAT_VALUE_TRUE;
179		Debug("bv-bitblast") << "d_inSatMode: " << d_inSatMode << std::endl;
180
181		if (val == prop::SatValue::SAT_VALUE_FALSE)
182		{
183		std::vector<prop::SatLiteral> unsat_assumptions;
184		d_satSolver->getUnsatAssumptions(unsat_assumptions);
185
186		Node conflict;
187		// Unsat assumptions produce conflict.
188		if (unsat_assumptions.size() > 0)
189		{
190		std::vector<Node> conf;
191		for (const prop::SatLiteral& lit : unsat_assumptions)
192		{
193		conf.push_back(d_literalFactCache[lit]);
194		Debug("bv-bitblast")
195		<< "unsat assumption (" << lit << "): " << conf.back() << std::endl;
196		}
197		conflict = nm->mkAnd(conf);
198		}
199		else // Input assertions produce conflict.
200		{
201		std::vector<Node> assertions(d_assertions.begin(), d_assertions.end());
202		conflict = nm->mkAnd(assertions);
203		}
204		d_im.conflict(conflict, InferenceId::BV_BITBLAST_CONFLICT);
205		}
206		}
207
208		bool BVSolverBitblast::preNotifyFact(
209		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
210		{
211		Valuation& val = d_state.getValuation();
212
213		/**
214		* Check whether `fact` is an input assertion on user-level 0.
215		*
216		* If this is the case we can assert `fact` to the SAT solver instead of
217		* using assumptions.
218		*/
219		if (options::bvAssertInput() && val.isSatLiteral(fact)
220		&& !val.isDecision(fact) && val.getDecisionLevel(fact) == 0
221		&& val.getIntroLevel(fact) == 0)
222		{
223		d_bbInputFacts.push_back(fact);
224		}
225		else
226		{
227		d_bbFacts.push_back(fact);
228		}
229
230		return false; // Return false to enable equality engine reasoning in Theory.
231		}
232
233		TrustNode BVSolverBitblast::explain(TNode n)
234		{
235		Debug("bv-bitblast") << "explain called on " << n << std::endl;
236		return d_im.explainLit(n);
237		}
238
239		bool BVSolverBitblast::collectModelValues(TheoryModel* m,
240		const std::set<Node>& termSet)
241		{
242		for (const auto& term : termSet)
243		{
244		if (!d_bitblaster->isVariable(term))
245		{
246		continue;
247		}
248
249		Node value = getValueFromSatSolver(term, true);
250		Assert(value.isConst());
251		if (!m->assertEquality(term, value, true))
252		{
253		return false;
254		}
255		}
256		return true;
257		}
258
259		EqualityStatus BVSolverBitblast::getEqualityStatus(TNode a, TNode b)
260		{
261		Debug("bv-bitblast") << "getEqualityStatus on " << a << " and " << b
262		<< std::endl;
263		if (!d_inSatMode)
264		{
265		Debug("bv-bitblast") << EQUALITY_UNKNOWN << std::endl;
266		return EQUALITY_UNKNOWN;
267		}
268		Node value_a = getValue(a);
269		Node value_b = getValue(b);
270
271		if (value_a == value_b)
272		{
273		Debug("bv-bitblast") << EQUALITY_TRUE_IN_MODEL << std::endl;
274		return EQUALITY_TRUE_IN_MODEL;
275		}
276		Debug("bv-bitblast") << EQUALITY_FALSE_IN_MODEL << std::endl;
277		return EQUALITY_FALSE_IN_MODEL;
278		}
279
280		Node BVSolverBitblast::getValueFromSatSolver(TNode node, bool initialize)
281		{
282		if (node.isConst())
283		{
284		return node;
285		}
286
287		if (!d_bitblaster->hasBBTerm(node))
288		{
289		return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
290		}
291
292		std::vector<Node> bits;
293		d_bitblaster->getBBTerm(node, bits);
294		Integer value(0), one(1), zero(0), bit;
295		for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
296		{
297		if (d_cnfStream->hasLiteral(bits[j]))
298		{
299		prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
300		prop::SatValue val = d_satSolver->modelValue(lit);
301		bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
302		}
303		else
304		{
305		if (!initialize) return Node();
306		bit = zero;
307		}
308		value = value * 2 + bit;
309		}
310		return utils::mkConst(bits.size(), value);
311		}
312
313		Node BVSolverBitblast::getValue(TNode node)
314		{
315		if (d_invalidateModelCache.get())
316		{
317		d_modelCache.clear();
318		}
319		d_invalidateModelCache.set(false);
320
321		std::vector<TNode> visit;
322
323		TNode cur;
324		visit.push_back(node);
325		do
326		{
327		cur = visit.back();
328		visit.pop_back();
329
330		auto it = d_modelCache.find(cur);
331		if (it != d_modelCache.end() && !it->second.isNull())
332		{
333		continue;
334		}
335
336		if (d_bitblaster->hasBBTerm(cur))
337		{
338		Node value = getValueFromSatSolver(cur, false);
339		if (value.isConst())
340		{
341		d_modelCache[cur] = value;
342		continue;
343		}
344		}
345		if (Theory::isLeafOf(cur, theory::THEORY_BV))
346		{
347		Node value = getValueFromSatSolver(cur, true);
348		d_modelCache[cur] = value;
349		continue;
350		}
351
352		if (it == d_modelCache.end())
353		{
354		visit.push_back(cur);
355		d_modelCache.emplace(cur, Node());
356		visit.insert(visit.end(), cur.begin(), cur.end());
357		}
358		else if (it->second.isNull())
359		{
360		NodeBuilder nb(cur.getKind());
361		if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
362		{
363		nb << cur.getOperator();
364		}
365
366		std::unordered_map<Node, Node>::iterator iit;
367		for (const TNode& child : cur)
368		{
369		iit = d_modelCache.find(child);
370		Assert(iit != d_modelCache.end());
371		Assert(iit->second.isConst());
372		nb << iit->second;
373		}
374		it->second = Rewriter::rewrite(nb.constructNode());
375		}
376		} while (!visit.empty());
377
378		auto it = d_modelCache.find(node);
379		Assert(it != d_modelCache.end());
380		return it->second;
381		}
382
383		void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact)
384		{
385		Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
386
387		if (assertFact)
388		{
389		d_cnfStream->convertAndAssert(fact[0], false, false);
390		}
391		else
392		{
393		d_cnfStream->ensureLiteral(fact[0]);
394		}
395
396		/* convertAndAssert() does not make the connection between the bit-vector
397		* atom and it's bit-blasted form (it only calls preRegister() from the
398		* registrar). Thus, we add the equalities now. */
399		auto& registeredAtoms = d_bbRegistrar->getRegisteredAtoms();
400		for (auto atom : registeredAtoms)
401		{
402		Node bb_atom = d_bitblaster->getStoredBBAtom(atom);
403		d_cnfStream->convertAndAssert(atom.eqNode(bb_atom), false, false);
404		}
405		// Clear cache since we only need to do this once per bit-blasted atom.
406		registeredAtoms.clear();
407		}
408
409		} // namespace bv
410		} // namespace theory
411	27735	} // namespace cvc5