-
Notifications
You must be signed in to change notification settings - Fork 17
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Parsing error on unary clause #83
Comments
@tanjaschindler Can you check this? |
@rainoftime, The smt-lib standard defines left-assoc operators only for at least two arguments. This is on page 34 of the SMT-LIB language document. For n > 2, Some other solvers may accept this syntax, but it doesn't follow the standard. |
@jhoenicke Thanks for the explanation! Is it possible to support this?
|
we have a small wrapper function
|
Do you mean there is a wrapper as the level of Java API? |
As this is not allowed by the SMT-LIB standard, I would say that an SMT library that creates such output is buggy. If the library can create such terms it should internally fix them by converting unary or/and/+/..., before creating the text representation for SMT-LIB. Allowing these unary operators is problematic, as the question is for which operators we should allow this. Cleary unary "-" is a different operator. What about unary "/", unary "=>", which are also declared as :left-assoc or :right-assoc? I would like to strictly follow the SMT-LIB standard here. |
Hi, for the following formula,
smtinterpol commit 0610d35 issues a warning/error
The input satisfies the SMT-Lib2 standard. Unary clauses can also exist in real cases.
The text was updated successfully, but these errors were encountered: