Crest-Z3 does not allow for the unary minus operator about crest-z3 HOT 2 CLOSED

This error was caused as parser did not implement unary operatior parsing.

The following code solve the problem.

Thanks for reporting.

diff --git a/src/base/z3_solver.cc b/src/base/z3_solver.cc
index 0984129..845809c 100644
--- a/src/base/z3_solver.cc
+++ b/src/base/z3_solver.cc
@@ -510,8 +510,15 @@ static Z3_ast ParseStatement(Z3_context &ctx, map<var_t,Z3_ast>& vars, string& s
pos = *pos + (end - start);
string val = stmt.substr(start, end-start);
ret = Z3_mk_numeral(ctx, const_cast<char>(val.c_str()), ty);

• } else if (stmt[_pos] == '-' || stmt[_pos] == '+') {
• /* unary */
• Z3_sort ty = Z3_mk_int_sort(ctx);
• int start = *pos;
• int end = stmt.find(' ', start) + 1;
• *pos = *pos + (end - start);
• string val = stmt.substr(start, end-start);
• ret = Z3_mk_numeral(ctx, const_cast<char*>(val.c_str()), ty);
  }

DEBUG(fprintf(stderr, "AST: %s\n", Z3_ast_to_string(ctx, ret)));
return ret;
}

from crest-z3.

Thank you, Heechul.

On Mon, Apr 8, 2013 at 8:06 AM, heechul [email protected] wrote:

This error was caused as parser did not implement unary operatior parsing.

The following code solve the problem.

Thanks for reporting.

diff --git a/src/base/z3_solver.cc b/src/base/z3_solver.cc
index 0984129 https://github.com/heechul/crest-z3/commit/0984129..845809c
100644
--- a/src/base/z3_solver.cc
+++ b/src/base/z3_solver.cc
@@ -510,8 +510,15 @@ static Z3_ast ParseStatement(Z3_context &ctx, map&
vars, string& s
pos = *pos + (end - start);
string val = stmt.substr(start, end-start);
ret = Z3_mk_numeral(ctx, const_cast<char>(val.c_str()), ty);

• } else if (stmt[_pos] == '-' || stmt[_pos] == '+') {
• /* unary */
• Z3_sort ty = Z3_mk_int_sort(ctx);
• int start = *pos;
• int end = stmt.find(' ', start) + 1;
• *pos = *pos + (end - start);
• string val = stmt.substr(start, end-start);
• ret = Z3_mk_numeral(ctx, const_cast(val.c_str()), ty); } -
  DEBUG(fprintf(stderr, "AST: %s\n", Z3_ast_to_string(ctx, ret))); return
  ret; }

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/1#issuecomment-16046569
.

Mike

from crest-z3.