Head

GCC Code Coverage Report

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