Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/bitblaster.h	Lines:	61	64	95.3 %
Date:	2021-11-07	Branches:	13	36	36.1 %


/******************************************************************************
 * 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/cnf_stream.h"
#include "prop/registrar.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_types.h"
#include "smt/solver_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();
};

// 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();
}

}  // 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/cnf_stream.h"
27		#include "prop/registrar.h"
28		#include "prop/sat_solver.h"
29		#include "prop/sat_solver_types.h"
30		#include "smt/solver_engine_scope.h"
31		#include "theory/bv/bitblast/bitblast_strategies_template.h"
32		#include "theory/rewriter.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	16836	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		// Bitblaster implementation
106
107		template <class T>
108	16841	void TBitblaster<T>::initAtomBBStrategies()
109		{
110	5557530	for (int i = 0; i < kind::LAST_KIND; ++i)
111		{
112	5540689	d_atomBBStrategies[i] = UndefinedAtomBBStrategy<T>;
113		}
114		/// setting default bb strategies for atoms
115	16841	d_atomBBStrategies[kind::EQUAL] = DefaultEqBB<T>;
116	16841	d_atomBBStrategies[kind::BITVECTOR_ULT] = DefaultUltBB<T>;
117	16841	d_atomBBStrategies[kind::BITVECTOR_ULE] = DefaultUleBB<T>;
118	16841	d_atomBBStrategies[kind::BITVECTOR_UGT] = DefaultUgtBB<T>;
119	16841	d_atomBBStrategies[kind::BITVECTOR_UGE] = DefaultUgeBB<T>;
120	16841	d_atomBBStrategies[kind::BITVECTOR_SLT] = DefaultSltBB<T>;
121	16841	d_atomBBStrategies[kind::BITVECTOR_SLE] = DefaultSleBB<T>;
122	16841	d_atomBBStrategies[kind::BITVECTOR_SGT] = DefaultSgtBB<T>;
123	16841	d_atomBBStrategies[kind::BITVECTOR_SGE] = DefaultSgeBB<T>;
124	16841	}
125
126		template <class T>
127	16841	void TBitblaster<T>::initTermBBStrategies()
128		{
129	5557530	for (int i = 0; i < kind::LAST_KIND; ++i)
130		{
131	5540689	d_termBBStrategies[i] = DefaultVarBB<T>;
132		}
133		/// setting default bb strategies for terms:
134	16841	d_termBBStrategies[kind::CONST_BITVECTOR] = DefaultConstBB<T>;
135	16841	d_termBBStrategies[kind::BITVECTOR_NOT] = DefaultNotBB<T>;
136	16841	d_termBBStrategies[kind::BITVECTOR_CONCAT] = DefaultConcatBB<T>;
137	16841	d_termBBStrategies[kind::BITVECTOR_AND] = DefaultAndBB<T>;
138	16841	d_termBBStrategies[kind::BITVECTOR_OR] = DefaultOrBB<T>;
139	16841	d_termBBStrategies[kind::BITVECTOR_XOR] = DefaultXorBB<T>;
140	16841	d_termBBStrategies[kind::BITVECTOR_XNOR] = DefaultXnorBB<T>;
141	16841	d_termBBStrategies[kind::BITVECTOR_NAND] = DefaultNandBB<T>;
142	16841	d_termBBStrategies[kind::BITVECTOR_NOR] = DefaultNorBB<T>;
143	16841	d_termBBStrategies[kind::BITVECTOR_COMP] = DefaultCompBB<T>;
144	16841	d_termBBStrategies[kind::BITVECTOR_MULT] = DefaultMultBB<T>;
145	16841	d_termBBStrategies[kind::BITVECTOR_ADD] = DefaultAddBB<T>;
146	16841	d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>;
147	16841	d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>;
148	16841	d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB<T>;
149	16841	d_termBBStrategies[kind::BITVECTOR_UREM] = DefaultUremBB<T>;
150	16841	d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy<T>;
151	16841	d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy<T>;
152	16841	d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy<T>;
153	16841	d_termBBStrategies[kind::BITVECTOR_SHL] = DefaultShlBB<T>;
154	16841	d_termBBStrategies[kind::BITVECTOR_LSHR] = DefaultLshrBB<T>;
155	16841	d_termBBStrategies[kind::BITVECTOR_ASHR] = DefaultAshrBB<T>;
156	16841	d_termBBStrategies[kind::BITVECTOR_ULTBV] = DefaultUltbvBB<T>;
157	16841	d_termBBStrategies[kind::BITVECTOR_SLTBV] = DefaultSltbvBB<T>;
158	16841	d_termBBStrategies[kind::BITVECTOR_ITE] = DefaultIteBB<T>;
159	16841	d_termBBStrategies[kind::BITVECTOR_EXTRACT] = DefaultExtractBB<T>;
160	16841	d_termBBStrategies[kind::BITVECTOR_REPEAT] = DefaultRepeatBB<T>;
161	16841	d_termBBStrategies[kind::BITVECTOR_ZERO_EXTEND] = DefaultZeroExtendBB<T>;
162	16841	d_termBBStrategies[kind::BITVECTOR_SIGN_EXTEND] = DefaultSignExtendBB<T>;
163	16841	d_termBBStrategies[kind::BITVECTOR_ROTATE_RIGHT] = DefaultRotateRightBB<T>;
164	16841	d_termBBStrategies[kind::BITVECTOR_ROTATE_LEFT] = DefaultRotateLeftBB<T>;
165	16841	}
166
167		template <class T>
168	16841	TBitblaster<T>::TBitblaster()
169		: d_termCache(),
170		d_modelCache(),
171	16841	d_nullContext(new context::Context()),
172	33682	d_cnfStream()
173		{
174	16841	initAtomBBStrategies();
175	16841	initTermBBStrategies();
176	16841	}
177
178		template <class T>
179	606904	bool TBitblaster<T>::hasBBTerm(TNode node) const
180		{
181	606904	return d_termCache.find(node) != d_termCache.end();
182		}
183		template <class T>
184	242309	void TBitblaster<T>::getBBTerm(TNode node, Bits& bits) const
185		{
186	242309	Assert(hasBBTerm(node));
187	242309	bits = d_termCache.find(node)->second;
188	242309	}
189
190		template <class T>
191		void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits)
192		{
193		d_termCache.insert(std::make_pair(node, bits));
194		}
195
196		template <class T>
197		void TBitblaster<T>::invalidateModelCache()
198		{
199		d_modelCache.clear();
200		}
201
202		} // namespace bv
203		} // namespace theory
204		} // namespace cvc5
205
206		#endif /* CVC5__THEORY__BV__BITBLAST__BITBLASTER_H */