Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_subtheory_bitblast.cpp	Lines:	99	142	69.7 %
Date:	2021-05-22	Branches:	182	484	37.6 %


/******************************************************************************
 * 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_lazy.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, BVSolverLazy* 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_lazy.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	9405	BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv)
36		: SubtheorySolver(c, bv),
37	9405	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	9405	d_useSatPropagation(options::bitvectorPropagate()),
43		d_abstractionModule(NULL),
44		d_quickCheck(),
45	28215	d_quickXplain()
46		{
47	9405	if (options::bitvectorQuickXplain())
48		{
49		d_quickCheck.reset(new BVQuickCheck("bb", bv));
50		d_quickXplain.reset(new QuickXPlain("bb", d_quickCheck.get()));
51		}
52	9405	}
53
54	18810	BitblastSolver::~BitblastSolver() {}
55
56	9405	BitblastSolver::Statistics::Statistics()
57	9405	: d_numCallstoCheck(smtStatisticsRegistry().registerInt(
58	18810	"theory::bv::BitblastSolver::NumCallsToCheck")),
59	9405	d_numBBLemmas(smtStatisticsRegistry().registerInt(
60	18810	"theory::bv::BitblastSolver::NumTimesLemmasBB"))
61		{
62	9405	}
63
64	2	void BitblastSolver::setAbstraction(AbstractionModule* abs) {
65	2	d_abstractionModule = abs;
66	2	d_bitblaster->setAbstraction(abs);
67	2	}
68
69	221293	void BitblastSolver::preRegister(TNode node) {
70	609269	if ((node.getKind() == kind::EQUAL \|\|
71	319212	node.getKind() == kind::BITVECTOR_ULT \|\|
72	305058	node.getKind() == kind::BITVECTOR_ULE \|\|
73	289571	node.getKind() == kind::BITVECTOR_SLT \|\|
74	748130	node.getKind() == kind::BITVECTOR_SLE) &&
75	389795	!d_bitblaster->hasBBAtom(node)) {
76	148774	CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer);
77	74387	d_bitblastQueue.push_back(node);
78	148774	if ((options::decisionUseWeight() \|\| options::decisionThreshold() != 0) &&
79	74387	!node.hasAttribute(decision::DecisionWeightAttr())) {
80		node.setAttribute(decision::DecisionWeightAttr(),computeAtomWeight(node));
81		}
82		}
83	221293	}
84
85		uint64_t BitblastSolver::computeAtomWeight(TNode node) {
86		NodeSet seen;
87		return d_bitblaster->computeAtomWeight(node, seen);
88		}
89
90	20101	void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
91	20101	d_bitblaster->explain(literal, assumptions);
92	20101	}
93
94	298919	void BitblastSolver::bitblastQueue() {
95	397957	while (!d_bitblastQueue.empty()) {
96	198076	TNode atom = d_bitblastQueue.front();
97	99038	d_bitblastQueue.pop();
98	99038	Debug("bv-bitblast-queue") << "BitblastSolver::bitblastQueue (" << atom << ")\n";
99	198100	if (options::bvAbstraction() &&
100	99062	d_abstractionModule->isLemmaAtom(atom)) {
101		// don't bit-blast lemma atoms
102		continue;
103		}
104	99038	if( !utils::isBitblastAtom(atom) ){
105		continue;
106		}
107	99038	Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
108		{
109	198076	TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
110	99038	d_bitblaster->bbAtom(atom);
111		}
112		}
113	199881	}
114
115	199881	bool BitblastSolver::check(Theory::Effort e)
116		{
117	199881	Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
118	199881	Assert(options::bitblastMode() == options::BitblastMode::LAZY);
119
120	199881	++(d_statistics.d_numCallstoCheck);
121
122	199881	Debug("bv-bitblast-debug") << "...process queue" << std::endl;
123		//// Lazy bit-blasting
124		// bit-blast enqueued nodes
125	199881	bitblastQueue();
126
127		// Processing assertions
128	2716005	while (!done())
129		{
130	2525039	TNode fact = get();
131	1267319	d_validModelCache = false;
132	1267319	Debug("bv-bitblast") << " fact " << fact << ")\n";
133
134	1267319	if (options::bvAbstraction())
135		{
136		// skip atoms that are the result of abstraction lemmas
137	4	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	1267319	if (!utils::isBitblastAtom(fact))
145		{
146	342	continue;
147		}
148
149	2533954	if (!d_bv->inConflict()
150	4563693	&& (!d_bv->wasPropagatedBySubtheory(fact)
151	2403947	\|\| d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST))
152		{
153		// Some atoms have not been bit-blasted yet
154	762762	d_bitblaster->bbAtom(fact);
155		// Assert to sat
156	762762	bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
157	762762	if (!ok)
158		{
159	18514	std::vector<TNode> conflictAtoms;
160	9257	d_bitblaster->getConflict(conflictAtoms);
161	9257	setConflict(utils::mkAnd(conflictAtoms));
162	9257	return false;
163		}
164		}
165		}
166
167	190624	Debug("bv-bitblast-debug") << "...do propagation" << std::endl;
168		// We need to ensure we are fully propagated, so propagate now
169	190624	if (d_useSatPropagation)
170		{
171	190624	d_bv->spendResource(Resource::BvPropagationStep);
172	190624	bool ok = d_bitblaster->propagate();
173	190624	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	190624	Debug("bv-bitblast-debug") << "...do solving" << std::endl;
184	190624	if (e == Theory::EFFORT_FULL)
185		{
186	10064	Assert(!d_bv->inConflict());
187	20128	Debug("bitvector::bitblaster")
188	10064	<< "BitblastSolver::addAssertions solving. \n";
189	10064	bool ok = d_bitblaster->solve();
190	10064	if (!ok)
191		{
192	10304	std::vector<TNode> conflictAtoms;
193	5152	d_bitblaster->getConflict(conflictAtoms);
194	10304	Node conflict = utils::mkAnd(conflictAtoms);
195	5152	setConflict(conflict);
196	5152	return false;
197		}
198		}
199
200	185472	Debug("bv-bitblast-debug") << "...do abs bb" << std::endl;
201	370950	if (options::bvAbstraction() && e == Theory::EFFORT_FULL
202	185474	&& 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	185472	return true;
240		}
241
242	29399	EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
243	29399	return d_bitblaster->getEqualityStatus(a, b);
244		}
245
246	3186	bool BitblastSolver::collectModelValues(TheoryModel* m,
247		const std::set<Node>& termSet)
248		{
249	3186	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	14409	void BitblastSolver::setConflict(TNode conflict)
263		{
264	28818	Node final_conflict = conflict;
265	14409	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	14409	d_bv->setConflict(final_conflict);
272	14409	}
273
274		} // namespace bv
275		} // namespace theory
276	28191	} // namespace cvc5