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-10	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(
    Env& env,
    TheoryState* s,
    TheoryInferenceManager& inferMgr,
    ProofNodeManager* pnm)
    : BVSolver(env, *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	3764	BVSolverBitblastInternal::BVSolverBitblastInternal(
71		Env& env,
72		TheoryState* s,
73		TheoryInferenceManager& inferMgr,
74	3764	ProofNodeManager* pnm)
75		: BVSolver(env, *s, inferMgr),
76		d_pnm(pnm),
77	3764	d_bitblaster(new BBProof(s, pnm, false))
78		{
79	3764	}
80
81	891264	void BVSolverBitblastInternal::addBBLemma(TNode fact)
82		{
83	891264	if (!d_bitblaster->hasBBAtom(fact))
84		{
85	13806	d_bitblaster->bbAtom(fact);
86		}
87	891264	NodeManager* nm = NodeManager::currentNM();
88
89	1782528	Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
90	1782528	Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
91
92	891264	if (d_pnm == nullptr)
93		{
94	793071	d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
95		}
96		else
97		{
98		TrustNode tlem =
99	196386	TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
100	98193	d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
101		}
102	891264	}
103
104	1479372	bool BVSolverBitblastInternal::preNotifyFact(
105		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
106		{
107	1479372	if (fact.getKind() == kind::NOT)
108		{
109	798989	fact = fact[0];
110		}
111
112	1479372	if (isBVAtom(fact))
113		{
114	890312	addBBLemma(fact);
115		}
116	589060	else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
117		{
118	644	TNode n = fact[0];
119
120	322	NodeManager* nm = NodeManager::currentNM();
121	644	Node lemma = nm->mkNode(kind::EQUAL, fact, n);
122
123	322	if (d_pnm == nullptr)
124		{
125	269	d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
126		}
127		else
128		{
129	106	d_bitblaster->getProofGenerator()->addRewriteStep(
130	53	fact, n, PfRule::BV_EAGER_ATOM, {}, {fact});
131		TrustNode tlem =
132	106	TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
133	53	d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
134		}
135
136	644	std::unordered_set<Node> bv_atoms;
137	322	collectBVAtoms(n, bv_atoms);
138	1274	for (const Node& nn : bv_atoms)
139		{
140	952	addBBLemma(nn);
141		}
142		}
143
144	1479372	return false; // Return false to enable equality engine reasoning in Theory.
145		}
146
147	193	TrustNode BVSolverBitblastInternal::explain(TNode n)
148		{
149	193	Debug("bv-bitblast-internal") << "explain called on " << n << std::endl;
150	193	return d_im.explainLit(n);
151		}
152
153	1620	bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m,
154		const std::set<Node>& termSet)
155		{
156	1620	return d_bitblaster->collectModelValues(m, termSet);
157		}
158
159	309	Node BVSolverBitblastInternal::getValue(TNode node, bool initialize)
160		{
161	309	if (node.isConst())
162		{
163		return node;
164		}
165
166	309	if (!d_bitblaster->hasBBTerm(node))
167		{
168	186	return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
169		}
170
171	123	Valuation& val = d_state.getValuation();
172
173	246	std::vector<Node> bits;
174	123	d_bitblaster->getBBTerm(node, bits);
175	246	Integer value(0), one(1), zero(0), bit;
176	451	for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
177		{
178		bool satValue;
179	338	if (val.hasSatValue(bits[j], satValue))
180		{
181	320	bit = satValue ? one : zero;
182		}
183		else
184		{
185	18	if (!initialize) return Node();
186	8	bit = zero;
187		}
188	328	value = value * 2 + bit;
189		}
190	113	return utils::mkConst(bits.size(), value);
191		}
192
193	3750	BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker()
194		{
195	3750	return &d_checker;
196		}
197
198		} // namespace bv
199		} // namespace theory
200	29502	} // namespace cvc5