Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/proof_bitblaster.cpp	Lines:	77	77	100.0 %
Date:	2021-09-13	Branches:	152	264	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(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_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	5327	BBProof::BBProof(Env& env,
27		TheoryState* state,
28		ProofNodeManager* pnm,
29	5327	bool fineGrained)
30		: EnvObj(env),
31	5327	d_bb(new NodeBitblaster(env, state)),
32		d_pnm(pnm),
33	5327	d_tcontext(new TheoryLeafTermContext(theory::THEORY_BV)),
34		d_tcpg(pnm ? new TConvProofGenerator(
35		pnm,
36		nullptr,
37		/* ONCE to visit each term only once, post-order. FIXPOINT
38		* could lead to infinite loops due to terms being rewritten
39		* to terms that contain themselves */
40		TConvPolicy::ONCE,
41		/* STATIC to get the same ProofNode for a shared subterm. */
42		TConvCachePolicy::STATIC,
43		"BBProof::TConvProofGenerator",
44	2791	d_tcontext.get(),
45	2791	false)
46		: nullptr),
47	18772	d_recordFineGrainedProofs(fineGrained)
48		{
49	5327	}
50
51	9092	BBProof::~BBProof() {}
52
53	15363	void BBProof::bbAtom(TNode node)
54		{
55	30726	std::vector<TNode> visit;
56	15363	visit.push_back(node);
57	30726	std::unordered_set<TNode> visited;
58
59	15363	bool fpenabled = isProofsEnabled() && d_recordFineGrainedProofs;
60
61	15363	NodeManager* nm = NodeManager::currentNM();
62
63	340653	while (!visit.empty())
64		{
65	265515	TNode n = visit.back();
66	222420	if (hasBBAtom(n) \|\| hasBBTerm(n))
67		{
68	59775	visit.pop_back();
69	59775	continue;
70		}
71
72	102870	if (visited.find(n) == visited.end())
73		{
74	51311	visited.insert(n);
75	51311	if (!Theory::isLeafOf(n, theory::THEORY_BV))
76		{
77	38747	visit.insert(visit.end(), n.begin(), n.end());
78		}
79		}
80		else
81		{
82	51559	if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
83		{
84	16474	Bits bits;
85	8237	d_bb->makeVariable(n, bits);
86	8237	if (fpenabled)
87		{
88	6578	Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
89	3289	d_bbMap.emplace(n, n_tobv);
90	6578	d_tcpg->addRewriteStep(n,
91		n_tobv,
92		PfRule::BV_BITBLAST_STEP,
93		{},
94		{n.eqNode(n_tobv)},
95	3289	false);
96		}
97		}
98	43322	else if (n.getType().isBitVector())
99		{
100	55918	Bits bits;
101	27959	d_bb->bbTerm(n, bits);
102	27959	Kind kind = n.getKind();
103	27959	if (fpenabled)
104		{
105	12878	Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
106	6439	d_bbMap.emplace(n, n_tobv);
107	12878	Node c_tobv;
108	6439	if (n.isConst())
109		{
110	1746	c_tobv = n;
111		}
112		else
113		{
114	9386	std::vector<Node> children_tobv;
115	4693	if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
116		{
117	1419	children_tobv.push_back(n.getOperator());
118		}
119
120	12726	for (const auto& child : n)
121		{
122	8033	children_tobv.push_back(d_bbMap.at(child));
123		}
124	4693	c_tobv = nm->mkNode(kind, children_tobv);
125		}
126	12878	d_tcpg->addRewriteStep(c_tobv,
127		n_tobv,
128		PfRule::BV_BITBLAST_STEP,
129		{},
130		{c_tobv.eqNode(n_tobv)},
131	6439	false);
132		}
133		}
134		else
135		{
136	15363	d_bb->bbAtom(n);
137	15363	if (fpenabled)
138		{
139	3124	Node n_tobv = getStoredBBAtom(n);
140	3124	std::vector<Node> children_tobv;
141	4686	for (const auto& child : n)
142		{
143	3124	children_tobv.push_back(d_bbMap.at(child));
144		}
145	3124	Node c_tobv = nm->mkNode(n.getKind(), children_tobv);
146	3124	d_tcpg->addRewriteStep(c_tobv,
147		n_tobv,
148		PfRule::BV_BITBLAST_STEP,
149		{},
150		{c_tobv.eqNode(n_tobv)},
151	1562	false);
152		}
153		}
154	51559	visit.pop_back();
155		}
156		}
157		/* Record coarse-grain bit-blast proof step. */
158	15363	if (isProofsEnabled() && !d_recordFineGrainedProofs)
159		{
160	7924	Node node_tobv = getStoredBBAtom(node);
161	7924	d_tcpg->addRewriteStep(node,
162		node_tobv,
163		PfRule::BV_BITBLAST,
164		{},
165		{node.eqNode(node_tobv)},
166	3962	false);
167		}
168	15363	}
169
170	1053904	bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
171
172	162954	bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
173
174	898345	Node BBProof::getStoredBBAtom(TNode node)
175		{
176	898345	return d_bb->getStoredBBAtom(node);
177		}
178
179	123	void BBProof::getBBTerm(TNode node, Bits& bits) const
180		{
181	123	d_bb->getBBTerm(node, bits);
182	123	}
183
184	1620	bool BBProof::collectModelValues(TheoryModel* m,
185		const std::set<Node>& relevantTerms)
186		{
187	1620	return d_bb->collectModelValues(m, relevantTerms);
188		}
189
190	99856	TConvProofGenerator* BBProof::getProofGenerator() { return d_tcpg.get(); }
191
192	30726	bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
193
194		} // namespace bv
195		} // namespace theory
196	29514	} // namespace cvc5