Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/bitblast_proof_generator.cpp	Lines:	27	27	100.0 %
Date:	2021-09-18	Branches:	52	96	54.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   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.
 * ****************************************************************************
 *
 * Bitblast proof generator for generating bit-blast proof steps.
 */
#include "theory/bv/bitblast/bitblast_proof_generator.h"

#include "proof/conv_proof_generator.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace theory {
namespace bv {

BitblastProofGenerator::BitblastProofGenerator(ProofNodeManager* pnm,
                                               TConvProofGenerator* tcpg)
    : d_pnm(pnm), d_tcpg(tcpg)
{
}

std::shared_ptr<ProofNode> BitblastProofGenerator::getProofFor(Node eq)
{
  const auto& [t, bbt] = d_cache.at(eq);

  CDProof cdp(d_pnm);
  /* Coarse-grained bit-blast step. */
  if (t.isNull())
  {
    cdp.addStep(eq, PfRule::BV_BITBLAST, {}, {eq});
  }
  else
  {
    /* Fine-grained bit-blast step for bit-blasting bit-vector atoms (bbAtom()).
     * Bit-blasting atoms involves three steps:
     *
     * 1) pre-rewrite: rewrite atom
     * 2) bit-blast rewritten atom
     * 3) post-rewrite: rewrite bit-blasted atom
     *
     * The CDProof is used for constructing the following proof of
     * transitivity:
     *
     * --------- RW  ----------- BB ------------- RW
     *  t = rwt       rwt = bbt      bbt = rwbbt
     * ---------------------------------------------- TRANS
     *                  t = rwbbt
     *
     *
     * where BB corresponds to the conversion proof PI_1 and a bit-blasting
     * step.  Note that if t and bbt remain the same after rewriting the
     * transitivity proof is not needed.
     *
     * The full proof tree is as follows:
     *
     * ------------------- RW        ------------------ BB ------------ RW
     *  P(x,y) = P(x',y')      PI_1   P(x'',y'') = bbt      bbt = rwbbt
     * ------------------------------------------------------------------ TRANS
     *                     P(x,y) = rwbbt
     *
     *
     *      PI_1 :=     -------- BB* ---------- BB*
     *                   x' = x''     y' = y''
     *                  ----------------------- CONG
     *                   P(x',y') = P(x'',y'')
     *
     *
     * where P is an arbitrary bit-vector atom and t := P(x,y), rwt := P(x',y').
     * BB* corresponds to recursively applying bit-blasting to all the
     * sub-terms and recording these bit-blast steps in the conversion proof.
     */

    Node rwt = Rewriter::rewrite(t);

    std::vector<Node> transSteps;

    // Record pre-rewrite of bit-vector atom.
    if (t != rwt)
    {
      cdp.addStep(t.eqNode(rwt), PfRule::REWRITE, {}, {t});
      transSteps.push_back(t.eqNode(rwt));
    }

    // Add bit-blast proof from conversion generator.
    cdp.addProof(d_tcpg->getProofFor(rwt.eqNode(bbt)));
    transSteps.push_back(rwt.eqNode(bbt));

    // Record post-rewrite of bit-blasted term.
    Node rwbbt = Rewriter::rewrite(bbt);
    if (bbt != rwbbt)
    {
      cdp.addStep(bbt.eqNode(rwbbt), PfRule::REWRITE, {}, {bbt});
      transSteps.push_back(bbt.eqNode(rwbbt));
    }

    // If pre- and post-rewrite did not apply, no rewrite steps need to be
    // recorded and the given equality `eq` is already justified by the proof
    // given by the conversion proof generator.
    if (transSteps.size() > 1)
    {
      cdp.addStep(eq, PfRule::TRANS, transSteps, {});
    }
  }

  return cdp.getProofFor(eq);
}

void BitblastProofGenerator::addBitblastStep(TNode t, TNode bbt, TNode eq)
{
  d_cache.emplace(eq, std::make_tuple(t, bbt));
}

}  // 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
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		* Bitblast proof generator for generating bit-blast proof steps.
14		*/
15		#include "theory/bv/bitblast/bitblast_proof_generator.h"
16
17		#include "proof/conv_proof_generator.h"
18		#include "theory/rewriter.h"
19
20		namespace cvc5 {
21		namespace theory {
22		namespace bv {
23
24	2794	BitblastProofGenerator::BitblastProofGenerator(ProofNodeManager* pnm,
25	2794	TConvProofGenerator* tcpg)
26	2794	: d_pnm(pnm), d_tcpg(tcpg)
27		{
28	2794	}
29
30	3124	std::shared_ptr<ProofNode> BitblastProofGenerator::getProofFor(Node eq)
31		{
32	3124	const auto& [t, bbt] = d_cache.at(eq);
33
34	6248	CDProof cdp(d_pnm);
35		/* Coarse-grained bit-blast step. */
36	3124	if (t.isNull())
37		{
38	1562	cdp.addStep(eq, PfRule::BV_BITBLAST, {}, {eq});
39		}
40		else
41		{
42		/* Fine-grained bit-blast step for bit-blasting bit-vector atoms (bbAtom()).
43		* Bit-blasting atoms involves three steps:
44		*
45		* 1) pre-rewrite: rewrite atom
46		* 2) bit-blast rewritten atom
47		* 3) post-rewrite: rewrite bit-blasted atom
48		*
49		* The CDProof is used for constructing the following proof of
50		* transitivity:
51		*
52		* --------- RW ----------- BB ------------- RW
53		* t = rwt rwt = bbt bbt = rwbbt
54		* ---------------------------------------------- TRANS
55		* t = rwbbt
56		*
57		*
58		* where BB corresponds to the conversion proof PI_1 and a bit-blasting
59		* step. Note that if t and bbt remain the same after rewriting the
60		* transitivity proof is not needed.
61		*
62		* The full proof tree is as follows:
63		*
64		* ------------------- RW ------------------ BB ------------ RW
65		* P(x,y) = P(x',y') PI_1 P(x'',y'') = bbt bbt = rwbbt
66		* ------------------------------------------------------------------ TRANS
67		* P(x,y) = rwbbt
68		*
69		*
70		* PI_1 := -------- BB* ---------- BB*
71		* x' = x'' y' = y''
72		* ----------------------- CONG
73		* P(x',y') = P(x'',y'')
74		*
75		*
76		* where P is an arbitrary bit-vector atom and t := P(x,y), rwt := P(x',y').
77		* BB* corresponds to recursively applying bit-blasting to all the
78		* sub-terms and recording these bit-blast steps in the conversion proof.
79		*/
80
81	3124	Node rwt = Rewriter::rewrite(t);
82
83	3124	std::vector<Node> transSteps;
84
85		// Record pre-rewrite of bit-vector atom.
86	1562	if (t != rwt)
87		{
88	17	cdp.addStep(t.eqNode(rwt), PfRule::REWRITE, {}, {t});
89	17	transSteps.push_back(t.eqNode(rwt));
90		}
91
92		// Add bit-blast proof from conversion generator.
93	1562	cdp.addProof(d_tcpg->getProofFor(rwt.eqNode(bbt)));
94	1562	transSteps.push_back(rwt.eqNode(bbt));
95
96		// Record post-rewrite of bit-blasted term.
97	3124	Node rwbbt = Rewriter::rewrite(bbt);
98	1562	if (bbt != rwbbt)
99		{
100	1439	cdp.addStep(bbt.eqNode(rwbbt), PfRule::REWRITE, {}, {bbt});
101	1439	transSteps.push_back(bbt.eqNode(rwbbt));
102		}
103
104		// If pre- and post-rewrite did not apply, no rewrite steps need to be
105		// recorded and the given equality `eq` is already justified by the proof
106		// given by the conversion proof generator.
107	1562	if (transSteps.size() > 1)
108		{
109	1441	cdp.addStep(eq, PfRule::TRANS, transSteps, {});
110		}
111		}
112
113	6248	return cdp.getProofFor(eq);
114		}
115
116	5547	void BitblastProofGenerator::addBitblastStep(TNode t, TNode bbt, TNode eq)
117		{
118	5547	d_cache.emplace(eq, std::make_tuple(t, bbt));
119	5547	}
120
121		} // namespace bv
122		} // namespace theory
123	29574	} // namespace cvc5