Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_solver_bitblast_internal.cpp	Lines:	79	81	97.5 %
Date:	2021-09-05	Branches:	150	266	56.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner, Gereon Kremer, Haniel Barbosa
 *
 * 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-blast solver that sends bit-blast lemmas directly to the internal
 * MiniSat.
 */

#include "theory/bv/bv_solver_bitblast_internal.h"

#include "proof/conv_proof_generator.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 {

/* -------------------------------------------------------------------------- */

namespace {

bool isBVAtom(TNode n)
{
  return (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;
}

/* Traverse Boolean nodes and collect BV atoms. */
void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
{
  std::vector<TNode> visit;
  std::unordered_set<TNode> visited;

  visit.push_back(n);

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

    if (visited.find(cur) != visited.end() || !cur.getType().isBoolean())
      continue;

    visited.insert(cur);
    if (isBVAtom(cur))
    {
      atoms.insert(cur);
      continue;
    }

    visit.insert(visit.end(), cur.begin(), cur.end());
  } while (!visit.empty());
}

}  // namespace

BVSolverBitblastInternal::BVSolverBitblastInternal(
    TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm)
    : BVSolver(*s, inferMgr),
      d_pnm(pnm),
      d_bitblaster(new BBProof(s, pnm, false))
{
}

void BVSolverBitblastInternal::addBBLemma(TNode fact)
{
  if (!d_bitblaster->hasBBAtom(fact))
  {
    d_bitblaster->bbAtom(fact);
  }
  NodeManager* nm = NodeManager::currentNM();

  Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
  Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);

  if (d_pnm == nullptr)
  {
    d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
  }
  else
  {
    TrustNode tlem =
        TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
    d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
  }
}

bool BVSolverBitblastInternal::preNotifyFact(
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
{
  if (fact.getKind() == kind::NOT)
  {
    fact = fact[0];
  }

  if (isBVAtom(fact))
  {
    addBBLemma(fact);
  }
  else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
  {
    TNode n = fact[0];

    NodeManager* nm = NodeManager::currentNM();
    Node lemma = nm->mkNode(kind::EQUAL, fact, n);

    if (d_pnm == nullptr)
    {
      d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
    }
    else
    {
      d_bitblaster->getProofGenerator()->addRewriteStep(
          fact, n, PfRule::BV_EAGER_ATOM, {}, {fact});
      TrustNode tlem =
          TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
      d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
    }

    std::unordered_set<Node> bv_atoms;
    collectBVAtoms(n, bv_atoms);
    for (const Node& nn : bv_atoms)
    {
      addBBLemma(nn);
    }
  }

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

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

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

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

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

  Valuation& val = d_state.getValuation();

  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)
  {
    bool satValue;
    if (val.hasSatValue(bits[j], satValue))
    {
      bit = satValue ? one : zero;
    }
    else
    {
      if (!initialize) return Node();
      bit = zero;
    }
    value = value * 2 + bit;
  }
  return utils::mkConst(bits.size(), value);
}

BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker()
{
  return &d_checker;
}

}  // 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, Haniel Barbosa
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-blast solver that sends bit-blast lemmas directly to the internal
14		* MiniSat.
15		*/
16
17		#include "theory/bv/bv_solver_bitblast_internal.h"
18
19		#include "proof/conv_proof_generator.h"
20		#include "theory/bv/theory_bv.h"
21		#include "theory/bv/theory_bv_utils.h"
22		#include "theory/theory_model.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace bv {
27
28		/* -------------------------------------------------------------------------- */
29
30		namespace {
31
32	1480639	bool isBVAtom(TNode n)
33		{
34	3539476	return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
35	902441	\|\| n.getKind() == kind::BITVECTOR_ULT
36	744244	\|\| n.getKind() == kind::BITVECTOR_ULE
37	744244	\|\| n.getKind() == kind::BITVECTOR_SLT
38	5031292	\|\| n.getKind() == kind::BITVECTOR_SLE;
39		}
40
41		/* Traverse Boolean nodes and collect BV atoms. */
42	322	void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
43		{
44	644	std::vector<TNode> visit;
45	644	std::unordered_set<TNode> visited;
46
47	322	visit.push_back(n);
48
49	945	do
50		{
51	1582	TNode cur = visit.back();
52	1267	visit.pop_back();
53
54	1267	if (visited.find(cur) != visited.end() \|\| !cur.getType().isBoolean())
55		continue;
56
57	1267	visited.insert(cur);
58	2219	if (isBVAtom(cur))
59		{
60	952	atoms.insert(cur);
61	952	continue;
62		}
63
64	315	visit.insert(visit.end(), cur.begin(), cur.end());
65	1267	} while (!visit.empty());
66	322	}
67
68		} // namespace
69
70	3767	BVSolverBitblastInternal::BVSolverBitblastInternal(
71	3767	TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm)
72		: BVSolver(*s, inferMgr),
73		d_pnm(pnm),
74	3767	d_bitblaster(new BBProof(s, pnm, false))
75		{
76	3767	}
77
78	891264	void BVSolverBitblastInternal::addBBLemma(TNode fact)
79		{
80	891264	if (!d_bitblaster->hasBBAtom(fact))
81		{
82	13806	d_bitblaster->bbAtom(fact);
83		}
84	891264	NodeManager* nm = NodeManager::currentNM();
85
86	1782528	Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
87	1782528	Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
88
89	891264	if (d_pnm == nullptr)
90		{
91	793071	d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
92		}
93		else
94		{
95		TrustNode tlem =
96	196386	TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
97	98193	d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
98		}
99	891264	}
100
101	1479372	bool BVSolverBitblastInternal::preNotifyFact(
102		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
103		{
104	1479372	if (fact.getKind() == kind::NOT)
105		{
106	798989	fact = fact[0];
107		}
108
109	1479372	if (isBVAtom(fact))
110		{
111	890312	addBBLemma(fact);
112		}
113	589060	else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
114		{
115	644	TNode n = fact[0];
116
117	322	NodeManager* nm = NodeManager::currentNM();
118	644	Node lemma = nm->mkNode(kind::EQUAL, fact, n);
119
120	322	if (d_pnm == nullptr)
121		{
122	269	d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
123		}
124		else
125		{
126	106	d_bitblaster->getProofGenerator()->addRewriteStep(
127	53	fact, n, PfRule::BV_EAGER_ATOM, {}, {fact});
128		TrustNode tlem =
129	106	TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
130	53	d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
131		}
132
133	644	std::unordered_set<Node> bv_atoms;
134	322	collectBVAtoms(n, bv_atoms);
135	1274	for (const Node& nn : bv_atoms)
136		{
137	952	addBBLemma(nn);
138		}
139		}
140
141	1479372	return false; // Return false to enable equality engine reasoning in Theory.
142		}
143
144	193	TrustNode BVSolverBitblastInternal::explain(TNode n)
145		{
146	193	Debug("bv-bitblast-internal") << "explain called on " << n << std::endl;
147	193	return d_im.explainLit(n);
148		}
149
150	1623	bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m,
151		const std::set<Node>& termSet)
152		{
153	1623	return d_bitblaster->collectModelValues(m, termSet);
154		}
155
156	309	Node BVSolverBitblastInternal::getValue(TNode node, bool initialize)
157		{
158	309	if (node.isConst())
159		{
160		return node;
161		}
162
163	309	if (!d_bitblaster->hasBBTerm(node))
164		{
165	186	return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
166		}
167
168	123	Valuation& val = d_state.getValuation();
169
170	246	std::vector<Node> bits;
171	123	d_bitblaster->getBBTerm(node, bits);
172	246	Integer value(0), one(1), zero(0), bit;
173	451	for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
174		{
175		bool satValue;
176	338	if (val.hasSatValue(bits[j], satValue))
177		{
178	320	bit = satValue ? one : zero;
179		}
180		else
181		{
182	18	if (!initialize) return Node();
183	8	bit = zero;
184		}
185	328	value = value * 2 + bit;
186		}
187	113	return utils::mkConst(bits.size(), value);
188		}
189
190	3753	BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker()
191		{
192	3753	return &d_checker;
193		}
194
195		} // namespace bv
196		} // namespace theory
197	29505	} // namespace cvc5