Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/proof_bitblaster.cpp	Lines:	83	83	100.0 %
Date:	2021-09-17	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(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 = Rewriter::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	5340	BBProof::BBProof(Env& env,
28		TheoryState* state,
29		ProofNodeManager* pnm,
30	5340	bool fineGrained)
31		: EnvObj(env),
32	5340	d_bb(new NodeBitblaster(env, state)),
33		d_pnm(pnm),
34	5340	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	2794	d_tcontext.get(),
46	2794	false)
47		: nullptr),
48	2794	d_bbpg(pnm ? new BitblastProofGenerator(pnm, d_tcpg.get()) : nullptr),
49	21608	d_recordFineGrainedProofs(fineGrained)
50		{
51	5340	}
52
53	9118	BBProof::~BBProof() {}
54
55	15414	void BBProof::bbAtom(TNode node)
56		{
57	15414	bool fineProofs = isProofsEnabled() && d_recordFineGrainedProofs;
58
59		/* Bit-blasting bit-vector atoms consists of 3 steps:
60		* 1. rewrite the atom
61		* 2. bit-blast the rewritten atom
62		* 3. rewrite the resulting bit-blasted term
63		*
64		* This happens in a single call to d_bb->bbAtom(...). When we record
65		* fine-grained proofs, we explicitly record the above 3 steps.
66		*
67		* Note: The below post-order traversal corresponds to the recursive
68		* bit-blasting of bit-vector terms that happens implicitly when calling the
69		* corresponding bit-blasting strategy in d_bb->bbAtom(...).
70		*/
71	15414	if (fineProofs)
72		{
73	3124	std::vector<TNode> visit;
74	3124	std::unordered_set<TNode> visited;
75	1562	NodeManager* nm = NodeManager::currentNM();
76
77		// post-rewrite atom
78	3124	Node rwNode = Rewriter::rewrite(node);
79
80		// Post-order traversal of `rwNode` to make sure that all subterms are
81		// bit-blasted and recorded.
82	1562	visit.push_back(rwNode);
83	49410	while (!visit.empty())
84		{
85	46419	TNode n = visit.back();
86	25353	if (hasBBAtom(n) \|\| hasBBTerm(n))
87		{
88	1429	visit.pop_back();
89	1429	continue;
90		}
91
92	22495	if (visited.find(n) == visited.end())
93		{
94	11203	visited.insert(n);
95	11203	if (!Theory::isLeafOf(n, theory::THEORY_BV))
96		{
97	6253	visit.insert(visit.end(), n.begin(), n.end());
98		}
99		}
100		else
101		{
102		/* Handle BV theory leafs as variables, i.e., apply the BITVECTOR_BITOF
103		* operator to each bit of `n`. */
104	11292	if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
105		{
106	6586	Bits bits;
107	3293	d_bb->makeVariable(n, bits);
108
109	6586	Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
110	3293	d_bbMap.emplace(n, bbt);
111	6586	d_tcpg->addRewriteStep(
112	3293	n, bbt, PfRule::BV_BITBLAST_STEP, {}, {n.eqNode(bbt)});
113		}
114	7999	else if (n.getType().isBitVector())
115		{
116	12874	Bits bits;
117	6437	d_bb->bbTerm(n, bits);
118
119	12874	Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
120	12874	Node rbbt;
121	6437	if (n.isConst())
122		{
123	1746	d_bbMap.emplace(n, bbt);
124	1746	rbbt = n;
125		}
126		else
127		{
128	4691	d_bbMap.emplace(n, bbt);
129	4691	rbbt = reconstruct(n);
130		}
131	12874	d_tcpg->addRewriteStep(
132	6437	rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
133		}
134		else
135		{
136	1562	Assert(n == rwNode);
137		}
138	11292	visit.pop_back();
139		}
140		}
141
142		/* Bit-blast given rewritten bit-vector atom `node`.
143		* Note: This will pre and post-rewrite and store it in the bit-blasting
144		* cache. */
145	1562	d_bb->bbAtom(node);
146	3124	Node result = d_bb->getStoredBBAtom(node);
147
148		// Retrieve bit-blasted `rwNode` without post-rewrite.
149	1562	Node bbt = rwNode.getKind() == kind::CONST_BOOLEAN
150	1562	\|\| rwNode.getKind() == kind::BITVECTOR_BITOF
151	1562	? rwNode
152	3124	: d_bb->applyAtomBBStrategy(rwNode);
153
154	3124	Node rbbt = reconstruct(rwNode);
155
156	3124	d_tcpg->addRewriteStep(
157	1562	rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
158
159	1562	d_bbpg->addBitblastStep(node, bbt, node.eqNode(result));
160		}
161		else
162		{
163	13852	d_bb->bbAtom(node);
164
165		/* Record coarse-grain bit-blast proof step. */
166	13852	if (isProofsEnabled() && !d_recordFineGrainedProofs)
167		{
168	7970	Node bbt = getStoredBBAtom(node);
169	3985	d_bbpg->addBitblastStep(Node(), Node(), node.eqNode(bbt));
170		}
171		}
172	15414	}
173
174	6253	Node BBProof::reconstruct(TNode t)
175		{
176	6253	NodeManager* nm = NodeManager::currentNM();
177
178	12506	std::vector<Node> children;
179	6253	if (t.getMetaKind() == kind::metakind::PARAMETERIZED)
180		{
181	1413	children.push_back(t.getOperator());
182		}
183	17412	for (const auto& child : t)
184		{
185	11159	children.push_back(d_bbMap.at(child));
186		}
187	12506	return nm->mkNode(t.getKind(), children);
188		}
189
190	920950	bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
191
192	24233	bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
193
194	902573	Node BBProof::getStoredBBAtom(TNode node)
195		{
196	902573	return d_bb->getStoredBBAtom(node);
197		}
198
199	123	void BBProof::getBBTerm(TNode node, Bits& bits) const
200		{
201	123	d_bb->getBBTerm(node, bits);
202	123	}
203
204	1614	bool BBProof::collectModelValues(TheoryModel* m,
205		const std::set<Node>& relevantTerms)
206		{
207	1614	return d_bb->collectModelValues(m, relevantTerms);
208		}
209
210	99826	BitblastProofGenerator* BBProof::getProofGenerator() { return d_bbpg.get(); }
211
212	29266	bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
213
214		} // namespace bv
215		} // namespace theory
216	29577	} // namespace cvc5