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-16	Branches:	151	262	57.6 %


/******************************************************************************
 * 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	5317	BBProof::BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained)
27	5317	: d_bb(new NodeBitblaster(state)),
28		d_pnm(pnm),
29	5317	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	2801	d_tcontext.get(),
41	2801	false)
42		: nullptr),
43	18752	d_recordFineGrainedProofs(fineGrained)
44		{
45	5317	}
46
47	5317	BBProof::~BBProof() {}
48
49	15368	void BBProof::bbAtom(TNode node)
50		{
51	30736	std::vector<TNode> visit;
52	15368	visit.push_back(node);
53	30736	std::unordered_set<TNode> visited;
54
55	15368	bool fpenabled = isProofsEnabled() && d_recordFineGrainedProofs;
56
57	15368	NodeManager* nm = NodeManager::currentNM();
58
59	340794	while (!visit.empty())
60		{
61	265641	TNode n = visit.back();
62	222498	if (hasBBAtom(n) \|\| hasBBTerm(n))
63		{
64	59785	visit.pop_back();
65	59785	continue;
66		}
67
68	102928	if (visited.find(n) == visited.end())
69		{
70	51340	visited.insert(n);
71	51340	if (!Theory::isLeafOf(n, theory::THEORY_BV))
72		{
73	38761	visit.insert(visit.end(), n.begin(), n.end());
74		}
75		}
76		else
77		{
78	51588	if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
79		{
80	16494	Bits bits;
81	8247	d_bb->makeVariable(n, bits);
82	8247	if (fpenabled)
83		{
84	6592	Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
85	3296	d_bbMap.emplace(n, n_tobv);
86	6592	d_tcpg->addRewriteStep(n,
87		n_tobv,
88		PfRule::BV_BITBLAST_STEP,
89		{},
90		{n.eqNode(n_tobv)},
91	3296	false);
92		}
93		}
94	43341	else if (n.getType().isBitVector())
95		{
96	55946	Bits bits;
97	27973	d_bb->bbTerm(n, bits);
98	27973	Kind kind = n.getKind();
99	27973	if (fpenabled)
100		{
101	12886	Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
102	6443	d_bbMap.emplace(n, n_tobv);
103	12886	Node c_tobv;
104	6443	if (n.isConst())
105		{
106	1749	c_tobv = n;
107		}
108		else
109		{
110	9388	std::vector<Node> children_tobv;
111	4694	if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
112		{
113	1415	children_tobv.push_back(n.getOperator());
114		}
115
116	12733	for (const auto& child : n)
117		{
118	8039	children_tobv.push_back(d_bbMap.at(child));
119		}
120	4694	c_tobv = nm->mkNode(kind, children_tobv);
121		}
122	12886	d_tcpg->addRewriteStep(c_tobv,
123		n_tobv,
124		PfRule::BV_BITBLAST_STEP,
125		{},
126		{c_tobv.eqNode(n_tobv)},
127	6443	false);
128		}
129		}
130		else
131		{
132	15368	d_bb->bbAtom(n);
133	15368	if (fpenabled)
134		{
135	3132	Node n_tobv = getStoredBBAtom(n);
136	3132	std::vector<Node> children_tobv;
137	4698	for (const auto& child : n)
138		{
139	3132	children_tobv.push_back(d_bbMap.at(child));
140		}
141	3132	Node c_tobv = nm->mkNode(n.getKind(), children_tobv);
142	3132	d_tcpg->addRewriteStep(c_tobv,
143		n_tobv,
144		PfRule::BV_BITBLAST_STEP,
145		{},
146		{c_tobv.eqNode(n_tobv)},
147	1566	false);
148		}
149		}
150	51588	visit.pop_back();
151		}
152		}
153		/* Record coarse-grain bit-blast proof step. */
154	15368	if (isProofsEnabled() && !d_recordFineGrainedProofs)
155		{
156	7936	Node node_tobv = getStoredBBAtom(node);
157	7936	d_tcpg->addRewriteStep(node,
158		node_tobv,
159		PfRule::BV_BITBLAST,
160		{},
161		{node.eqNode(node_tobv)},
162	3968	false);
163		}
164	15368	}
165
166	1010657	bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
167
168	163022	bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
169
170	855044	Node BBProof::getStoredBBAtom(TNode node)
171		{
172	855044	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	100291	TConvProofGenerator* BBProof::getProofGenerator() { return d_tcpg.get(); }
187
188	30736	bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
189
190		} // namespace bv
191		} // namespace theory
192	29340	} // namespace cvc5