Comments (4)
Typing smtlib3 is going to be a non-trivial task indeed. I've already started to think about the changes that would be required to properly handle it. Currently the main points that will requires changes are:
- modules (this is not really that complex, rather it requires a bit of thinking about the design and import/open/lookup complexity tradeoffs in terms of performance): dolmen untyped ids already support module name/paths, but some native support will have to be added to the core typechecker to support modules import/open.
- overloading of user-defined operators: this is going to be annoying as it will most certainly require to support overloading in the core typechecker (rather than support it in the builtins as done currently), and I think it might require the typechecker to inspect (or rather unify) types in order to be able to resolve a name to the correct typed symbol, which I don't like because it basically breaks the abstraction between the typer and the expressions, :/
- qualified imports with restrictions to only some instances of polymorphic type constructors: as far as I can tell this is the real problem, and might require a lot to correctly work, depending on the exact specification of such import restrictions (e.g. what happens if functions imported by this module can produce some values of types not imported, would this have to be checked and rejected by the type-checker or would it be the user's responsibility to import a coherent subset of a module, what happens with imports from other modules which can produce values of not imported types, what happens if the same module is imported multiple times with different type instances allowed, etc...)
- upgrading the Expr module (and the core typechecker) to higher-order (this one should be fairly easy).
So quite a lot of non-trivial work. I'll try and work on that as soon as possible. Do you have any idea of the timeframe of the v3 release ?
from dolmen.
At least 1 year for a final version, I believe. I think you could express your difficulty on the SMTLIB mailing list if you think that some part are too complicated or not precise enough. For example overloading can be accepted only if an as
is provided (and it is now with the correct type of the function not only the result) or all the argument have a type without non-user type variable. Or overloading of polymorphic function can be completely forbidden: perhaps polymorphism or overloading not both, for defining the family of a particular function symbol!
At the end it is just a first public draft. Once available you should listen to @tinelli talk at SMTLIB: one important point is that it should not be a too big burden for solver implementor. So you can choose your own restrictions if you think they make sense and they help you to implement a possible/simpler v3, then we can propose them as amendment to the draft.
from dolmen.
I'll try and post something on the SMTLIB google group soon to raise my concerns (primarily about overloading + polymorphism as an infinite family of overloaded functions, which makes resolving a symbol non-local in my opinion).
from dolmen.
Dolmen now has support for higher-order typing, which is a first step towards supporting smtlibv3.
from dolmen.
Related Issues (20)
- Additional builtins in the State? HOT 1
- Wrong check-model
- Bitvectors of size 0 should be forbidden
- Ill-typed statement on Bitvector is accepted by Dolmen HOT 1
- Expose `with_cache`? HOT 1
- Support Alt-Ergo's `cut` and `check` HOT 12
- Add authors files
- Unclear error message during model checking HOT 7
- Spec errors on the difference logic benchmarks of the SMT-LIB HOT 2
- Reject names starting with `@` and `.` outside of models
- Handling of `set-option :global-declarations`
- Handling of named terms HOT 2
- Check sat assuming HOT 2
- DIMACS variables do not appear as decls HOT 1
- Uncaught exception on buggy file
- 4.08 support broken (`List.concat_map`) HOT 10
- Quoted identifiers can be keywords HOT 12
- Warning regarding the `dolmen_type` file HOT 2
- Support non-incremental parsing from stdin HOT 1
- Handling abstract values in `(get-value)` statements HOT 8
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 dolmen.