Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_subtheory_bitblast.cpp	Lines:	26	142	18.3 %
Date:	2021-09-14	Branches:	41	452	9.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Liana Hadarean, Aina Niemetz, Dejan Jovanovic
 *
 * 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.
 * ****************************************************************************
 *
 * Algebraic solver.
 */

#include "theory/bv/bv_subtheory_bitblast.h"

#include "decision/decision_attributes.h"
#include "options/bv_options.h"
#include "options/decision_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/abstraction.h"
#include "theory/bv/bitblast/lazy_bitblaster.h"
#include "theory/bv/bv_quick_check.h"
#include "theory/bv/bv_solver_layered.h"
#include "theory/bv/theory_bv_utils.h"

using namespace std;
using namespace cvc5::context;

namespace cvc5 {
namespace theory {
namespace bv {

BitblastSolver::BitblastSolver(context::Context* c, BVSolverLayered* bv)
    : SubtheorySolver(c, bv),
      d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
      d_bitblastQueue(c),
      d_statistics(),
      d_validModelCache(c, true),
      d_lemmaAtomsQueue(c),
      d_useSatPropagation(options::bitvectorPropagate()),
      d_abstractionModule(NULL),
      d_quickCheck(),
      d_quickXplain()
{
  if (options::bitvectorQuickXplain())
  {
    d_quickCheck.reset(new BVQuickCheck("bb", bv));
    d_quickXplain.reset(new QuickXPlain("bb", d_quickCheck.get()));
  }
}

BitblastSolver::~BitblastSolver() {}

BitblastSolver::Statistics::Statistics()
    : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
        "theory::bv::BitblastSolver::NumCallsToCheck")),
      d_numBBLemmas(smtStatisticsRegistry().registerInt(
          "theory::bv::BitblastSolver::NumTimesLemmasBB"))
{
}

void BitblastSolver::setAbstraction(AbstractionModule* abs) {
  d_abstractionModule = abs;
  d_bitblaster->setAbstraction(abs);
}

void BitblastSolver::preRegister(TNode node) {
  if ((node.getKind() == kind::EQUAL ||
       node.getKind() == kind::BITVECTOR_ULT ||
       node.getKind() == kind::BITVECTOR_ULE ||
       node.getKind() == kind::BITVECTOR_SLT ||
       node.getKind() == kind::BITVECTOR_SLE) &&
      !d_bitblaster->hasBBAtom(node)) {
    CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer);
    d_bitblastQueue.push_back(node);
    if ((options::decisionUseWeight() || options::decisionThreshold() != 0) &&
        !node.hasAttribute(decision::DecisionWeightAttr())) {
      node.setAttribute(decision::DecisionWeightAttr(),computeAtomWeight(node));
    }
  }
}

uint64_t BitblastSolver::computeAtomWeight(TNode node) {
  NodeSet seen;
  return d_bitblaster->computeAtomWeight(node, seen);
}

void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
  d_bitblaster->explain(literal, assumptions);
}

void BitblastSolver::bitblastQueue() {
  while (!d_bitblastQueue.empty()) {
    TNode atom = d_bitblastQueue.front();
    d_bitblastQueue.pop();
    Debug("bv-bitblast-queue") << "BitblastSolver::bitblastQueue (" << atom << ")\n";
    if (options::bvAbstraction() &&
        d_abstractionModule->isLemmaAtom(atom)) {
      // don't bit-blast lemma atoms
      continue;
    }
    if( !utils::isBitblastAtom(atom) ){
      continue;
    }
    Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
    {
      TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
      d_bitblaster->bbAtom(atom);
    }
  }
}

