blob: 9674a66ced48b89ff6c571639e1243edfccc895e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
/********************* */
/*! \file word.h
** \verbatim
** Top contributors (to current version):
** Dejan Jovanovic
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
/*
* word.h
*
* Created on: Jul 13, 2012
* Author: dejan
*/
#ifndef WORD_H_
#define WORD_H_
#include <string>
#include <iostream>
#include <cvc4/cvc4.h>
namespace hashsmt {
class Word {
/** Expression managaer we're using for all word expressions */
static CVC4::ExprManager* s_manager;
protected:
/** The expression of this word */
CVC4::Expr d_expr;
/** Get the expression manager words are using */
static CVC4::ExprManager* em();
Word(CVC4::Expr expr = CVC4::Expr())
: d_expr(expr) {}
/** Extend the representing expression to the given size >= size() */
CVC4::Expr extendToSize(unsigned size) const;
public:
Word(unsigned size, unsigned value = 0);
Word(unsigned size, std::string name);
Word& operator = (const Word& b);
Word operator + (const Word& b) const;
Word& operator += (const Word& b);
Word operator ~ () const;
Word operator & (const Word& b) const;
Word operator | (const Word& b) const;
Word& operator |= (const Word& b);
Word operator ^ (const Word& b) const;
Word operator << (unsigned amount) const;
Word operator >> (unsigned amount) const;
unsigned size() const;
void print(std::ostream& out) const;
CVC4::Expr getExpr() const {
return d_expr;
}
/** Returns the comparison expression */
CVC4::Expr operator == (const Word& b) const;
/** Concatenate the given words */
static Word concat(const Word words[], unsigned size);
};
inline std::ostream& operator << (std::ostream& out, const Word& word) {
word.print(out);
return out;
}
/** Symbolic 32-bit unsigned integer as a CVC4 bitvector expression */
class cvc4_uint32 : public Word {
public:
/** Construction from constants of the right size */
cvc4_uint32(unsigned value = 0)
: Word(32, value) {}
/** Construction of variables of the right size */
cvc4_uint32(std::string name)
: Word(32, name) {}
/** Automatic extend/cut to uint32 */
cvc4_uint32(const Word& word);
};
/** Symbolic 8-bit unsigned char as a CVC4 bitvector expression */
class cvc4_uchar8 : public Word {
public:
/** Construction from constants of the right size */
cvc4_uchar8(unsigned value = 0)
: Word(8, value) {}
/** Construction of variables of the right size */
cvc4_uchar8(std::string name)
: Word(8, name) {}
/** Automatic extend/cut to uchar8 */
cvc4_uchar8(const Word& word);
};
}
#endif /* WORD_H_ */
|
