mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

fix #6446

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-08 18:37:16 -08:00
parent 4d86d73942
commit 9a656772b4
1 changed files with 35 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

51
src/muz/fp/datalog_parser.cpp
View file

@ -286,9 +286,8 @@ public:
dtoken read_num() { dtoken read_num() {
while(isdigit(m_curr_char)) { while (isdigit(m_curr_char))
save_and_next(); save_and_next();
}
return TK_NUM; return TK_NUM;
} }
@ -781,15 +780,29 @@ protected:
symbol td1(td); symbol td1(td);
expr_ref v1(m), v2(m); expr_ref v1(m), v2(m);
sort* s = nullptr; sort* s = nullptr;
dtoken tok2 = m_lexer->next_token(); uint64_t num1(0), num3(0);
if (tok2 != TK_NEQ && tok2 != TK_GT && tok2 != TK_LT && tok2 != TK_EQ) { if (tok1 == TK_NUM) {
return unexpected(tok2, "built-in infix operator"); char const* data = m_lexer->get_token_data();
rational num(data);
if (!num.is_uint64())
return unexpected(tok1, "integer expected");
num1 = num.get_uint64();
} }
dtoken tok2 = m_lexer->next_token();
if (tok2 != TK_NEQ && tok2 != TK_GT && tok2 != TK_LT && tok2 != TK_EQ)
return unexpected(tok2, "built-in infix operator");
dtoken tok3 = m_lexer->next_token(); dtoken tok3 = m_lexer->next_token();
td = m_lexer->get_token_data(); td = m_lexer->get_token_data();
if (tok3 != TK_STRING && tok3 != TK_NUM && !(tok3 == TK_ID && m_vars.contains(td))) { if (tok3 != TK_STRING && tok3 != TK_NUM && !(tok3 == TK_ID && m_vars.contains(td)))
return unexpected(tok3, "identifier"); return unexpected(tok3, "identifier");
if (tok3 == TK_NUM) {
char const* data = m_lexer->get_token_data();
rational num(data);
if (!num.is_uint64())
return unexpected(tok1, "integer expected");
num3 = num.get_uint64();
} }
symbol td2(td); symbol td2(td);
if (tok1 == TK_ID) { if (tok1 == TK_ID) {
@ -805,18 +818,21 @@ protected:
if (!v1 && !v2) { if (!v1 && !v2) {
return unexpected(tok3, "at least one argument should be a variable"); return unexpected(tok3, "at least one argument should be a variable");
} }
if (v1) { if (v1)
s = v1->get_sort(); s = v1->get_sort();
} else
else {
s = v2->get_sort(); s = v2->get_sort();
}
if (!v1) { if (tok1 == TK_NUM)
v1 = mk_symbol_const(num1, s);
if (tok3 == TK_NUM)
v2 = mk_symbol_const(num3, s);
if (!v1)
v1 = mk_const(td1, s); v1 = mk_const(td1, s);
} if (!v2)
if (!v2) {
v2 = mk_const(td2, s); v2 = mk_const(td2, s);
}
switch(tok2) { switch(tok2) {
case TK_EQ: case TK_EQ:
@ -1126,8 +1142,11 @@ protected:
if (m_arith.is_int(s)) if (m_arith.is_int(s))
return m_arith.mk_numeral(rational(el, rational::ui64()), s); return m_arith.mk_numeral(rational(el, rational::ui64()), s);
else if (m_decl_util.try_get_size(s, sz)) { else if (m_decl_util.try_get_size(s, sz)) {
if (el >= sz) if (el >= sz) {
throw default_exception("numeric value out of bounds of domain"); std::ostringstream ous;
ous << "numeric value " << el << " is out of bounds of domain size " << sz;
throw default_exception(ous.str());
}
return m_decl_util.mk_numeral(el, s); return m_decl_util.mk_numeral(el, s);
} }
else { else {