bool BitblastSolver::check(Theory::Effort e)
{
  Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
  Assert(options::bitblastMode() == options::BitblastMode::LAZY);

  ++(d_statistics.d_numCallstoCheck);

  Debug("bv-bitblast-debug") << "...process queue" << std::endl;
  //// Lazy bit-blasting
  // bit-blast enqueued nodes
  bitblastQueue();

  // Processing assertions
  while (!done())
  {
    TNode fact = get();
    d_validModelCache = false;
    Debug("bv-bitblast") << "  fact " << fact << ")\n";

    if (options::bvAbstraction())
    {
      // skip atoms that are the result of abstraction lemmas
      if (d_abstractionModule->isLemmaAtom(fact))
      {
        d_lemmaAtomsQueue.push_back(fact);
        continue;
      }
    }
    // skip facts involving integer equalities (from bv2nat)
    if (!utils::isBitblastAtom(fact))
    {
      continue;
    }

    if (!d_bv->inConflict()
        && (!d_bv->wasPropagatedBySubtheory(fact)
            || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST))
    {
      // Some atoms have not been bit-blasted yet
      d_bitblaster->bbAtom(fact);
      // Assert to sat
      bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
      if (!ok)
      {
        std::vector<TNode> conflictAtoms;
        d_bitblaster->getConflict(conflictAtoms);
        setConflict(utils::mkAnd(conflictAtoms));
        return false;
      }
    }
  }

  Debug("bv-bitblast-debug") << "...do propagation" << std::endl;
  // We need to ensure we are fully propagated, so propagate now
  if (d_useSatPropagation)
  {
    d_bv->spendResource(Resource::BvPropagationStep);
    bool ok = d_bitblaster->propagate();
    if (!ok)
    {
      std::vector<TNode> conflictAtoms;
      d_bitblaster->getConflict(conflictAtoms);
      setConflict(utils::mkAnd(conflictAtoms));
      return false;
    }
  }

  // Solving
  Debug("bv-bitblast-debug") << "...do solving" << std::endl;
  if (e == Theory::EFFORT_FULL)
  {
    Assert(!d_bv->inConflict());
    Debug("bitvector::bitblaster")
        << "BitblastSolver::addAssertions solving. \n";
    bool ok = d_bitblaster->solve();
    if (!ok)
    {
      std::vector<TNode> conflictAtoms;
      d_bitblaster->getConflict(conflictAtoms);
      Node conflict = utils::mkAnd(conflictAtoms);
      setConflict(conflict);
      return false;
    }
  }

  Debug("bv-bitblast-debug") << "...do abs bb" << std::endl;
  if (options::bvAbstraction() && e == Theory::EFFORT_FULL
      && d_lemmaAtomsQueue.size())
  {
    // bit-blast lemma atoms
    while (!d_lemmaAtomsQueue.empty())
    {
      TNode lemma_atom = d_lemmaAtomsQueue.front();
      d_lemmaAtomsQueue.pop();
      if (!utils::isBitblastAtom(lemma_atom))
      {
        continue;
      }
      d_bitblaster->bbAtom(lemma_atom);
      // Assert to sat and check for conflicts
      bool ok = d_bitblaster->assertToSat(lemma_atom, d_useSatPropagation);
      if (!ok)
      {
        std::vector<TNode> conflictAtoms;
        d_bitblaster->getConflict(conflictAtoms);
        setConflict(utils::mkAnd(conflictAtoms));
        return false;
      }
    }

    Assert(!d_bv->inConflict());
    bool ok = d_bitblaster->solve();
    if (!ok)
    {
      std::vector<TNode> conflictAtoms;
      d_bitblaster->getConflict(conflictAtoms);
      Node conflict = utils::mkAnd(conflictAtoms);
      setConflict(conflict);
      ++(d_statistics.d_numBBLemmas);
      return false;
    }
  }


  return true;
}

EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
  return d_bitblaster->getEqualityStatus(a, b);
}

bool BitblastSolver::collectModelValues(TheoryModel* m,
                                        const std::set<Node>& termSet)
{
  return d_bitblaster->collectModelValues(m, termSet);
}

Node BitblastSolver::getModelValue(TNode node)
{
  if (d_bv->d_invalidateModelCache.get()) {
    d_bitblaster->invalidateModelCache();
  }
  d_bv->d_invalidateModelCache.set(false);
  Node val = d_bitblaster->getTermModel(node, true);
  return val;
}

