Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/proof_bitblaster.cpp	Lines:	76	76	100.0 %
Date:	2021-08-01	Branches:	151	268	56.3 %


/******************************************************************************
 * 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/theory_model.h"

namespace cvc5 {
namespace theory {
namespace bv {

BBProof::BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained)
    : d_bb(new NodeBitblaster(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_recordFineGrainedProofs(fineGrained)
{
}

BBProof::~BBProof() {}

void BBProof::bbAtom(TNode node)
{
  std::vector<TNode> visit;
  visit.push_back(node);
  std::unordered_set<TNode> visited;

  bool fpenabled = isProofsEnabled() && d_recordFineGrainedProofs;

  NodeManager* nm = NodeManager::currentNM();

  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
    {
      if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
      {
        Bits bits;
        d_bb->makeVariable(n, bits);
        if (fpenabled)
        {
          Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
          d_bbMap.emplace(n, n_tobv);
          d_tcpg->addRewriteStep(n,
                                 n_tobv,
                                 PfRule::BV_BITBLAST_STEP,
                                 {},
                                 {n.eqNode(n_tobv)},
                                 false);
        }
      }
      else if (n.getType().isBitVector())
      {
        Bits bits;
        d_bb->bbTerm(n, bits);
        Kind kind = n.getKind();
        if (fpenabled)
        {
          Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
          d_bbMap.emplace(n, n_tobv);
          Node c_tobv;
          if (n.isConst())
          {
            c_tobv = n;
          }
          else
          {
            std::vector<Node> children_tobv;
            if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
            {
              children_tobv.push_back(n.getOperator());
            }

            for (const auto& child : n)
            {
              children_tobv.push_back(d_bbMap.at(child));
            }
            c_tobv = nm->mkNode(kind, children_tobv);
          }
          d_tcpg->addRewriteStep(c_tobv,
                                 n_tobv,
                                 PfRule::BV_BITBLAST_STEP,
                                 {},
                                 {c_tobv.eqNode(n_tobv)},
                                 false);
        }
      }
      else
      {
        d_bb->bbAtom(n);
        if (fpenabled)
        {
          Node n_tobv = getStoredBBAtom(n);
          std::vector<Node> children_tobv;
          for (const auto& child : n)
          {
            children_tobv.push_back(d_bbMap.at(child));
          }
          Node c_tobv = nm->mkNode(n.getKind(), children_tobv);
          d_tcpg->addRewriteStep(c_tobv,
                                 n_tobv,
                                 PfRule::BV_BITBLAST_STEP,
                                 {},
                                 {c_tobv.eqNode(n_tobv)},
                                 false);
        }
      }
      visit.pop_back();
    }
  }
  /* Record coarse-grain bit-blast proof step. */
  if (isProofsEnabled() && !d_recordFineGrainedProofs)
  {
    Node node_tobv = getStoredBBAtom(node);
    d_tcpg->addRewriteStep(node,
                           node_tobv,
                           PfRule::BV_BITBLAST,
                           {},
                           {node.eqNode(node_tobv)},
                           false);
  }
}

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);
}

