Comments (4)
OK, interesting. Have you tried reporting this to Z3's people? Citing the documentation:
The error handler is invoked if a model is not available because the commands above were not invoked for the given solver, or if the result was Z3_L_FALSE.
Requesting a model when Z3_solver_check
returns Z3_L_UNDEF
is not supposed to give you a segfault, as far as I can tell.
Nowadays I'm a bit disconnected with the SMT-world but as far as I remember one could get a model from an undefined result. Perhaps requires to set an option or something.
from haskell-z3.
We have a workaround in our fork for now, but we're planning on writing new, type-safe bindings for smt; will let you know once we figure it out and maybe our changes can be useful to you!
from haskell-z3.
Sure, please submit a pull request if you have a proposal to fix it. I would very much appreciate it. In this case the correct fix IMO is to make solverGetModel
in Z3.Base
to check for errors. I guess there are Undef cases were you have no model available.
Regarding the type-safe bindings. I would be very happy to see a type-safe alternative. It depends how much type-safe you want to be. We tried that in earlier versions, it was called Z3.Lang
, and ended up removing it. It is easy when you restrict yourself to a subset of SMT theories. It gets tricky and kind of hacky to handle functions and other stuff. Most people using these bindings are building tools, and for that use case too much type-safety can actually be cumbersome to work with. I believe that SBV's author ended up adding an unsafe Dynamic
module for that reason.
Then I had plans to make the bindings "safer" even if not type/statically-safe. But I no longer have enough spare time for that!
from haskell-z3.
Sounds goo, thanks!
from haskell-z3.
Related Issues (20)
- Crash on parseSMTLib2String HOT 8
- Problem installing on OSX HOT 1
- Nondeterministic segfaults from z3 HOT 14
- Empty model with Z3 >=4.8 HOT 4
- segfault on evalBv HOT 1
- Cannot build with Z3 4.8.5 HOT 6
- MonadFail and GHC 8.6+ HOT 1
- MonadZ3 for ReaderT HOT 1
- error dyld Library not loaded: libz3.dylib HOT 2
- Possibility of an interface with better ergonomics? HOT 6
- Inconsistent integer argument handling HOT 1
- Program hangs when running evalZ3 or evalZ3WithEnv more than once HOT 4
- Publish new version with new combinators (mkPower missing) HOT 4
- Reference URL's in haddock documentation seem to be broken.
- Reference URL's in haddock documentation seem to be broken
- Support for parametric datatypes HOT 1
- "Unexpected code was reached." when parsing HOT 2
- Installation on Windows 10
- Unable to install on M1/M2 Mac HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from haskell-z3.