void BitblastSolver::setConflict(TNode conflict)
{
  Node final_conflict = conflict;
  if (options::bitvectorQuickXplain() &&
      conflict.getKind() == kind::AND) {
    // std::cout << "Original conflict " << conflict.getNumChildren() << "\n";
    final_conflict = d_quickXplain->minimizeConflict(conflict);
    //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n";
  }
  d_bv->setConflict(final_conflict);
}

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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Liana Hadarean, Aina Niemetz, Dejan Jovanovic
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		* Algebraic solver.
14		*/
15
16		#include "theory/bv/bv_subtheory_bitblast.h"
17
18		#include "decision/decision_attributes.h"
19		#include "options/bv_options.h"
20		#include "options/decision_options.h"
21		#include "smt/smt_statistics_registry.h"
22		#include "theory/bv/abstraction.h"
23		#include "theory/bv/bitblast/lazy_bitblaster.h"
24		#include "theory/bv/bv_quick_check.h"
25		#include "theory/bv/bv_solver_layered.h"
26		#include "theory/bv/theory_bv_utils.h"
27
28		using namespace std;
29		using namespace cvc5::context;
30
31		namespace cvc5 {
32		namespace theory {
33		namespace bv {
34
35	2	BitblastSolver::BitblastSolver(context::Context* c, BVSolverLayered* bv)
36		: SubtheorySolver(c, bv),
37	2	d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
38		d_bitblastQueue(c),
39		d_statistics(),
40		d_validModelCache(c, true),
41		d_lemmaAtomsQueue(c),
42	2	d_useSatPropagation(options::bitvectorPropagate()),
43		d_abstractionModule(NULL),
44		d_quickCheck(),
45	6	d_quickXplain()
46		{
47	2	if (options::bitvectorQuickXplain())
48		{
49		d_quickCheck.reset(new BVQuickCheck("bb", bv));
50		d_quickXplain.reset(new QuickXPlain("bb", d_quickCheck.get()));
51		}
52	2	}
53
54	4	BitblastSolver::~BitblastSolver() {}
55
56	2	BitblastSolver::Statistics::Statistics()
57	2	: d_numCallstoCheck(smtStatisticsRegistry().registerInt(
58	4	"theory::bv::BitblastSolver::NumCallsToCheck")),
59	2	d_numBBLemmas(smtStatisticsRegistry().registerInt(
60	4	"theory::bv::BitblastSolver::NumTimesLemmasBB"))
61		{
62	2	}
63
64		void BitblastSolver::setAbstraction(AbstractionModule* abs) {
65		d_abstractionModule = abs;
66		d_bitblaster->setAbstraction(abs);
67		}
68
69	28	void BitblastSolver::preRegister(TNode node) {
70	74	if ((node.getKind() == kind::EQUAL \|\|
71	36	node.getKind() == kind::BITVECTOR_ULT \|\|
72	36	node.getKind() == kind::BITVECTOR_ULE \|\|
73	36	node.getKind() == kind::BITVECTOR_SLT \|\|
74	94	node.getKind() == kind::BITVECTOR_SLE) &&
75	48	!d_bitblaster->hasBBAtom(node)) {
76	20	CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer);
77	10	d_bitblastQueue.push_back(node);
78	20	if ((options::decisionUseWeight() \|\| options::decisionThreshold() != 0) &&
79	10	!node.hasAttribute(decision::DecisionWeightAttr())) {
80		node.setAttribute(decision::DecisionWeightAttr(),computeAtomWeight(node));
81		}
82		}
83	28	}
84
85		uint64_t BitblastSolver::computeAtomWeight(TNode node) {
86		NodeSet seen;
87		return d_bitblaster->computeAtomWeight(node, seen);
88		}
89
90		void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
91		d_bitblaster->explain(literal, assumptions);
92		}
93
94		void BitblastSolver::bitblastQueue() {
95		while (!d_bitblastQueue.empty()) {
96		TNode atom = d_bitblastQueue.front();
97		d_bitblastQueue.pop();
98		Debug("bv-bitblast-queue") << "BitblastSolver::bitblastQueue (" << atom << ")\n";
99		if (options::bvAbstraction() &&
100		d_abstractionModule->isLemmaAtom(atom)) {
101		// don't bit-blast lemma atoms
102		continue;
103		}
104		if( !utils::isBitblastAtom(atom) ){
105		continue;
106		}
107		Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
108		{
109		TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
110		d_bitblaster->bbAtom(atom);
111		}
112		}
113		}
114
115		bool BitblastSolver::check(Theory::Effort e)
116		{
117		Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
118		Assert(options::bitblastMode() == options::BitblastMode::LAZY);
119
120		++(d_statistics.d_numCallstoCheck);
121
122		Debug("bv-bitblast-debug") << "...process queue" << std::endl;
123		//// Lazy bit-blasting
124		// bit-blast enqueued nodes
125		bitblastQueue();
126
127		// Processing assertions
128		while (!done())
129		{
130		TNode fact = get();
131		d_validModelCache = false;
132		Debug("bv-bitblast") << " fact " << fact << ")\n";
133
134		if (options::bvAbstraction())
135		{
136		// skip atoms that are the result of abstraction lemmas
137		if (d_abstractionModule->isLemmaAtom(fact))
138		{
139		d_lemmaAtomsQueue.push_back(fact);
140		continue;
141		}
142		}
143		// skip facts involving integer equalities (from bv2nat)
144		if (!utils::isBitblastAtom(fact))
145		{
146		continue;
147		}
148
149		if (!d_bv->inConflict()
150		&& (!d_bv->wasPropagatedBySubtheory(fact)
151		\|\| d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST))
152		{
153		// Some atoms have not been bit-blasted yet
154		d_bitblaster->bbAtom(fact);
155		// Assert to sat
156		bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
157		if (!ok)
158		{
159		std::vector<TNode> conflictAtoms;
160		d_bitblaster->getConflict(conflictAtoms);
161		setConflict(utils::mkAnd(conflictAtoms));
162		return false;
163		}
164		}
165		}
166
167		Debug("bv-bitblast-debug") << "...do propagation" << std::endl;
168		// We need to ensure we are fully propagated, so propagate now
169		if (d_useSatPropagation)
170		{
171		d_bv->spendResource(Resource::BvPropagationStep);
172		bool ok = d_bitblaster->propagate();
173		if (!ok)
174		{
175		std::vector<TNode> conflictAtoms;
176		d_bitblaster->getConflict(conflictAtoms);
177		setConflict(utils::mkAnd(conflictAtoms));
178		return false;
179		}
180		}
181
182		// Solving
183		Debug("bv-bitblast-debug") << "...do solving" << std::endl;
184		if (e == Theory::EFFORT_FULL)
185		{
186		Assert(!d_bv->inConflict());
187		Debug("bitvector::bitblaster")
188		<< "BitblastSolver::addAssertions solving. \n";
189		bool ok = d_bitblaster->solve();
190		if (!ok)
191		{
192		std::vector<TNode> conflictAtoms;
193		d_bitblaster->getConflict(conflictAtoms);
194		Node conflict = utils::mkAnd(conflictAtoms);
195		setConflict(conflict);
196		return false;
197		}
198		}
199
200		Debug("bv-bitblast-debug") << "...do abs bb" << std::endl;
201		if (options::bvAbstraction() && e == Theory::EFFORT_FULL
202		&& d_lemmaAtomsQueue.size())
203		{
204		// bit-blast lemma atoms
205		while (!d_lemmaAtomsQueue.empty())
206		{
207		TNode lemma_atom = d_lemmaAtomsQueue.front();
208		d_lemmaAtomsQueue.pop();
209		if (!utils::isBitblastAtom(lemma_atom))
210		{
211		continue;
212		}
213		d_bitblaster->bbAtom(lemma_atom);
214		// Assert to sat and check for conflicts
215		bool ok = d_bitblaster->assertToSat(lemma_atom, d_useSatPropagation);
216		if (!ok)
217		{
218		std::vector<TNode> conflictAtoms;
219		d_bitblaster->getConflict(conflictAtoms);
220		setConflict(utils::mkAnd(conflictAtoms));
221		return false;
222		}
223		}
224
225		Assert(!d_bv->inConflict());
226		bool ok = d_bitblaster->solve();
227		if (!ok)
228		{
229		std::vector<TNode> conflictAtoms;
230		d_bitblaster->getConflict(conflictAtoms);
231		Node conflict = utils::mkAnd(conflictAtoms);
232		setConflict(conflict);
233		++(d_statistics.d_numBBLemmas);
234		return false;
235		}
236		}
237
238
239		return true;
240		}
241
242		EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
243		return d_bitblaster->getEqualityStatus(a, b);
244		}
245
246		bool BitblastSolver::collectModelValues(TheoryModel* m,
247		const std::set<Node>& termSet)
248		{
249		return d_bitblaster->collectModelValues(m, termSet);
250		}
251
252		Node BitblastSolver::getModelValue(TNode node)
253		{
254		if (d_bv->d_invalidateModelCache.get()) {
255		d_bitblaster->invalidateModelCache();
256		}
257		d_bv->d_invalidateModelCache.set(false);
258		Node val = d_bitblaster->getTermModel(node, true);
259		return val;
260		}
261
262		void BitblastSolver::setConflict(TNode conflict)
263		{
264		Node final_conflict = conflict;
265		if (options::bitvectorQuickXplain() &&
266		conflict.getKind() == kind::AND) {
267		// std::cout << "Original conflict " << conflict.getNumChildren() << "\n";
268		final_conflict = d_quickXplain->minimizeConflict(conflict);
269		//std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n";
270		}
271		d_bv->setConflict(final_conflict);
272		}
273
274		} // namespace bv
275		} // namespace theory
276	29517	} // namespace cvc5