10000 Datatype constructors aren't visible · Issue #5486 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Datatype constructors aren't visible #5486

New issue

Have a question about this project? Sign up for a free Git 8000 Hub 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
LeventErkok opened this issue Aug 17, 2021 · 2 comments
Closed

Datatype constructors aren't visible #5486

LeventErkok opened this issue Aug 17, 2021 · 2 comments

Comments

@LeventErkok
Copy link

This script:

(set-logic ALL)

(declare-datatypes ((Pair 2)) ((par (X Y) ((pair (first X) (second Y))))))

; Uncomment the following line and it works!
; (define-fun x () (Pair Bool Bool) (pair true true))

(assert (= (first (pair true true))  true))

Causes z3 to say:

(error "line 8 column 33: unknown constant pair (Bool Bool) ")

Interestingly, if you uncomment the 6th line with define-fun, it goes through without any complaint.
@LeventErkok LeventErkok mentioned this issue Aug 17, 2021
Closed
@NikolajBjorner
Copy link
Contributor

Type resolution by the parser is rudimentary: it searches through existing types to resolve for pair. It does not deduce the type of pair based on arguments (even if this is "just" a matter of matching). By default expect to have to type annotate. Luckily, SMTLIB2 has the facilities:

(assert (= (first ((as pair (Pair Bool Bool)) true true))  true))

@LeventErkok
Copy link
Author

Thanks @NikolajBjorner I get tripped on this on a regular basis and always forget to annotate.

NikolajBjorner added a commit that referenced this issue Aug 17, 2021
@NikolajBjorner
#5486 - improve type elaboration by epsilon to make common cases pars…
5c9f4dc 
…e without type annotation
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
@LeventErkok @NikolajBjorner
0