Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/proof_bitblaster.cpp	Lines:	27	83	32.5 %
Date:	2021-09-30	Branches:	27	310	8.7 %


/******************************************************************************
 * 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	157	BBProof::BBProof(Env& env,
28		TheoryState* state,
29		ProofNodeManager* pnm,
30	157	bool fineGrained)
31		: EnvObj(env),
32	157	d_bb(new NodeBitblaster(env, state)),
33		d_pnm(pnm),
34	157	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	60	d_tcontext.get(),
46	60	false)
47		: nullptr),
48	60	d_bbpg(pnm ? new BitblastProofGenerator(pnm, d_tcpg.get()) : nullptr),
49	591	d_recordFineGrainedProofs(fineGrained)
50		{
51	157	}
52
53	314	BBProof::~BBProof() {}
54
55	76	void BBProof::bbAtom(TNode node)
56		{
57	76	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	76	if (fineProofs)
72		{
73		std::vector<TNode> visit;
74		std::unordered_set<TNode> visited;
75		NodeManager* nm = NodeManager::currentNM();
76
77		// post-rewrite atom
78		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		visit.push_back(rwNode);
83		while (!visit.empty())
84		{
85		TNode n = visit.back();
86		if (hasBBAtom(n) \|\| hasBBTerm(n))
87		{
88		visit.pop_back();
89		continue;
90		}
91
92		if (visited.find(n) == visited.end())
93		{
94		visited.insert(n);
95		if (!Theory::isLeafOf(n, theory::THEORY_BV))
96		{
97		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		if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
105		{
106		Bits bits;
107		d_bb->makeVariable(n, bits);
108
109		Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
110		d_bbMap.emplace(n, bbt);
111		d_tcpg->addRewriteStep(
112		n, bbt, PfRule::BV_BITBLAST_STEP, {}, {n.eqNode(bbt)});
113		}
114		else if (n.getType().isBitVector())
115		{
116		Bits bits;
117		d_bb->bbTerm(n, bits);
118
119		Node bbt = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
120		Node rbbt;
121		if (n.isConst())
122		{
123		d_bbMap.emplace(n, bbt);
124		rbbt = n;
125		}
126		else
127		{
128		d_bbMap.emplace(n, bbt);
129		rbbt = reconstruct(n);
130		}
131		d_tcpg->addRewriteStep(
132		rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
133		}
134		else
135		{
136		Assert(n == rwNode);
137		}
138		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		d_bb->bbAtom(node);
146		Node result = d_bb->getStoredBBAtom(node);
147
148		// Retrieve bit-blasted `rwNode` without post-rewrite.
149		Node bbt = rwNode.getKind() == kind::CONST_BOOLEAN
150		\|\| rwNode.getKind() == kind::BITVECTOR_BITOF
151		? rwNode
152		: d_bb->applyAtomBBStrategy(rwNode);
153
154		Node rbbt = reconstruct(rwNode);
155
156		d_tcpg->addRewriteStep(
157		rbbt, bbt, PfRule::BV_BITBLAST_STEP, {}, {rbbt.eqNode(bbt)});
158
159		d_bbpg->addBitblastStep(node, bbt, node.eqNode(result));
160		}
161		else
162		{
163	76	d_bb->bbAtom(node);
164
165		/* Record coarse-grain bit-blast proof step. */
166	76	if (isProofsEnabled() && !d_recordFineGrainedProofs)
167		{
168		Node bbt = getStoredBBAtom(node);
169		d_bbpg->addBitblastStep(Node(), Node(), node.eqNode(bbt));
170		}
171		}
172	76	}
173
174		Node BBProof::reconstruct(TNode t)
175		{
176		NodeManager* nm = NodeManager::currentNM();
177
178		std::vector<Node> children;
179		if (t.getMetaKind() == kind::metakind::PARAMETERIZED)
180		{
181		children.push_back(t.getOperator());
182		}
183		for (const auto& child : t)
184		{
185		children.push_back(d_bbMap.at(child));
186		}
187		return nm->mkNode(t.getKind(), children);
188		}
189
190	100	bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
191
192	42	bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
193
194	100	Node BBProof::getStoredBBAtom(TNode node)
195		{
196	100	return d_bb->getStoredBBAtom(node);
197		}
198
199	18	void BBProof::getBBTerm(TNode node, Bits& bits) const
200		{
201	18	d_bb->getBBTerm(node, bits);
202	18	}
203
204	49	bool BBProof::collectModelValues(TheoryModel* m,
205		const std::set<Node>& relevantTerms)
206		{
207	49	return d_bb->collectModelValues(m, relevantTerms);
208		}
209
210		BitblastProofGenerator* BBProof::getProofGenerator() { return d_bbpg.get(); }
211
212	152	bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
213
214		} // namespace bv
215		} // namespace theory
216	22755	} // namespace cvc5