Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/bitblaster.h	Lines:	67	107	62.6 %
Date:	2021-09-29	Branches:	13	262	5.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Liana Hadarean, Mathias Preiner, Alex Ozdemir
 *
 * 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.
 * ****************************************************************************
 *
 * Wrapper around the SAT solver used for bitblasting.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__BV__BITBLAST__BITBLASTER_H
#define CVC5__THEORY__BV__BITBLAST__BITBLASTER_H

#include <unordered_map>
#include <unordered_set>
#include <vector>

#include "expr/node.h"
#include "prop/bv_sat_solver_notify.h"
#include "prop/cnf_stream.h"
#include "prop/registrar.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_types.h"
#include "smt/smt_engine_scope.h"
#include "theory/bv/bitblast/bitblast_strategies_template.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "theory/valuation.h"
#include "util/resource_manager.h"

namespace cvc5 {
namespace theory {
namespace bv {

typedef std::unordered_set<Node> NodeSet;
typedef std::unordered_set<TNode> TNodeSet;

/**
 * The Bitblaster that manages the mapping between Nodes
 * and their bitwise definition
 *
 */

template <class T>
class TBitblaster
{
 protected:
  typedef std::vector<T> Bits;
  typedef std::unordered_map<Node, Bits> TermDefMap;
  typedef std::unordered_set<TNode> TNodeSet;
  typedef std::unordered_map<Node, Node> ModelCache;

  typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster<T>*);
  typedef T (*AtomBBStrategy)(TNode, TBitblaster<T>*);

  // caches and mappings
  TermDefMap d_termCache;
  ModelCache d_modelCache;
  // sat solver used for bitblasting and associated CnfStream
  std::unique_ptr<context::Context> d_nullContext;
  std::unique_ptr<prop::CnfStream> d_cnfStream;

  void initAtomBBStrategies();
  void initTermBBStrategies();

 protected:
  /// function tables for the various bitblasting strategies indexed by node
  /// kind
  TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
  virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
  virtual prop::SatSolver* getSatSolver() = 0;


 public:
  TBitblaster();
  virtual ~TBitblaster() {}
  virtual void bbAtom(TNode node) = 0;
  virtual void bbTerm(TNode node, Bits& bits) = 0;
  virtual void makeVariable(TNode node, Bits& bits) = 0;
  virtual T getBBAtom(TNode atom) const = 0;
  virtual bool hasBBAtom(TNode atom) const = 0;
  virtual void storeBBAtom(TNode atom, T atom_bb) = 0;

  bool hasBBTerm(TNode node) const;
  void getBBTerm(TNode node, Bits& bits) const;
  virtual void storeBBTerm(TNode term, const Bits& bits);

  /**
   * Return a constant representing the value of a in the  model.
   * If fullModel is true set unconstrained bits to 0. If not return
   * NullNode() for a fully or partially unconstrained.
   *
   */
  Node getTermModel(TNode node, bool fullModel);
  void invalidateModelCache();
};

class MinisatEmptyNotify : public prop::BVSatSolverNotify
{
 public:
  MinisatEmptyNotify() {}
  bool notify(prop::SatLiteral lit) override { return true; }
  void notify(prop::SatClause& clause) override {}
  void spendResource(Resource r) override
  {
    smt::currentResourceManager()->spendResource(r);
  }

