blob: 4f761c8f762af4d28c6487f1c30a68246b0467a8 (
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
|
/********************* */
/*! \file expr_sequence.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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 Implementation of the sequence data type.
**/
#include "expr/expr_sequence.h"
#include "expr/expr.h"
#include "expr/node.h"
#include "expr/sequence.h"
#include "expr/type.h"
#include "expr/type_node.h"
namespace CVC4 {
ExprSequence::ExprSequence(const Type& t, const std::vector<Expr>& seq)
{
d_type.reset(new Type(t));
std::vector<Node> nseq;
for (const Expr& e : seq)
{
nseq.push_back(Node::fromExpr(e));
}
d_sequence.reset(new Sequence(TypeNode::fromType(t), nseq));
}
ExprSequence::~ExprSequence() {}
ExprSequence::ExprSequence(const ExprSequence& other)
: d_type(new Type(other.getType())),
d_sequence(new Sequence(other.getSequence()))
{
}
ExprSequence& ExprSequence::operator=(const ExprSequence& other)
{
(*d_type) = other.getType();
(*d_sequence) = other.getSequence();
return *this;
}
const Type& ExprSequence::getType() const { return *d_type; }
const Sequence& ExprSequence::getSequence() const { return *d_sequence; }
bool ExprSequence::operator==(const ExprSequence& es) const
{
return getType() == es.getType() && getSequence() == es.getSequence();
}
bool ExprSequence::operator!=(const ExprSequence& es) const
{
return !(*this == es);
}
bool ExprSequence::operator<(const ExprSequence& es) const
{
return (getType() < es.getType())
|| (getType() == es.getType() && getSequence() < es.getSequence());
}
bool ExprSequence::operator<=(const ExprSequence& es) const
{
return (getType() < es.getType())
|| (getType() == es.getType() && getSequence() <= es.getSequence());
}
bool ExprSequence::operator>(const ExprSequence& es) const
{
return !(*this <= es);
}
bool ExprSequence::operator>=(const ExprSequence& es) const
{
return !(*this < es);
}
std::ostream& operator<<(std::ostream& os, const ExprSequence& s)
{
return os << "__expr_sequence__(" << s.getType() << ", " << s.getSequence()
<< ")";
}
size_t ExprSequenceHashFunction::operator()(const ExprSequence& es) const
{
uint64_t hash = fnv1a::fnv1a_64(TypeHashFunction()(es.getType()));
return static_cast<size_t>(SequenceHashFunction()(es.getSequence()), hash);
}
} // namespace CVC4
|
