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-11-05	Branches:	53	98	54.1 %


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