  void safePoint(Resource r) override {}
};

// Bitblaster implementation

template <class T>
void TBitblaster<T>::initAtomBBStrategies()
{
  for (int i = 0; i < kind::LAST_KIND; ++i)
  {
    d_atomBBStrategies[i] = UndefinedAtomBBStrategy<T>;
  }
  /// setting default bb strategies for atoms
  d_atomBBStrategies[kind::EQUAL] = DefaultEqBB<T>;
  d_atomBBStrategies[kind::BITVECTOR_ULT] = DefaultUltBB<T>;
  d_atomBBStrategies[kind::BITVECTOR_ULE] = DefaultUleBB<T>;
  d_atomBBStrategies[kind::BITVECTOR_UGT] = DefaultUgtBB<T>;
  d_atomBBStrategies[kind::BITVECTOR_UGE] = DefaultUgeBB<T>;
  d_atomBBStrategies[kind::BITVECTOR_SLT] = DefaultSltBB<T>;
  d_atomBBStrategies[kind::BITVECTOR_SLE] = DefaultSleBB<T>;
  d_atomBBStrategies[kind::BITVECTOR_SGT] = DefaultSgtBB<T>;
  d_atomBBStrategies[kind::BITVECTOR_SGE] = DefaultSgeBB<T>;
}

template <class T>
void TBitblaster<T>::initTermBBStrategies()
{
  for (int i = 0; i < kind::LAST_KIND; ++i)
  {
    d_termBBStrategies[i] = DefaultVarBB<T>;
  }
  /// setting default bb strategies for terms:
  d_termBBStrategies[kind::CONST_BITVECTOR] = DefaultConstBB<T>;
  d_termBBStrategies[kind::BITVECTOR_NOT] = DefaultNotBB<T>;
  d_termBBStrategies[kind::BITVECTOR_CONCAT] = DefaultConcatBB<T>;
  d_termBBStrategies[kind::BITVECTOR_AND] = DefaultAndBB<T>;
  d_termBBStrategies[kind::BITVECTOR_OR] = DefaultOrBB<T>;
  d_termBBStrategies[kind::BITVECTOR_XOR] = DefaultXorBB<T>;
  d_termBBStrategies[kind::BITVECTOR_XNOR] = DefaultXnorBB<T>;
  d_termBBStrategies[kind::BITVECTOR_NAND] = DefaultNandBB<T>;
  d_termBBStrategies[kind::BITVECTOR_NOR] = DefaultNorBB<T>;
  d_termBBStrategies[kind::BITVECTOR_COMP] = DefaultCompBB<T>;
  d_termBBStrategies[kind::BITVECTOR_MULT] = DefaultMultBB<T>;
  d_termBBStrategies[kind::BITVECTOR_ADD] = DefaultAddBB<T>;
  d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>;
  d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>;
  d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB<T>;
  d_termBBStrategies[kind::BITVECTOR_UREM] = DefaultUremBB<T>;
  d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy<T>;
  d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy<T>;
  d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy<T>;
  d_termBBStrategies[kind::BITVECTOR_SHL] = DefaultShlBB<T>;
  d_termBBStrategies[kind::BITVECTOR_LSHR] = DefaultLshrBB<T>;
  d_termBBStrategies[kind::BITVECTOR_ASHR] = DefaultAshrBB<T>;
  d_termBBStrategies[kind::BITVECTOR_ULTBV] = DefaultUltbvBB<T>;
  d_termBBStrategies[kind::BITVECTOR_SLTBV] = DefaultSltbvBB<T>;
  d_termBBStrategies[kind::BITVECTOR_ITE] = DefaultIteBB<T>;
  d_termBBStrategies[kind::BITVECTOR_EXTRACT] = DefaultExtractBB<T>;
  d_termBBStrategies[kind::BITVECTOR_REPEAT] = DefaultRepeatBB<T>;
  d_termBBStrategies[kind::BITVECTOR_ZERO_EXTEND] = DefaultZeroExtendBB<T>;
  d_termBBStrategies[kind::BITVECTOR_SIGN_EXTEND] = DefaultSignExtendBB<T>;
  d_termBBStrategies[kind::BITVECTOR_ROTATE_RIGHT] = DefaultRotateRightBB<T>;
  d_termBBStrategies[kind::BITVECTOR_ROTATE_LEFT] = DefaultRotateLeftBB<T>;
}

template <class T>
TBitblaster<T>::TBitblaster()
    : d_termCache(),
      d_modelCache(),
      d_nullContext(new context::Context()),
      d_cnfStream()
{
  initAtomBBStrategies();
  initTermBBStrategies();
}

template <class T>
bool TBitblaster<T>::hasBBTerm(TNode node) const
{
  return d_termCache.find(node) != d_termCache.end();
}
template <class T>
void TBitblaster<T>::getBBTerm(TNode node, Bits& bits) const
{
  Assert(hasBBTerm(node));
  bits = d_termCache.find(node)->second;
}

template <class T>
void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits)
{
  d_termCache.insert(std::make_pair(node, bits));
}

template <class T>
void TBitblaster<T>::invalidateModelCache()
{
  d_modelCache.clear();
}

template <class T>
Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
{
  if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node];

  if (node.isConst()) return node;

