8000 unknown constant mkSBVTuple2 · Issue #589 · LeventErkok/sbv · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

unknown constant mkSBVTuple2 #589

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 accoun 8000 t related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
gregsgit opened this issue Aug 17, 2021 · 8 comments
Closed

unknown constant mkSBVTuple2 #589

gregsgit opened this issue Aug 17, 2021 · 8 comments
Labels
External issue

Comments

@gregsgit
Copy link

crash.log
Main.hs.txt

new to SBV. Using lots of tuples, including for example:

type    SRule           = STuple (Label, Label, Label, Label) (Maybe (Label, Label))

Z3 version 4.8.12 - 64 bit - build hashcode 3a402ca2c14c3891d24658318406f80ce59b719f

Any thoughts on a workaround?
Thanks.

***    Expected  : success
***    Received  : (error "line 163 column 46: unknown constant mkSBVTuple2 ((_ BitVec 16) (_ BitVec 16)) 
***                declared: (declare-fun mkSBVTuple2
***                             ((SBVTuple4 Label Label Label Label)
***                              (SBVMaybe (SBVTuple2 Label Label)))
***                             (SBVTuple2 (SBVTuple4 Label Label Label Label)
***                                        (SBVMaybe (SBVTuple2 Label Label)))) 
***                declared: (declare-fun mkSBVTuple2 (Label Label) (SBVTuple2 Label Label)) ")
***
***    Exit code : ExitFailure (-15)
***    Executable: /home/gregs/other-repos/z3/build/z3
***    Options   : -nw -in -smt2
@LeventErkok
Copy link
Owner
LeventErkok commented Aug 17, 2021 •
edited
Loading

Looks like z3 is not quite up to handling this usage. Try cvc4, like this:

myConfig = cvc4 { extraArgs = ["--strings-exp"] }

However, when I run it like that cvc4 gets going but does not terminate quickly. Quantifiers are usually a soft-spot for SMT solvers; if you can avoid them, that'd be the way to go.

@gregsgit
Copy link
Author
gregsgit commented Aug 17, 2021 via email

@LeventErkok
Copy link
Owner

@gregsgit

This seems to be an issue with z3 itself. I've reported it here: Z3Prover/z3#5486

LeventErkok added a commit that referenced this issue Aug 17, 2021
@LeventErkok
#589 Put extra annotations on constructors
0d5b1e5
@LeventErkok
Copy link
Owner

@gregsgit

Based on feedback from the z3 folks, I pushed this commit 0d5b1e5 which should handle the problem you're running into.

Give it a test and let me know if it gets you past the failure.

@gregsgit
Copy link
Author

That fix works; I get past the failure; thank you very much!

@gregsgit
Copy link
Author

Fixed

@LeventErkok
Copy link
Owner

Great! Thanks for the update.

@LeventErkok
Copy link
Owner

@gregsgit

A new release of SBV (v8.16) is now on package that contains this fix: https://hackage.haskell.org/package/sbv

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

No branches or pull requests
2 participants
@LeventErkok @gregsgit
0