Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_solver_bitblast_internal.cpp	Lines:	68	80	85.0 %
Date:	2021-09-29	Branches:	125	268	46.6 %


/******************************************************************************
 * 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/bitblast/bitblast_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(env, s, pnm, false)),
      d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
{
}

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
    {
      TrustNode tlem =
          d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
      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/bitblast/bitblast_proof_generator.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
31		namespace {
32
33	1188	bool isBVAtom(TNode n)
34		{
35	2466	return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
36	1098	\|\| n.getKind() == kind::BITVECTOR_ULT
37	1088	\|\| n.getKind() == kind::BITVECTOR_ULE
38	1088	\|\| n.getKind() == kind::BITVECTOR_SLT
39	4652	\|\| n.getKind() == kind::BITVECTOR_SLE;
40		}
41
42		/* Traverse Boolean nodes and collect BV atoms. */
43	2	void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
44		{
45	4	std::vector<TNode> visit;
46	4	std::unordered_set<TNode> visited;
47
48	2	visit.push_back(n);
49
50	4	do
51		{
52	12	TNode cur = visit.back();
53	6	visit.pop_back();
54
55	6	if (visited.find(cur) != visited.end() \|\| !cur.getType().isBoolean())
56		continue;
57
58	6	visited.insert(cur);
59	6	if (isBVAtom(cur))
60		{
61		atoms.insert(cur);
62		continue;
63		}
64
65	6	visit.insert(visit.end(), cur.begin(), cur.end());
66	6	} while (!visit.empty());
67	2	}
68
69		} // namespace
70
71	157	BVSolverBitblastInternal::BVSolverBitblastInternal(
72		Env& env,
73		TheoryState* s,
74		TheoryInferenceManager& inferMgr,
75	157	ProofNodeManager* pnm)
76		: BVSolver(env, *s, inferMgr),
77		d_pnm(pnm),
78	157	d_bitblaster(new BBProof(env, s, pnm, false)),
79	314	d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
80		{
81	157	}
82
83	100	void BVSolverBitblastInternal::addBBLemma(TNode fact)
84		{
85	100	if (!d_bitblaster->hasBBAtom(fact))
86		{
87	76	d_bitblaster->bbAtom(fact);
88		}
89	100	NodeManager* nm = NodeManager::currentNM();
90
91	200	Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
92	200	Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
93
94	100	if (d_pnm == nullptr)
95		{
96	100	d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
97		}
98		else
99		{
100		TrustNode tlem =
101		TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
102		d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
103		}
104	100	}
105
106	1182	bool BVSolverBitblastInternal::preNotifyFact(
107		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
108		{
109	1182	if (fact.getKind() == kind::NOT)
110		{
111	144	fact = fact[0];
112		}
113
114	1182	if (isBVAtom(fact))
115		{
116	100	addBBLemma(fact);
117		}
118	1082	else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
119		{
120	4	TNode n = fact[0];
121
122	2	NodeManager* nm = NodeManager::currentNM();
123	4	Node lemma = nm->mkNode(kind::EQUAL, fact, n);
124
125	2	if (d_pnm == nullptr)
126		{
127	2	d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
128		}
129		else
130		{
131		TrustNode tlem =
132		d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
133		d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
134		}
135
136	4	std::unordered_set<Node> bv_atoms;
137	2	collectBVAtoms(n, bv_atoms);
138	2	for (const Node& nn : bv_atoms)
139		{
140		addBBLemma(nn);
141		}
142		}
143
144	1182	return false; // Return false to enable equality engine reasoning in Theory.
145		}
146
147		TrustNode BVSolverBitblastInternal::explain(TNode n)
148		{
149		Debug("bv-bitblast-internal") << "explain called on " << n << std::endl;
150		return d_im.explainLit(n);
151		}
152
153	49	bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m,
154		const std::set<Node>& termSet)
155		{
156	49	return d_bitblaster->collectModelValues(m, termSet);
157		}
158
159	42	Node BVSolverBitblastInternal::getValue(TNode node, bool initialize)
160		{
161	42	if (node.isConst())
162		{
163		return node;
164		}
165
166	42	if (!d_bitblaster->hasBBTerm(node))
167		{
168	24	return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
169		}
170
171	18	Valuation& val = d_state.getValuation();
172
173	36	std::vector<Node> bits;
174	18	d_bitblaster->getBBTerm(node, bits);
175	36	Integer value(0), one(1), zero(0), bit;
176	58	for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
177		{
178		bool satValue;
179	44	if (val.hasSatValue(bits[j], satValue))
180		{
181	32	bit = satValue ? one : zero;
182		}
183		else
184		{
185	12	if (!initialize) return Node();
186	8	bit = zero;
187		}
188	40	value = value * 2 + bit;
189		}
190	14	return utils::mkConst(bits.size(), value);
191		}
192
193	143	BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker()
194		{
195	143	return &d_checker;
196		}
197
198		} // namespace bv
199		} // namespace theory
200	22746	} // namespace cvc5