mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

take second suggestion from #2234

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-16 10:39:34 -07:00
parent c611fbeaee
commit 596acf26ce
1 changed files with 23 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/opt/opt_parse.cpp
View file

@ -687,14 +687,22 @@ private:
return peek(pos) == "<=" || peek(pos) == "=<";
}
bool peek_minus_infty(unsigned pos) {
bool peek_minus_infty_long(unsigned pos) {
return peek(pos) == "-" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
}
bool peek_plus_infty(unsigned pos) {
bool peek_minus_infty_short(unsigned pos) {
return peek(pos) == "-inf" || peek(pos) == "-infinity";
}
bool peek_plus_infty_long(unsigned pos) {
return peek(pos) == "+" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
}
bool peek_plus_infty_short(unsigned pos) {
return peek(pos) == "+inf" || peek(pos) == "+infinity";
}
void parse_indicator(symbol& var, rational& val) {
if (peek(1) == "=" && tok.peek_num(2) && peek(3) == "->") {
var = peek(0);
@ -731,14 +739,22 @@ private:
tok.next(3);
parse_upper(v);
}
else if (peek_minus_infty(0) && peek_le(2)) {
else if (peek_minus_infty_long(0) && peek_le(2)) {
v = peek(3);
tok.next(4);
parse_upper(v);
}
else if (peek_plus_infty(2) && peek_le(1)) {
else if (peek_minus_infty_short(0) && peek_le(1)) {
v = peek(2);
tok.next(3);
parse_upper(v);
}
else if (peek_plus_infty_long(2) && peek_le(1)) {
tok.next(4);
}
else if (peek_plus_infty_short(2) && peek_le(1)) {
tok.next(3);
}
else if (peek_le(1) && tok.peek_num(2)) {
v = peek(0);
tok.next(2);
@ -757,9 +773,11 @@ private:
update_upper(v, rhs);
tok.next(2);
}
else if (peek_le(0) && peek_plus_infty(1)) {
else if (peek_le(0) && peek_plus_infty_long(1)) {
tok.next(3);
}
else if (peek_le(0) && peek_plus_infty_short(1)) {
tok.next(2); }
}