Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/node_bitblaster.cpp	Lines:	77	81	95.1 %
Date:	2021-09-15	Branches:	124	326	38.0 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Bitblaster used to bitblast to Boolean Nodes.
 */
#include "theory/bv/bitblast/node_bitblaster.h"

#include "options/bv_options.h"
#include "theory/theory_model.h"
#include "theory/theory_state.h"

namespace cvc5 {
namespace theory {
namespace bv {

NodeBitblaster::NodeBitblaster(Env& env, TheoryState* s)
    : TBitblaster<Node>(), EnvObj(env), d_state(s)
{
}

void NodeBitblaster::bbAtom(TNode node)
{
  node = node.getKind() == kind::NOT ? node[0] : node;

  if (hasBBAtom(node))
  {
    return;
  }

  /* Note: We rewrite here since it's not guaranteed (yet) that facts sent
   * to theories are rewritten.
   */
  Node normalized = rewrite(node);
  Node atom_bb =
      normalized.getKind() != kind::CONST_BOOLEAN
              && normalized.getKind() != kind::BITVECTOR_BITOF
          ? d_atomBBStrategies[normalized.getKind()](normalized, this)
          : normalized;

  storeBBAtom(node, rewrite(atom_bb));
}

void NodeBitblaster::storeBBAtom(TNode atom, Node atom_bb)
{
  d_bbAtoms.emplace(atom, atom_bb);
}

void NodeBitblaster::storeBBTerm(TNode node, const Bits& bits)
{
  d_termCache.emplace(node, bits);
}

bool NodeBitblaster::hasBBAtom(TNode lit) const
{
  if (lit.getKind() == kind::NOT)
  {
    lit = lit[0];
  }
  return d_bbAtoms.find(lit) != d_bbAtoms.end();
}

void NodeBitblaster::makeVariable(TNode var, Bits& bits)
{
  Assert(bits.size() == 0);
  for (unsigned i = 0; i < utils::getSize(var); ++i)
  {
    bits.push_back(utils::mkBitOf(var, i));
  }
  d_variables.insert(var);
}

Node NodeBitblaster::getBBAtom(TNode node) const { return node; }

void NodeBitblaster::bbTerm(TNode node, Bits& bits)
{
  Assert(node.getType().isBitVector());
  if (hasBBTerm(node))
  {
    getBBTerm(node, bits);
    return;
  }
  d_termBBStrategies[node.getKind()](node, bits, this);
  Assert(bits.size() == utils::getSize(node));
  storeBBTerm(node, bits);
}

Node NodeBitblaster::getStoredBBAtom(TNode node)
{
  bool negated = false;
  if (node.getKind() == kind::NOT)
  {
    node = node[0];
    negated = true;
  }

  Assert(hasBBAtom(node));
  Node atom_bb = d_bbAtoms.at(node);
  return negated ? atom_bb.negate() : atom_bb;
}

Node NodeBitblaster::getModelFromSatSolver(TNode a, bool fullModel)
{
  if (!hasBBTerm(a))
  {
    return utils::mkConst(utils::getSize(a), 0u);
  }

  bool assignment;
  Bits bits;
  getBBTerm(a, bits);
  Integer value(0);
  Integer one(1), zero(0);
  for (int i = bits.size() - 1; i >= 0; --i)
  {
    Integer bit;
    if (d_state->hasSatValue(bits[i], assignment))
    {
      bit = assignment ? one : zero;
    }
    else
    {
      bit = zero;
    }
    value = value * 2 + bit;
  }
  return utils::mkConst(bits.size(), value);
}

void NodeBitblaster::computeRelevantTerms(std::set<Node>& termSet)
{
  Assert(options().bv.bitblastMode == options::BitblastMode::EAGER);
  for (const auto& var : d_variables)
  {
    termSet.insert(var);
  }
}

bool NodeBitblaster::collectModelValues(TheoryModel* m,
                                        const std::set<Node>& relevantTerms)
{
  for (const auto& var : relevantTerms)
  {
    if (d_variables.find(var) == d_variables.end()) continue;

    Node const_value = getModelFromSatSolver(var, true);
    Assert(const_value.isNull() || const_value.isConst());
    if (!const_value.isNull())
    {
      if (!m->assertEquality(var, const_value, true))
      {
        return false;
      }
    }
  }
  return true;
}

bool NodeBitblaster::isVariable(TNode node)
{
  return d_variables.find(node) != d_variables.end();
}

Node NodeBitblaster::applyAtomBBStrategy(TNode node)
{
  Assert(node.getKind() != kind::CONST_BOOLEAN);
  Assert(node.getKind() != kind::BITVECTOR_BITOF);
  return d_atomBBStrategies[node.getKind()](node, this);
}

}  // 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		* Bitblaster used to bitblast to Boolean Nodes.
14		*/
15		#include "theory/bv/bitblast/node_bitblaster.h"
16
17		#include "options/bv_options.h"
18		#include "theory/theory_model.h"
19		#include "theory/theory_state.h"
20
21		namespace cvc5 {
22		namespace theory {
23		namespace bv {
24
25	11500	NodeBitblaster::NodeBitblaster(Env& env, TheoryState* s)
26	11500	: TBitblaster<Node>(), EnvObj(env), d_state(s)
27		{
28	11500	}
29
30	2537226	void NodeBitblaster::bbAtom(TNode node)
31		{
32	2537226	node = node.getKind() == kind::NOT ? node[0] : node;
33
34	2537226	if (hasBBAtom(node))
35		{
36	2486045	return;
37		}
38
39		/* Note: We rewrite here since it's not guaranteed (yet) that facts sent
40		* to theories are rewritten.
41		*/
42	102362	Node normalized = rewrite(node);
43		Node atom_bb =
44	51181	normalized.getKind() != kind::CONST_BOOLEAN
45	51127	&& normalized.getKind() != kind::BITVECTOR_BITOF
46	102308	? d_atomBBStrategies[normalized.getKind()](normalized, this)
47	153489	: normalized;
48
49	51181	storeBBAtom(node, rewrite(atom_bb));
50		}
51
52	51181	void NodeBitblaster::storeBBAtom(TNode atom, Node atom_bb)
53		{
54	51181	d_bbAtoms.emplace(atom, atom_bb);
55	51181	}
56
57	90431	void NodeBitblaster::storeBBTerm(TNode node, const Bits& bits)
58		{
59	90431	d_termCache.emplace(node, bits);
60	90431	}
61
62	6884123	bool NodeBitblaster::hasBBAtom(TNode lit) const
63		{
64	6884123	if (lit.getKind() == kind::NOT)
65		{
66		lit = lit[0];
67		}
68	6884123	return d_bbAtoms.find(lit) != d_bbAtoms.end();
69		}
70
71	22853	void NodeBitblaster::makeVariable(TNode var, Bits& bits)
72		{
73	22853	Assert(bits.size() == 0);
74	267895	for (unsigned i = 0; i < utils::getSize(var); ++i)
75		{
76	245042	bits.push_back(utils::mkBitOf(var, i));
77		}
78	22853	d_variables.insert(var);
79	22853	}
80
81		Node NodeBitblaster::getBBAtom(TNode node) const { return node; }
82
83	262695	void NodeBitblaster::bbTerm(TNode node, Bits& bits)
84		{
85	262695	Assert(node.getType().isBitVector());
86	262695	if (hasBBTerm(node))
87		{
88	172264	getBBTerm(node, bits);
89	172264	return;
90		}
91	90431	d_termBBStrategies[node.getKind()](node, bits, this);
92	90431	Assert(bits.size() == utils::getSize(node));
93	90431	storeBBTerm(node, bits);
94		}
95
96	3425947	Node NodeBitblaster::getStoredBBAtom(TNode node)
97		{
98	3425947	bool negated = false;
99	3425947	if (node.getKind() == kind::NOT)
100		{
101	1155391	node = node[0];
102	1155391	negated = true;
103		}
104
105	3425947	Assert(hasBBAtom(node));
106	6851894	Node atom_bb = d_bbAtoms.at(node);
107	6851894	return negated ? atom_bb.negate() : atom_bb;
108		}
109
110	4306	Node NodeBitblaster::getModelFromSatSolver(TNode a, bool fullModel)
111		{
112	4306	if (!hasBBTerm(a))
113		{
114		return utils::mkConst(utils::getSize(a), 0u);
115		}
116
117		bool assignment;
118	8612	Bits bits;
119	4306	getBBTerm(a, bits);
120	8612	Integer value(0);
121	8612	Integer one(1), zero(0);
122	45481	for (int i = bits.size() - 1; i >= 0; --i)
123		{
124	82350	Integer bit;
125	41175	if (d_state->hasSatValue(bits[i], assignment))
126		{
127	36841	bit = assignment ? one : zero;
128		}
129		else
130		{
131	4334	bit = zero;
132		}
133	41175	value = value * 2 + bit;
134		}
135	4306	return utils::mkConst(bits.size(), value);
136		}
137
138	11	void NodeBitblaster::computeRelevantTerms(std::set<Node>& termSet)
139		{
140	11	Assert(options().bv.bitblastMode == options::BitblastMode::EAGER);
141	36	for (const auto& var : d_variables)
142		{
143	25	termSet.insert(var);
144		}
145	11	}
146
147	1614	bool NodeBitblaster::collectModelValues(TheoryModel* m,
148		const std::set<Node>& relevantTerms)
149		{
150	274746	for (const auto& var : relevantTerms)
151		{
152	273132	if (d_variables.find(var) == d_variables.end()) continue;
153
154	8612	Node const_value = getModelFromSatSolver(var, true);
155	4306	Assert(const_value.isNull() \|\| const_value.isConst());
156	4306	if (!const_value.isNull())
157		{
158	4306	if (!m->assertEquality(var, const_value, true))
159		{
160		return false;
161		}
162		}
163		}
164	1614	return true;
165		}
166
167	186570	bool NodeBitblaster::isVariable(TNode node)
168		{
169	186570	return d_variables.find(node) != d_variables.end();
170		}
171
172	1562	Node NodeBitblaster::applyAtomBBStrategy(TNode node)
173		{
174	1562	Assert(node.getKind() != kind::CONST_BOOLEAN);
175	1562	Assert(node.getKind() != kind::BITVECTOR_BITOF);
176	1562	return d_atomBBStrategies[node.getKind()](node, this);
177		}
178
179		} // namespace bv
180		} // namespace theory
181	29577	} // namespace cvc5