Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/simple_bitblaster.cpp	Lines:	61	70	87.1 %
Date:	2021-05-24	Branches:	100	270	37.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 for simple BV solver.
 *
 */
#include "theory/bv/bitblast/simple_bitblaster.h"

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

namespace cvc5 {
namespace theory {
namespace bv {

BBSimple::BBSimple(TheoryState* s) : TBitblaster<Node>(), d_state(s) {}

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

  if (hasBBAtom(node))
  {
    return;
  }

  Node normalized = Rewriter::rewrite(node);
  Node atom_bb =
      normalized.getKind() != kind::CONST_BOOLEAN
              && normalized.getKind() != kind::BITVECTOR_BITOF
          ? d_atomBBStrategies[normalized.getKind()](normalized, this)
          : normalized;

  storeBBAtom(node, Rewriter::rewrite(atom_bb));
}

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

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

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

void BBSimple::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 BBSimple::getBBAtom(TNode node) const { return node; }

void BBSimple::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 BBSimple::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 BBSimple::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);
}

bool BBSimple::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 BBSimple::isVariable(TNode node)
{
  return d_variables.find(node) != d_variables.end();
}

}  // 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 for simple BV solver.
14		*
15		*/
16		#include "theory/bv/bitblast/simple_bitblaster.h"
17
18		#include "theory/theory_model.h"
19		#include "theory/theory_state.h"
20
21		namespace cvc5 {
22		namespace theory {
23		namespace bv {
24
25	15	BBSimple::BBSimple(TheoryState* s) : TBitblaster<Node>(), d_state(s) {}
26
27	68	void BBSimple::bbAtom(TNode node)
28		{
29	68	node = node.getKind() == kind::NOT ? node[0] : node;
30
31	68	if (hasBBAtom(node))
32		{
33		return;
34		}
35
36	136	Node normalized = Rewriter::rewrite(node);
37		Node atom_bb =
38	68	normalized.getKind() != kind::CONST_BOOLEAN
39	68	&& normalized.getKind() != kind::BITVECTOR_BITOF
40	136	? d_atomBBStrategies[normalized.getKind()](normalized, this)
41	204	: normalized;
42
43	68	storeBBAtom(node, Rewriter::rewrite(atom_bb));
44		}
45
46	68	void BBSimple::storeBBAtom(TNode atom, Node atom_bb)
47		{
48	68	d_bbAtoms.emplace(atom, atom_bb);
49	68	}
50
51	88	void BBSimple::storeBBTerm(TNode node, const Bits& bits)
52		{
53	88	d_termCache.emplace(node, bits);
54	88	}
55
56	716	bool BBSimple::hasBBAtom(TNode lit) const
57		{
58	716	if (lit.getKind() == kind::NOT)
59		{
60		lit = lit[0];
61		}
62	716	return d_bbAtoms.find(lit) != d_bbAtoms.end();
63		}
64
65	64	void BBSimple::makeVariable(TNode var, Bits& bits)
66		{
67	64	Assert(bits.size() == 0);
68	468	for (unsigned i = 0; i < utils::getSize(var); ++i)
69		{
70	404	bits.push_back(utils::mkBitOf(var, i));
71		}
72	64	d_variables.insert(var);
73	64	}
74
75		Node BBSimple::getBBAtom(TNode node) const { return node; }
76
77	248	void BBSimple::bbTerm(TNode node, Bits& bits)
78		{
79	248	Assert(node.getType().isBitVector());
80	248	if (hasBBTerm(node))
81		{
82	160	getBBTerm(node, bits);
83	160	return;
84		}
85	88	d_termBBStrategies[node.getKind()](node, bits, this);
86	88	Assert(bits.size() == utils::getSize(node));
87	88	storeBBTerm(node, bits);
88		}
89
90	116	Node BBSimple::getStoredBBAtom(TNode node)
91		{
92	116	bool negated = false;
93	116	if (node.getKind() == kind::NOT)
94		{
95		node = node[0];
96		negated = true;
97		}
98
99	116	Assert(hasBBAtom(node));
100	232	Node atom_bb = d_bbAtoms.at(node);
101	232	return negated ? atom_bb.negate() : atom_bb;
102		}
103
104	19	Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel)
105		{
106	19	if (!hasBBTerm(a))
107		{
108		return utils::mkConst(utils::getSize(a), 0u);
109		}
110
111		bool assignment;
112	38	Bits bits;
113	19	getBBTerm(a, bits);
114	38	Integer value(0);
115	38	Integer one(1), zero(0);
116	127	for (int i = bits.size() - 1; i >= 0; --i)
117		{
118	216	Integer bit;
119	108	if (d_state->hasSatValue(bits[i], assignment))
120		{
121	100	bit = assignment ? one : zero;
122		}
123		else
124		{
125	8	bit = zero;
126		}
127	108	value = value * 2 + bit;
128		}
129	19	return utils::mkConst(bits.size(), value);
130		}
131
132	7	bool BBSimple::collectModelValues(TheoryModel* m,
133		const std::set<Node>& relevantTerms)
134		{
135	164	for (const auto& var : relevantTerms)
136		{
137	157	if (d_variables.find(var) == d_variables.end()) continue;
138
139	38	Node const_value = getModelFromSatSolver(var, true);
140	19	Assert(const_value.isNull() \|\| const_value.isConst());
141	19	if (!const_value.isNull())
142		{
143	19	if (!m->assertEquality(var, const_value, true))
144		{
145		return false;
146		}
147		}
148		}
149	7	return true;
150		}
151
152		bool BBSimple::isVariable(TNode node)
153		{
154		return d_variables.find(node) != d_variables.end();
155		}
156
157		} // namespace bv
158		} // namespace theory
159	28191	} // namespace cvc5