1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 char_decl_plugin.cpp
7
8 Abstract:
9
10 char_plugin for unicode suppport
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2021-01-26
15
16
17 --*/
18 #include "util/gparams.h"
19 #include "ast/char_decl_plugin.h"
20 #include "ast/arith_decl_plugin.h"
21 #include "ast/ast_pp.h"
22
char_decl_plugin()23 char_decl_plugin::char_decl_plugin():
24 m_charc_sym("Char") {
25 }
26
~char_decl_plugin()27 char_decl_plugin::~char_decl_plugin() {
28 m_manager->dec_ref(m_char);
29 }
30
mk_func_decl(decl_kind k,unsigned num_parameters,parameter const * parameters,unsigned arity,sort * const * domain,sort * range)31 func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters,
32 unsigned arity, sort* const* domain, sort* range) {
33 ast_manager& m = *m_manager;
34 std::stringstream msg;
35 switch (k) {
36 case OP_CHAR_LE:
37 if (arity != 2)
38 msg << "incorrect number of arguments passed. Expected 2, received " << arity;
39 else if(domain[0] != m_char)
40 msg << "incorrect first argument type " << mk_pp(domain[0], *m_manager);
41 else if (domain[1] != m_char)
42 msg << "incorrect second argument type " << mk_pp(domain[1], *m_manager);
43 else
44 return m.mk_func_decl(symbol("char.<="), arity, domain, m.mk_bool_sort(), func_decl_info(m_family_id, k, 0, nullptr));
45 m.raise_exception(msg.str());
46
47 case OP_CHAR_CONST:
48 if (num_parameters != 1)
49 msg << "incorrect number of parameters passed. Expected 1, received " << num_parameters;
50 else if (arity != 0)
51 msg << "incorrect number of arguments passed. Expected 0, received " << arity;
52 else if (!parameters[0].is_int())
53 msg << "integer parameter expected";
54 else if (parameters[0].get_int() < 0)
55 msg << "non-negative parameter expected";
56 else if (parameters[0].get_int() > static_cast<int>(max_char()))
57 msg << "parameter expected within character range";
58 else
59 return m.mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, num_parameters, parameters));
60 m.raise_exception(msg.str());
61 case OP_CHAR_TO_INT:
62 if (num_parameters != 0)
63 msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters;
64 else if (arity != 1)
65 msg << "incorrect number of arguments passed. Expected one character, received " << arity;
66 else {
67 arith_util a(m);
68 return m.mk_func_decl(symbol("char.to_int"), arity, domain, a.mk_int(), func_decl_info(m_family_id, k, 0, nullptr));
69 }
70 m.raise_exception(msg.str());
71 case OP_CHAR_TO_BV:
72 if (num_parameters != 0)
73 msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters;
74 else if (arity != 1)
75 msg << "incorrect number of arguments passed. Expected one character, received " << arity;
76 else if (m_char != domain[0])
77 msg << "expected character sort argument";
78 else {
79 bv_util b(m);
80 unsigned sz = num_bits();
81 return m.mk_func_decl(symbol("char.to_bv"), arity, domain, b.mk_sort(sz), func_decl_info(m_family_id, k, 0, nullptr));
82 }
83 m.raise_exception(msg.str());
84 case OP_CHAR_FROM_BV: {
85 bv_util b(m);
86 if (num_parameters != 0)
87 msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters;
88 else if (arity != 1)
89 msg << "incorrect number of arguments passed. Expected one character, received " << arity;
90 else if (!b.is_bv_sort(domain[0]) || b.get_bv_size(domain[0]) != num_bits())
91 msg << "expected bit-vector sort argument with " << num_bits();
92 else {
93 return m.mk_func_decl(symbol("char.from_bv"), arity, domain, m_char, func_decl_info(m_family_id, k, 0, nullptr));
94 }
95 m.raise_exception(msg.str());
96 }
97 case OP_CHAR_IS_DIGIT:
98 if (num_parameters != 0)
99 msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters;
100 else if (arity != 1)
101 msg << "incorrect number of arguments passed. Expected one character, received " << arity;
102 else {
103 return m.mk_func_decl(symbol("char.is_digit"), arity, domain, m.mk_bool_sort(), func_decl_info(m_family_id, k, 0, nullptr));
104 }
105 m.raise_exception(msg.str());
106
107 default:
108 UNREACHABLE();
109 }
110 return nullptr;
111 }
112
set_manager(ast_manager * m,family_id id)113 void char_decl_plugin::set_manager(ast_manager * m, family_id id) {
114 decl_plugin::set_manager(m, id);
115 m_char = m->mk_sort(symbol("Unicode"), sort_info(m_family_id, CHAR_SORT, 0, nullptr));
116 m->inc_ref(m_char);
117 }
118
get_op_names(svector<builtin_name> & op_names,symbol const & logic)119 void char_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const& logic) {
120 op_names.push_back(builtin_name("char.<=", OP_CHAR_LE));
121 op_names.push_back(builtin_name("Char", OP_CHAR_CONST));
122 op_names.push_back(builtin_name("char.to_int", OP_CHAR_TO_INT));
123 op_names.push_back(builtin_name("char.is_digit", OP_CHAR_IS_DIGIT));
124 op_names.push_back(builtin_name("char.to_bv", OP_CHAR_TO_BV));
125 op_names.push_back(builtin_name("char.from_bv", OP_CHAR_FROM_BV));
126 }
127
get_sort_names(svector<builtin_name> & sort_names,symbol const & logic)128 void char_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const& logic) {
129 sort_names.push_back(builtin_name("Unicode", CHAR_SORT));
130 }
131
is_value(app * e) const132 bool char_decl_plugin::is_value(app* e) const {
133 return is_app_of(e, m_family_id, OP_CHAR_CONST);
134 }
135
is_unique_value(app * e) const136 bool char_decl_plugin::is_unique_value(app* e) const {
137 return is_value(e);
138 }
139
are_equal(app * a,app * b) const140 bool char_decl_plugin::are_equal(app* a, app* b) const {
141 return a == b;
142 }
143
are_distinct(app * a,app * b) const144 bool char_decl_plugin::are_distinct(app* a, app* b) const {
145 return
146 a != b &&
147 is_app_of(a, m_family_id, OP_CHAR_CONST) &&
148 is_app_of(b, m_family_id, OP_CHAR_CONST);
149 }
150
mk_char(unsigned u)151 app* char_decl_plugin::mk_char(unsigned u) {
152 SASSERT(u <= max_char());
153 parameter param(u);
154 func_decl* f = m_manager->mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, 1, ¶m));
155 return m_manager->mk_const(f);
156 }
157
get_some_value(sort * s)158 expr* char_decl_plugin::get_some_value(sort* s) {
159 return mk_char('A');
160 }
161
mk_le(expr * a,expr * b)162 app* char_decl_plugin::mk_le(expr* a, expr* b) {
163 expr_ref _ch1(a, *m_manager), _ch2(b, *m_manager);
164 unsigned v1 = 0, v2 = 0;
165 if (a == b)
166 return m_manager->mk_true();
167 bool c1 = is_const_char(a, v1);
168 bool c2 = is_const_char(b, v2);
169 if (c1 && c2)
170 return m_manager->mk_bool_val(v1 <= v2);
171 if (c1 && v1 == 0)
172 return m_manager->mk_true();
173 if (c2 && v2 == max_char())
174 return m_manager->mk_true();
175 expr* es[2] = { a, b };
176 return m_manager->mk_app(m_family_id, OP_CHAR_LE, 2, es);
177 }
178