  Node value = getModelFromSatSolver(node, false);
  if (!value.isNull())
  {
    Debug("bv-equality-status")
        << "TLazyBitblaster::getTermModel from SatSolver" << node << " => "
        << value << "\n";
    d_modelCache[node] = value;
    Assert(value.isConst());
    return value;
  }

  if (Theory::isLeafOf(node, theory::THEORY_BV))
  {
    // if it is a leaf may ask for fullModel
    value = getModelFromSatSolver(node, true);
    Debug("bv-equality-status") << "TLazyBitblaster::getTermModel from VarValue"
                                << node << " => " << value << "\n";
    Assert((fullModel && !value.isNull() && value.isConst()) || !fullModel);
    if (!value.isNull())
    {
      d_modelCache[node] = value;
    }
    return value;
  }
  Assert(node.getType().isBitVector());

  NodeBuilder nb(node.getKind());
  if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
  {
    nb << node.getOperator();
  }

  for (unsigned i = 0; i < node.getNumChildren(); ++i)
  {
    nb << getTermModel(node[i], fullModel);
  }
  value = nb;
  value = Rewriter::rewrite(value);
  Assert(value.isConst());
  d_modelCache[node] = value;
  Debug("bv-term-model") << "TLazyBitblaster::getTermModel Building Value"
                         << node << " => " << value << "\n";
  return value;
}

}  // namespace bv
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__BV__BITBLAST__BITBLASTER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Liana Hadarean, Mathias Preiner, Alex Ozdemir
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		* Wrapper around the SAT solver used for bitblasting.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__BV__BITBLAST__BITBLASTER_H
19		#define CVC5__THEORY__BV__BITBLAST__BITBLASTER_H
20
21		#include <unordered_map>
22		#include <unordered_set>
23		#include <vector>
24
25		#include "expr/node.h"
26		#include "prop/bv_sat_solver_notify.h"
27		#include "prop/cnf_stream.h"
28		#include "prop/registrar.h"
29		#include "prop/sat_solver.h"
30		#include "prop/sat_solver_types.h"
31		#include "smt/smt_engine_scope.h"
32		#include "theory/bv/bitblast/bitblast_strategies_template.h"
33		#include "theory/rewriter.h"
34		#include "theory/theory.h"
35		#include "theory/valuation.h"
36		#include "util/resource_manager.h"
37
38		namespace cvc5 {
39		namespace theory {
40		namespace bv {
41
42		typedef std::unordered_set<Node> NodeSet;
43		typedef std::unordered_set<TNode> TNodeSet;
44
45		/**
46		* The Bitblaster that manages the mapping between Nodes
47		* and their bitwise definition
48		*
49		*/
50
51		template <class T>
52		class TBitblaster
53		{
54		protected:
55		typedef std::vector<T> Bits;
56		typedef std::unordered_map<Node, Bits> TermDefMap;
57		typedef std::unordered_set<TNode> TNodeSet;
58		typedef std::unordered_map<Node, Node> ModelCache;
59
60		typedef void (TermBBStrategy)(TNode, Bits&, TBitblaster<T>);
61		typedef T (AtomBBStrategy)(TNode, TBitblaster<T>);
62
63		// caches and mappings
64		TermDefMap d_termCache;
65		ModelCache d_modelCache;
66		// sat solver used for bitblasting and associated CnfStream
67		std::unique_ptr<context::Context> d_nullContext;
68		std::unique_ptr<prop::CnfStream> d_cnfStream;
69
70		void initAtomBBStrategies();
71		void initTermBBStrategies();
72
73		protected:
74		/// function tables for the various bitblasting strategies indexed by node
75		/// kind
76		TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
77		AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
78		virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
79		virtual prop::SatSolver* getSatSolver() = 0;
80
81
82		public:
83		TBitblaster();
84	6268	virtual ~TBitblaster() {}
85		virtual void bbAtom(TNode node) = 0;
86		virtual void bbTerm(TNode node, Bits& bits) = 0;
87		virtual void makeVariable(TNode node, Bits& bits) = 0;
88		virtual T getBBAtom(TNode atom) const = 0;
89		virtual bool hasBBAtom(TNode atom) const = 0;
90		virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
91
92		bool hasBBTerm(TNode node) const;
93		void getBBTerm(TNode node, Bits& bits) const;
94		virtual void storeBBTerm(TNode term, const Bits& bits);
95
96		/**
97		* Return a constant representing the value of a in the model.
98		* If fullModel is true set unconstrained bits to 0. If not return
99		* NullNode() for a fully or partially unconstrained.
100		*
101		*/
102		Node getTermModel(TNode node, bool fullModel);
103		void invalidateModelCache();
104		};
105
106	4	class MinisatEmptyNotify : public prop::BVSatSolverNotify
107		{
108		public:
109	2	MinisatEmptyNotify() {}
110		bool notify(prop::SatLiteral lit) override { return true; }
111		void notify(prop::SatClause& clause) override {}
112	4	void spendResource(Resource r) override
113		{
114	4	smt::currentResourceManager()->spendResource(r);
115	4	}
116
117	1940	void safePoint(Resource r) override {}
118		};
119
120		// Bitblaster implementation
121
122		template <class T>
123	6271	void TBitblaster<T>::initAtomBBStrategies()
124		{
125	2056888	for (int i = 0; i < kind::LAST_KIND; ++i)
126		{
127	2050617	d_atomBBStrategies[i] = UndefinedAtomBBStrategy<T>;
128		}
129		/// setting default bb strategies for atoms
130	6271	d_atomBBStrategies[kind::EQUAL] = DefaultEqBB<T>;
131	6271	d_atomBBStrategies[kind::BITVECTOR_ULT] = DefaultUltBB<T>;
132	6271	d_atomBBStrategies[kind::BITVECTOR_ULE] = DefaultUleBB<T>;
133	6271	d_atomBBStrategies[kind::BITVECTOR_UGT] = DefaultUgtBB<T>;
134	6271	d_atomBBStrategies[kind::BITVECTOR_UGE] = DefaultUgeBB<T>;
135	6271	d_atomBBStrategies[kind::BITVECTOR_SLT] = DefaultSltBB<T>;
136	6271	d_atomBBStrategies[kind::BITVECTOR_SLE] = DefaultSleBB<T>;
137	6271	d_atomBBStrategies[kind::BITVECTOR_SGT] = DefaultSgtBB<T>;
138	6271	d_atomBBStrategies[kind::BITVECTOR_SGE] = DefaultSgeBB<T>;
139	6271	}
140
141		template <class T>
142	6271	void TBitblaster<T>::initTermBBStrategies()
143		{
144	2056888	for (int i = 0; i < kind::LAST_KIND; ++i)
145		{
146	2050617	d_termBBStrategies[i] = DefaultVarBB<T>;
147		}
148		/// setting default bb strategies for terms:
149	6271	d_termBBStrategies[kind::CONST_BITVECTOR] = DefaultConstBB<T>;
150	6271	d_termBBStrategies[kind::BITVECTOR_NOT] = DefaultNotBB<T>;
151	6271	d_termBBStrategies[kind::BITVECTOR_CONCAT] = DefaultConcatBB<T>;
152	6271	d_termBBStrategies[kind::BITVECTOR_AND] = DefaultAndBB<T>;
153	6271	d_termBBStrategies[kind::BITVECTOR_OR] = DefaultOrBB<T>;
154	6271	d_termBBStrategies[kind::BITVECTOR_XOR] = DefaultXorBB<T>;
155	6271	d_termBBStrategies[kind::BITVECTOR_XNOR] = DefaultXnorBB<T>;
156	6271	d_termBBStrategies[kind::BITVECTOR_NAND] = DefaultNandBB<T>;
157	6271	d_termBBStrategies[kind::BITVECTOR_NOR] = DefaultNorBB<T>;
158	6271	d_termBBStrategies[kind::BITVECTOR_COMP] = DefaultCompBB<T>;
159	6271	d_termBBStrategies[kind::BITVECTOR_MULT] = DefaultMultBB<T>;
160	6271	d_termBBStrategies[kind::BITVECTOR_ADD] = DefaultAddBB<T>;
161	6271	d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>;
162	6271	d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>;
163	6271	d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB<T>;
164	6271	d_termBBStrategies[kind::BITVECTOR_UREM] = DefaultUremBB<T>;
165	6271	d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy<T>;
166	6271	d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy<T>;
167	6271	d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy<T>;
168	6271	d_termBBStrategies[kind::BITVECTOR_SHL] = DefaultShlBB<T>;
169	6271	d_termBBStrategies[kind::BITVECTOR_LSHR] = DefaultLshrBB<T>;
170	6271	d_termBBStrategies[kind::BITVECTOR_ASHR] = DefaultAshrBB<T>;
171	6271	d_termBBStrategies[kind::BITVECTOR_ULTBV] = DefaultUltbvBB<T>;
172	6271	d_termBBStrategies[kind::BITVECTOR_SLTBV] = DefaultSltbvBB<T>;
173	6271	d_termBBStrategies[kind::BITVECTOR_ITE] = DefaultIteBB<T>;
174	6271	d_termBBStrategies[kind::BITVECTOR_EXTRACT] = DefaultExtractBB<T>;
175	6271	d_termBBStrategies[kind::BITVECTOR_REPEAT] = DefaultRepeatBB<T>;
176	6271	d_termBBStrategies[kind::BITVECTOR_ZERO_EXTEND] = DefaultZeroExtendBB<T>;
177	6271	d_termBBStrategies[kind::BITVECTOR_SIGN_EXTEND] = DefaultSignExtendBB<T>;
178	6271	d_termBBStrategies[kind::BITVECTOR_ROTATE_RIGHT] = DefaultRotateRightBB<T>;
179	6271	d_termBBStrategies[kind::BITVECTOR_ROTATE_LEFT] = DefaultRotateLeftBB<T>;
180	6271	}
181
182		template <class T>
183	6271	TBitblaster<T>::TBitblaster()
184		: d_termCache(),
185		d_modelCache(),
186	6271	d_nullContext(new context::Context()),
187	12542	d_cnfStream()
188		{
189	6271	initAtomBBStrategies();
190	6271	initTermBBStrategies();
191	6271	}
192
193		template <class T>
194	319346	bool TBitblaster<T>::hasBBTerm(TNode node) const
195		{
196	319346	return d_termCache.find(node) != d_termCache.end();
197		}
198		template <class T>
199	131659	void TBitblaster<T>::getBBTerm(TNode node, Bits& bits) const
200		{
201	131659	Assert(hasBBTerm(node));
202	131659	bits = d_termCache.find(node)->second;
203	131659	}
204
205		template <class T>
206		void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits)
207		{
208		d_termCache.insert(std::make_pair(node, bits));
209		}
210
211		template <class T>
212		void TBitblaster<T>::invalidateModelCache()
213		{
214		d_modelCache.clear();
215		}
216
217		template <class T>
218		Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
219		{
220		if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node];
221
222		if (node.isConst()) return node;
223
224		Node value = getModelFromSatSolver(node, false);
225		if (!value.isNull())
226		{
227		Debug("bv-equality-status")
228		<< "TLazyBitblaster::getTermModel from SatSolver" << node << " => "
229		<< value << "\n";
230		d_modelCache[node] = value;
231		Assert(value.isConst());
232		return value;
233		}
234
235		if (Theory::isLeafOf(node, theory::THEORY_BV))
236		{
237		// if it is a leaf may ask for fullModel
238		value = getModelFromSatSolver(node, true);
239		Debug("bv-equality-status") << "TLazyBitblaster::getTermModel from VarValue"
240		<< node << " => " << value << "\n";
241		Assert((fullModel && !value.isNull() && value.isConst()) \|\| !fullModel);
242		if (!value.isNull())
243		{
244		d_modelCache[node] = value;
245		}
246		return value;
247		}
248		Assert(node.getType().isBitVector());
249
250		NodeBuilder nb(node.getKind());
251		if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
252		{
253		nb << node.getOperator();
254		}
255
256		for (unsigned i = 0; i < node.getNumChildren(); ++i)
257		{
258		nb << getTermModel(node[i], fullModel);
259		}
260		value = nb;
261		value = Rewriter::rewrite(value);
262		Assert(value.isConst());
263		d_modelCache[node] = value;
264		Debug("bv-term-model") << "TLazyBitblaster::getTermModel Building Value"
265		<< node << " => " << value << "\n";
266		return value;
267		}
268
269		} // namespace bv
270		} // namespace theory
271		} // namespace cvc5
272
273		#endif /* CVC5__THEORY__BV__BITBLAST__BITBLASTER_H */