8000 Java - Quantifier.getBody() throws Cast Error · Issue #2460 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Java - Quantifier.getBody() throws Cast Error #2460

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.

Sign up for GitHub

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

Jump to bottom
Closed
schedutron opened this issue Aug 3, 2019 · 2 comments
Closed

Java - Quantifier.getBody() throws Cast Error #2460

schedutron opened this issue Aug 3, 2019 · 2 comments

Comments

@schedutron
Copy link
Contributor

I have a lambda expression q that is of class Quantifier and has the following string representation:

(lambda ((x!1 Int))
  (let ((a!1 (ite (= (ite (<= 2 x!1) 2 1) 2)
                  (STUDENT_TupleType
                    _ID__12345
                    _NAME__Bourikas
                    NULL_DEPT_NAME_1
                    31)
                  (STUDENT_TupleType
                    _ID__00128
                    _NAME__Bourikas
                    _DEPT_uNAME__Music
                    2))))
    (ite (= (ite (<= 2 x!1) 2 1) 1)
         (STUDENT_TupleType _ID__12345 _NAME__Bourikas NULL_DEPT_NAME_1 31)
         a!1)))

When I try to output q.getBody(), I get the following cast error:

Exception in thread "main" java.lang.ClassCastException: com.microsoft.z3.DatatypeExpr cannot be cast to com.microsoft.z3.BoolExpr
	at com.microsoft.z3.Quantifier.getBody(Quantifier.java:144)
	at main.Z3Project.parseTest(Z3Project.java:94)
	at main.Z3Project.main(Z3Project.java:267)
@schedutron
Copy link
Contributor Author

q.getBody() works correctly now, but if I want to cast the above quantifier to a lambda with the following:

Lambda lres = (Lambda) q.getBody();

I get back

java.lang.ClassCastException: com.microsoft.z3.DatatypeExpr cannot be cast to com.microsoft.z3.Lambda

@NikolajBjorner
6689
Copy link
Contributor

You would need to use an appropriate version of Context.mkLambda to create a lambda expression.
The body of your lambda/quantifier appears to have a Datatype sort. The sort of Lambdas is going to be an array, representing the function space from arguments to the value of the body.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@NikolajBjorner @schedutron
0