Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_solver_bitblast_internal.cpp	Lines:	80	82	97.6 %
Date:	2021-11-07	Branches:	152	268	56.7 %


/******************************************************************************
 * 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 "options/bv_options.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::needsEqualityEngine(EeSetupInfo& esi)
{
  // Disable equality engine if --bitblast=eager is enabled.
  return options().bv.bitblastMode != options::BitblastMode::EAGER;
}

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);
    }
  }

  // Disable the equality engine in --bitblast=eager mode. Otherwise return
  // false to enable equality engine reasoning in Theory.
  return options().bv.bitblastMode == options::BitblastMode::EAGER;
}

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 "options/bv_options.h"
20		#include "proof/conv_proof_generator.h"
21		#include "theory/bv/bitblast/bitblast_proof_generator.h"
22		#include "theory/bv/theory_bv.h"
23		#include "theory/bv/theory_bv_utils.h"
24		#include "theory/theory_model.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace bv {
29
30		/* -------------------------------------------------------------------------- */
31
32		namespace {
33
34	1520711	bool isBVAtom(TNode n)
35		{
36	3639042	return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
37	923091	\|\| n.getKind() == kind::BITVECTOR_ULT
38	759920	\|\| n.getKind() == kind::BITVECTOR_ULE
39	759920	\|\| n.getKind() == kind::BITVECTOR_SLT
40	5162873	\|\| n.getKind() == kind::BITVECTOR_SLE;
41		}
42
43		/* Traverse Boolean nodes and collect BV atoms. */
44	379	void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
45		{
46	758	std::vector<TNode> visit;
47	758	std::unordered_set<TNode> visited;
48
49	379	visit.push_back(n);
50
51	967	do
52		{
53	1675	TNode cur = visit.back();
54	1346	visit.pop_back();
55
56	1346	if (visited.find(cur) != visited.end() \|\| !cur.getType().isBoolean())
57		continue;
58
59	1346	visited.insert(cur);
60	2363	if (isBVAtom(cur))
61		{
62	1017	atoms.insert(cur);
63	1017	continue;
64		}
65
66	329	visit.insert(visit.end(), cur.begin(), cur.end());
67	1346	} while (!visit.empty());
68	379	}
69
70		} // namespace
71
72	7984	BVSolverBitblastInternal::BVSolverBitblastInternal(
73		Env& env,
74		TheoryState* s,
75		TheoryInferenceManager& inferMgr,
76	7984	ProofNodeManager* pnm)
77		: BVSolver(env, *s, inferMgr),
78		d_pnm(pnm),
79	7984	d_bitblaster(new BBProof(env, s, pnm, false)),
80	15968	d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
81		{
82	7984	}
83
84	919971	void BVSolverBitblastInternal::addBBLemma(TNode fact)
85		{
86	919971	if (!d_bitblaster->hasBBAtom(fact))
87		{
88	13933	d_bitblaster->bbAtom(fact);
89		}
90	919971	NodeManager* nm = NodeManager::currentNM();
91
92	1839942	Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
93	1839942	Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
94
95	919971	if (d_pnm == nullptr)
96		{
97	821599	d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
98		}
99		else
100		{
101		TrustNode tlem =
102	196744	TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
103	98372	d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
104		}
105	919971	}
106
107	7984	bool BVSolverBitblastInternal::needsEqualityEngine(EeSetupInfo& esi)
108		{
109		// Disable equality engine if --bitblast=eager is enabled.
110	7984	return options().bv.bitblastMode != options::BitblastMode::EAGER;
111		}
112
113	1519365	bool BVSolverBitblastInternal::preNotifyFact(
114		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
115		{
116	1519365	if (fact.getKind() == kind::NOT)
117		{
118	820752	fact = fact[0];
119		}
120
121	1519365	if (isBVAtom(fact))
122		{
123	918954	addBBLemma(fact);
124		}
125	600411	else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
126		{
127	758	TNode n = fact[0];
128
129	379	NodeManager* nm = NodeManager::currentNM();
130	758	Node lemma = nm->mkNode(kind::EQUAL, fact, n);
131
132	379	if (d_pnm == nullptr)
133		{
134	319	d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
135		}
136		else
137		{
138		TrustNode tlem =
139	120	d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
140	60	d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
141		}
142
143	758	std::unordered_set<Node> bv_atoms;
144	379	collectBVAtoms(n, bv_atoms);
145	1396	for (const Node& nn : bv_atoms)
146		{
147	1017	addBBLemma(nn);
148		}
149		}
150
151		// Disable the equality engine in --bitblast=eager mode. Otherwise return
152		// false to enable equality engine reasoning in Theory.
153	1519365	return options().bv.bitblastMode == options::BitblastMode::EAGER;
154		}
155
156	182	TrustNode BVSolverBitblastInternal::explain(TNode n)
157		{
158	182	Debug("bv-bitblast-internal") << "explain called on " << n << std::endl;
159	182	return d_im.explainLit(n);
160		}
161
162	3315	bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m,
163		const std::set<Node>& termSet)
164		{
165	3315	return d_bitblaster->collectModelValues(m, termSet);
166		}
167
168	307	Node BVSolverBitblastInternal::getValue(TNode node, bool initialize)
169		{
170	307	if (node.isConst())
171		{
172		return node;
173		}
174
175	307	if (!d_bitblaster->hasBBTerm(node))
176		{
177	186	return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
178		}
179
180	121	Valuation& val = d_state.getValuation();
181
182	242	std::vector<Node> bits;
183	121	d_bitblaster->getBBTerm(node, bits);
184	242	Integer value(0), one(1), zero(0), bit;
185	433	for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
186		{
187		bool satValue;
188	322	if (val.hasSatValue(bits[j], satValue))
189		{
190	304	bit = satValue ? one : zero;
191		}
192		else
193		{
194	18	if (!initialize) return Node();
195	8	bit = zero;
196		}
197	312	value = value * 2 + bit;
198		}
199	111	return utils::mkConst(bits.size(), value);
200		}
201
202	7970	BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker()
203		{
204	7970	return &d_checker;
205		}
206
207		} // namespace bv
208		} // namespace theory
209	31137	} // namespace cvc5