TConvProofGenerator* BBProof::getProofGenerator() { return d_tcpg.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/theory_model.h"
21
22		namespace cvc5 {
23		namespace theory {
24		namespace bv {
25
26	5470	BBProof::BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained)
27	5470	: d_bb(new NodeBitblaster(state)),
28		d_pnm(pnm),
29	5470	d_tcontext(new TheoryLeafTermContext(theory::THEORY_BV)),
30		d_tcpg(pnm ? new TConvProofGenerator(
31		pnm,
32		nullptr,
33		/* ONCE to visit each term only once, post-order. FIXPOINT
34		* could lead to infinite loops due to terms being rewritten
35		* to terms that contain themselves */
36		TConvPolicy::ONCE,
37		/* STATIC to get the same ProofNode for a shared subterm. */
38		TConvCachePolicy::STATIC,
39		"BBProof::TConvProofGenerator",
40	2960	d_tcontext.get(),
41	2960	false)
42		: nullptr),
43	19370	d_recordFineGrainedProofs(fineGrained)
44		{
45	5470	}
46
47	5470	BBProof::~BBProof() {}
48
49	15806	void BBProof::bbAtom(TNode node)
50		{
51	31612	std::vector<TNode> visit;
52	15806	visit.push_back(node);
53	31612	std::unordered_set<TNode> visited;
54
55	15806	bool fpenabled = isProofsEnabled() && d_recordFineGrainedProofs;
56
57	15806	NodeManager* nm = NodeManager::currentNM();
58
59	346418	while (!visit.empty())
60		{
61	270495	TNode n = visit.back();
62	225423	if (hasBBAtom(n) \|\| hasBBTerm(n))
63		{
64	60117	visit.pop_back();
65	60117	continue;
66		}
67
68	105189	if (visited.find(n) == visited.end())
69		{
70	52464	visited.insert(n);
71	52464	if (!Theory::isLeafOf(n, theory::THEORY_BV))
72		{
73	39303	visit.insert(visit.end(), n.begin(), n.end());
74		}
75		}
76		else
77		{
78	52725	if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
79		{
80	17646	Bits bits;
81	8823	d_bb->makeVariable(n, bits);
82	8823	if (fpenabled)
83		{
84	7156	Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
85	3578	d_bbMap.emplace(n, n_tobv);
86	7156	d_tcpg->addRewriteStep(n,
87		n_tobv,
88		PfRule::BV_BITBLAST_STEP,
89		{},
90		{n.eqNode(n_tobv)},
91	3578	false);
92		}
93		}
94	43902	else if (n.getType().isBitVector())
95		{
96	56192	Bits bits;
97	28096	d_bb->bbTerm(n, bits);
98	28096	Kind kind = n.getKind();
99	28096	if (fpenabled)
100		{
101	12858	Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
102	6429	d_bbMap.emplace(n, n_tobv);
103	12858	Node c_tobv;
104	6429	if (n.isConst())
105		{
106	1771	c_tobv = n;
107		}
108		else
109		{
110	9316	std::vector<Node> children_tobv;
111	4658	if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
112		{
113	1409	children_tobv.push_back(n.getOperator());
114		}
115
116	12645	for (const auto& child : n)
117		{
118	7987	children_tobv.push_back(d_bbMap.at(child));
119		}
120	4658	c_tobv = nm->mkNode(kind, children_tobv);
121		}
122	12858	d_tcpg->addRewriteStep(c_tobv,
123		n_tobv,
124		PfRule::BV_BITBLAST_STEP,
125		{},
126		{c_tobv.eqNode(n_tobv)},
127	6429	false);
128		}
129		}
130		else
131		{
132	15806	d_bb->bbAtom(n);
133	15806	if (fpenabled)
134		{
135	3456	Node n_tobv = getStoredBBAtom(n);
136	3456	std::vector<Node> children_tobv;
137	5184	for (const auto& child : n)
138		{
139	3456	children_tobv.push_back(d_bbMap.at(child));
140		}
141	3456	Node c_tobv = nm->mkNode(n.getKind(), children_tobv);
142	3456	d_tcpg->addRewriteStep(c_tobv,
143		n_tobv,
144		PfRule::BV_BITBLAST_STEP,
145		{},
146		{c_tobv.eqNode(n_tobv)},
147	1728	false);
148		}
149		}
150	52725	visit.pop_back();
151		}
152		}
153		/* Record coarse-grain bit-blast proof step. */
154	15806	if (isProofsEnabled() && !d_recordFineGrainedProofs)
155		{
156	7838	Node node_tobv = getStoredBBAtom(node);
157	7838	d_tcpg->addRewriteStep(node,
158		node_tobv,
159		PfRule::BV_BITBLAST,
160		{},
161		{node.eqNode(node_tobv)},
162	3919	false);
163		}
164	15806	}
165
166	1164142	bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
167
168	165615	bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
169
170	1006211	Node BBProof::getStoredBBAtom(TNode node)
171		{
172	1006211	return d_bb->getStoredBBAtom(node);
173		}
174
175	123	void BBProof::getBBTerm(TNode node, Bits& bits) const
176		{
177	123	d_bb->getBBTerm(node, bits);
178	123	}
179
180	1633	bool BBProof::collectModelValues(TheoryModel* m,
181		const std::set<Node>& relevantTerms)
182		{
183	1633	return d_bb->collectModelValues(m, relevantTerms);
184		}
185
186	93992	TConvProofGenerator* BBProof::getProofGenerator() { return d_tcpg.get(); }
187
188	31612	bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
189
190		} // namespace bv
191		} // namespace theory
192	29280	} // namespace cvc5