Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/proof_bitblaster.cpp	Lines:	83	83	100.0 %
Date:	2021-11-07	Branches:	164	310	52.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * A bit-blaster wrapper around BBSimple for proof logging.
 */
#include "theory/bv/bitblast/proof_bitblaster.h"

#include <unordered_set>

#include "proof/conv_proof_generator.h"
#include "theory/bv/bitblast/bitblast_proof_generator.h"
#include "theory/theory_model.h"

namespace cvc5 {
namespace theory {
namespace bv {

BBProof::BBProof(Env& env,
                 TheoryState* state,
                 ProofNodeManager* pnm,
                 bool fineGrained)
    : EnvObj(env),
      d_bb(new NodeBitblaster(env, state)),
      d_pnm(pnm),
      d_tcontext(new TheoryLeafTermContext(theory::THEORY_BV)),
      d_tcpg(pnm ? new TConvProofGenerator(
                 pnm,
                 nullptr,
                 /* ONCE to visit each term only once, post-order.  FIXPOINT
                  * could lead to infinite loops due to terms being rewritten
                  * to terms that contain themselves */
                 TConvPolicy::ONCE,
                 /* STATIC to get the same ProofNode for a shared subterm. */
                 TConvCachePolicy::STATIC,
                 "BBProof::TConvProofGenerator",
                 d_tcontext.get(),
                 false)
                 : nullptr),
      d_bbpg(pnm ? new BitblastProofGenerator(env, pnm, d_tcpg.get())
                 : nullptr),
      d_recordFineGrainedProofs(fineGrained)
{
}

BBProof::~BBProof() {}

void BBProof::bbAtom(TNode node)
{
  bool fineProofs = isProofsEnabled() && d_recordFineGrainedProofs;

  /* Bit-blasting bit-vector atoms consists of 3 steps:
   *   1. rewrite the atom
   *   2. bit-blast the rewritten atom
   *   3. rewrite the resulting bit-blasted term
   *
   * This happens in a single call to d_bb->bbAtom(...). When we record
   * fine-grained proofs, we explicitly record the above 3 steps.
   *
   * Note: The below post-order traversal corresponds to the recursive
   * bit-blasting of bit-vector terms that happens implicitly when calling the
   * corresponding bit-blasting strategy in d_bb->bbAtom(...).
   */
  if (fineProofs)
  {
    std::vector<TNode> visit;
    std::unordered_set<TNode> visited;
    NodeManager* nm = NodeManager::currentNM();

    // post-rewrite atom
    Node rwNode = rewrite(node);

    // Post-order traversal of `rwNode` to make sure that all subterms are
    // bit-blasted and recorded.
    visit.push_back(rwNode);
    while (!visit.empty())
    {
      TNode n = visit.back();
      if (hasBBAtom(n) || hasBBTerm(n))
      {
        visit.pop_back();
        continue;
      }

      if (visited.find(n) == visited.end())
      {
        visited.insert(n);
        if (!Theory::isLeafOf(n, theory::THEORY_BV))
        {
          visit.insert(visit.end(), n.begin(), n.end());
        }
      }
      else
      {
        /* Handle BV theory leafs as variables, i.e., apply the BITVECTOR_BITOF
         * operator to each bit of `n`. */
        if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
        {
          Bits bits;
          d_bb->makeVariable(n, bits);

          Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
          d_bbMap.emplace(n, bbt);
          d_tcpg->addRewriteStep(
              n, bbt, PfRule::BV_BITBLAST_STEP, {}, {n.eqNode(bbt)});
        }
        else if (n.getType().isBitVector())
        {
          Bits bits;
          d_bb->bbTerm(n, bits);

          Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
          Node rbbt;
          if (n.isConst())
          {
            d_bbMap.emplace(n, bbt);
            rbbt = n;
          }
          else
          {
            d_bbMap.emplace(n, bbt);
            rbbt = reconstruct(n);
          }
          d_tcpg->addRewriteStep(
              rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
        }
        else
        {
          Assert(n == rwNode);
        }
        visit.pop_back();
      }
    }

    /* Bit-blast given rewritten bit-vector atom `node`.
     * Note: This will pre and post-rewrite and store it in the bit-blasting
     * cache. */
    d_bb->bbAtom(node);
    Node result = d_bb->getStoredBBAtom(node);

    // Retrieve bit-blasted `rwNode` without post-rewrite.
    Node bbt = rwNode.getKind() == kind::CONST_BOOLEAN
                       || rwNode.getKind() == kind::BITVECTOR_BITOF
                   ? rwNode
                   : d_bb->applyAtomBBStrategy(rwNode);

    Node rbbt = reconstruct(rwNode);

    d_tcpg->addRewriteStep(
        rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});

    d_bbpg->addBitblastStep(node, bbt, node.eqNode(result));
  }
  else
  {
    d_bb->bbAtom(node);

    /* Record coarse-grain bit-blast proof step. */
    if (isProofsEnabled() && !d_recordFineGrainedProofs)
    {
      Node bbt = getStoredBBAtom(node);
      d_bbpg->addBitblastStep(Node(), Node(), node.eqNode(bbt));
    }
  }
}

Node BBProof::reconstruct(TNode t)
{
  NodeManager* nm = NodeManager::currentNM();

  std::vector<Node> children;
  if (t.getMetaKind() == kind::metakind::PARAMETERIZED)
  {
    children.push_back(t.getOperator());
  }
  for (const auto& child : t)
  {
    children.push_back(d_bbMap.at(child));
  }
  return nm->mkNode(t.getKind(), children);
}

bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }

bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }

Node BBProof::getStoredBBAtom(TNode node)
{
  return d_bb->getStoredBBAtom(node);
}

void BBProof::getBBTerm(TNode node, Bits& bits) const
{
  d_bb->getBBTerm(node, bits);
}

bool BBProof::collectModelValues(TheoryModel* m,
                                 const std::set<Node>& relevantTerms)
{
  return d_bb->collectModelValues(m, relevantTerms);
}

BitblastProofGenerator* BBProof::getProofGenerator() { return d_bbpg.get(); }

bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }

}  // namespace bv
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Mathias Preiner
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		* A bit-blaster wrapper around BBSimple for proof logging.
14		*/
15		#include "theory/bv/bitblast/proof_bitblaster.h"
16
17		#include <unordered_set>
18
19		#include "proof/conv_proof_generator.h"
20		#include "theory/bv/bitblast/bitblast_proof_generator.h"
21		#include "theory/theory_model.h"
22
23		namespace cvc5 {
24		namespace theory {
25		namespace bv {
26
27	9552	BBProof::BBProof(Env& env,
28		TheoryState* state,
29		ProofNodeManager* pnm,
30	9552	bool fineGrained)
31		: EnvObj(env),
32	9552	d_bb(new NodeBitblaster(env, state)),
33		d_pnm(pnm),
34	9552	d_tcontext(new TheoryLeafTermContext(theory::THEORY_BV)),
35		d_tcpg(pnm ? new TConvProofGenerator(
36		pnm,
37		nullptr,
38		/* ONCE to visit each term only once, post-order. FIXPOINT
39		* could lead to infinite loops due to terms being rewritten
40		* to terms that contain themselves */
41		TConvPolicy::ONCE,
42		/* STATIC to get the same ProofNode for a shared subterm. */
43		TConvCachePolicy::STATIC,
44		"BBProof::TConvProofGenerator",
45	6934	d_tcontext.get(),
46	6934	false)
47		: nullptr),
48	6934	d_bbpg(pnm ? new BitblastProofGenerator(env, pnm, d_tcpg.get())
49		: nullptr),
50	42524	d_recordFineGrainedProofs(fineGrained)
51		{
52	9552	}
53
54	17536	BBProof::~BBProof() {}
55
56	15501	void BBProof::bbAtom(TNode node)
57		{
58	15501	bool fineProofs = isProofsEnabled() && d_recordFineGrainedProofs;
59
60		/* Bit-blasting bit-vector atoms consists of 3 steps:
61		* 1. rewrite the atom
62		* 2. bit-blast the rewritten atom
63		* 3. rewrite the resulting bit-blasted term
64		*
65		* This happens in a single call to d_bb->bbAtom(...). When we record
66		* fine-grained proofs, we explicitly record the above 3 steps.
67		*
68		* Note: The below post-order traversal corresponds to the recursive
69		* bit-blasting of bit-vector terms that happens implicitly when calling the
70		* corresponding bit-blasting strategy in d_bb->bbAtom(...).
71		*/
72	15501	if (fineProofs)
73		{
74	3136	std::vector<TNode> visit;
75	3136	std::unordered_set<TNode> visited;
76	1568	NodeManager* nm = NodeManager::currentNM();
77
78		// post-rewrite atom
79	3136	Node rwNode = rewrite(node);
80
81		// Post-order traversal of `rwNode` to make sure that all subterms are
82		// bit-blasted and recorded.
83	1568	visit.push_back(rwNode);
84	49274	while (!visit.empty())
85		{
86	46280	TNode n = visit.back();
87	25279	if (hasBBAtom(n) \|\| hasBBTerm(n))
88		{
89	1426	visit.pop_back();
90	1426	continue;
91		}
92
93	22427	if (visited.find(n) == visited.end())
94		{
95	11170	visited.insert(n);
96	11170	if (!Theory::isLeafOf(n, theory::THEORY_BV))
97		{
98	6236	visit.insert(visit.end(), n.begin(), n.end());
99		}
100		}
101		else
102		{
103		/* Handle BV theory leafs as variables, i.e., apply the BITVECTOR_BITOF
104		* operator to each bit of `n`. */
105	11257	if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
106		{
107	6588	Bits bits;
108	3294	d_bb->makeVariable(n, bits);
109
110	6588	Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
111	3294	d_bbMap.emplace(n, bbt);
112	6588	d_tcpg->addRewriteStep(
113	3294	n, bbt, PfRule::BV_BITBLAST_STEP, {}, {n.eqNode(bbt)});
114		}
115	7963	else if (n.getType().isBitVector())
116		{
117	12790	Bits bits;
118	6395	d_bb->bbTerm(n, bits);
119
120	12790	Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
121	12790	Node rbbt;
122	6395	if (n.isConst())
123		{
124	1727	d_bbMap.emplace(n, bbt);
125	1727	rbbt = n;
126		}
127		else
128		{
129	4668	d_bbMap.emplace(n, bbt);
130	4668	rbbt = reconstruct(n);
131		}
132	12790	d_tcpg->addRewriteStep(
133	6395	rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
134		}
135		else
136		{
137	1568	Assert(n == rwNode);
138		}
139	11257	visit.pop_back();
140		}
141		}
142
143		/* Bit-blast given rewritten bit-vector atom `node`.
144		* Note: This will pre and post-rewrite and store it in the bit-blasting
145		* cache. */
146	1568	d_bb->bbAtom(node);
147	3136	Node result = d_bb->getStoredBBAtom(node);
148
149		// Retrieve bit-blasted `rwNode` without post-rewrite.
150	1568	Node bbt = rwNode.getKind() == kind::CONST_BOOLEAN
151	1568	\|\| rwNode.getKind() == kind::BITVECTOR_BITOF
152	1568	? rwNode
153	3136	: d_bb->applyAtomBBStrategy(rwNode);
154
155	3136	Node rbbt = reconstruct(rwNode);
156
157	3136	d_tcpg->addRewriteStep(
158	1568	rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
159
160	1568	d_bbpg->addBitblastStep(node, bbt, node.eqNode(result));
161		}
162		else
163		{
164	13933	d_bb->bbAtom(node);
165
166		/* Record coarse-grain bit-blast proof step. */
167	13933	if (isProofsEnabled() && !d_recordFineGrainedProofs)
168		{
169	7998	Node bbt = getStoredBBAtom(node);
170	3999	d_bbpg->addBitblastStep(Node(), Node(), node.eqNode(bbt));
171		}
172		}
173	15501	}
174
175	6236	Node BBProof::reconstruct(TNode t)
176		{
177	6236	NodeManager* nm = NodeManager::currentNM();
178
179	12472	std::vector<Node> children;
180	6236	if (t.getMetaKind() == kind::metakind::PARAMETERIZED)
181		{
182	1416	children.push_back(t.getOperator());
183		}
184	17351	for (const auto& child : t)
185		{
186	11115	children.push_back(d_bbMap.at(child));
187		}
188	12472	return nm->mkNode(t.getKind(), children);
189		}
190
191	943824	bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
192
193	24160	bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
194
195	925538	Node BBProof::getStoredBBAtom(TNode node)
196		{
197	925538	return d_bb->getStoredBBAtom(node);
198		}
199
200	121	void BBProof::getBBTerm(TNode node, Bits& bits) const
201		{
202	121	d_bb->getBBTerm(node, bits);
203	121	}
204
205	3315	bool BBProof::collectModelValues(TheoryModel* m,
206		const std::set<Node>& relevantTerms)
207		{
208	3315	return d_bb->collectModelValues(m, relevantTerms);
209		}
210
211	99940	BitblastProofGenerator* BBProof::getProofGenerator() { return d_bbpg.get(); }
212
213	29434	bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
214
215		} // namespace bv
216		} // namespace theory
217	31137	} // namespace cvc5