sally/src/expr/term_ops.cpp at 4488f6ea1ac93f9801c4adecdaf873a60cf6ed98 · cgjohannsen/sally · GitHub

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
126
/**
 * This file is part of sally.
 * Copyright (C) 2015 SRI International.
 *
 * Sally is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Sally is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with sally.  If not, see <http://www.gnu.org/licenses/>.
 */

#include "expr/term_ops.h"

#include <iostream>
#include <cassert>

namespace sally {
namespace expr {

std::ostream& operator << (std::ostream& out, term_op op) {

#define SWITCH_TO_STRING(op) case op: out << #op; break;
  switch (op) {
    SWITCH_TO_STRING(TYPE_TYPE)
    SWITCH_TO_STRING(TYPE_BOOL)
    SWITCH_TO_STRING(TYPE_INTEGER)
    SWITCH_TO_STRING(TYPE_REAL)
    SWITCH_TO_STRING(TYPE_STRING)
    SWITCH_TO_STRING(TYPE_BITVECTOR)
    SWITCH_TO_STRING(TYPE_STRUCT)
    SWITCH_TO_STRING(TYPE_TUPLE)
    SWITCH_TO_STRING(TYPE_ENUM)
    SWITCH_TO_STRING(TYPE_RECORD)
    SWITCH_TO_STRING(TYPE_FUNCTION)
    SWITCH_TO_STRING(TYPE_ARRAY)
    SWITCH_TO_STRING(TYPE_PREDICATE_SUBTYPE)
    SWITCH_TO_STRING(VARIABLE)
    SWITCH_TO_STRING(TERM_EQ)
    SWITCH_TO_STRING(TERM_ITE)
    SWITCH_TO_STRING(CONST_BOOL)
    SWITCH_TO_STRING(TERM_AND)
    SWITCH_TO_STRING(TERM_OR)
    SWITCH_TO_STRING(TERM_NOT)
    SWITCH_TO_STRING(TERM_IMPLIES)
    SWITCH_TO_STRING(TERM_XOR)
    SWITCH_TO_STRING(CONST_RATIONAL)
    SWITCH_TO_STRING(TERM_ADD)
    SWITCH_TO_STRING(TERM_SUB)
    SWITCH_TO_STRING(TERM_MUL)
    SWITCH_TO_STRING(TERM_DIV)
    SWITCH_TO_STRING(TERM_MOD)
    SWITCH_TO_STRING(TERM_LEQ)
    SWITCH_TO_STRING(TERM_LT)
    SWITCH_TO_STRING(TERM_GEQ)
    SWITCH_TO_STRING(TERM_GT)
    SWITCH_TO_STRING(TERM_TO_INT)
    SWITCH_TO_STRING(TERM_TO_REAL)
    SWITCH_TO_STRING(TERM_IS_INT)
    SWITCH_TO_STRING(CONST_STRING)
    SWITCH_TO_STRING(CONST_BITVECTOR)
    SWITCH_TO_STRING(TERM_BV_ADD)
    SWITCH_TO_STRING(TERM_BV_SUB)
    SWITCH_TO_STRING(TERM_BV_MUL)
    SWITCH_TO_STRING(TERM_BV_UDIV)
    SWITCH_TO_STRING(TERM_BV_SDIV)
    SWITCH_TO_STRING(TERM_BV_UREM)
    SWITCH_TO_STRING(TERM_BV_SREM)
    SWITCH_TO_STRING(TERM_BV_SMOD)
    SWITCH_TO_STRING(TERM_BV_XOR)
    SWITCH_TO_STRING(TERM_BV_SHL)
    SWITCH_TO_STRING(TERM_BV_LSHR)
    SWITCH_TO_STRING(TERM_BV_ASHR)
    SWITCH_TO_STRING(TERM_BV_NOT)
    SWITCH_TO_STRING(TERM_BV_AND)
    SWITCH_TO_STRING(TERM_BV_OR)
    SWITCH_TO_STRING(TERM_BV_NAND)
    SWITCH_TO_STRING(TERM_BV_NOR)
    SWITCH_TO_STRING(TERM_BV_XNOR)
    SWITCH_TO_STRING(TERM_BV_CONCAT)
    SWITCH_TO_STRING(TERM_BV_EXTRACT)
    SWITCH_TO_STRING(TERM_BV_ULEQ)
    SWITCH_TO_STRING(TERM_BV_SLEQ)
    SWITCH_TO_STRING(TERM_BV_ULT)
    SWITCH_TO_STRING(TERM_BV_SLT)
    SWITCH_TO_STRING(TERM_BV_UGEQ)
    SWITCH_TO_STRING(TERM_BV_SGEQ)
    SWITCH_TO_STRING(TERM_BV_UGT)
    SWITCH_TO_STRING(TERM_BV_SGT)
    SWITCH_TO_STRING(TERM_BV_SGN_EXTEND)
    SWITCH_TO_STRING(TERM_BV_NEG)
    SWITCH_TO_STRING(TERM_BV_EXTEND)
    SWITCH_TO_STRING(TERM_BV_ROR)
    SWITCH_TO_STRING(TERM_BV_ROL)
    SWITCH_TO_STRING(TERM_ARRAY_READ)
    SWITCH_TO_STRING(TERM_ARRAY_WRITE)
    SWITCH_TO_STRING(TERM_ARRAY_LAMBDA)
    SWITCH_TO_STRING(TERM_TUPLE_CONSTRUCT)
    SWITCH_TO_STRING(TERM_TUPLE_READ)
    SWITCH_TO_STRING(TERM_TUPLE_WRITE)
    SWITCH_TO_STRING(TERM_RECORD_CONSTRUCT)
    SWITCH_TO_STRING(TERM_RECORD_READ)
    SWITCH_TO_STRING(TERM_RECORD_WRITE)
    SWITCH_TO_STRING(CONST_ENUM)
    SWITCH_TO_STRING(TERM_LAMBDA)
    SWITCH_TO_STRING(TERM_EXISTS)
    SWITCH_TO_STRING(TERM_FORALL)
    SWITCH_TO_STRING(TERM_FUN_APP);
    SWITCH_TO_STRING(OP_LAST)

  default:
    assert(false);
    out << "unknown" << (unsigned) op;
  }
#undef SWITCH_TO_STRING
  return out;
}

}
}