Comments (5)
After consideration, adding definitions to the input problem won't solve the issue because this definition will probably involve quantifiers and Dolmen doesn't support model checking of quantified problems.
from dolmen.
Technically, adding support for these function is quite easy (in terms of code needed for typing and evaluation). However, the main problem I see are the following:
- how to enable use of these functions: it probably need to be behind a flag at least for the CLI, and we'd need to figure out a reasonable way to do that
- what happens if/when other projects use their own custom functions ? do we add all of these custom functions to
dolmen
and grow the list of CLI flags to accomodate all of the expansions ?
from dolmen.
Would it make sense to use dune-site's plugin mechanism for this?
Dolmen could expose a registry of builtins that plugins can register themselves into to provide the implementation of such functions. The easiest would be that the plugin also expose a name so that the builtins provided by, say, the "alt-ergo" plugin are enabled iff the command line --enable-builtins alt-ergo
(maybe also DOLMEN_ENABLE_BUILTINS
environment variable) is passed (and from the API there would something like BuiltinRegistry.get_builtins_for "alt-ergo"
).
This way, the custom functions do not live in Dolmen itself, but there could be separate packages such as dolmen-plugin-alt-ergo
(which could be maintained by Alt-Ergo rather than by Dolmen) that provides the approriate builtins and are picked up by Dolmen dynamically through dune-site.
from dolmen.
(sorry for the delay)
Using dune's plugin mechanism seems like a good fit for this. I won't have the time to work on that feature in the near (or medium) future, but if you're still interested, you're welcome to open a PR to add this, ^^
from dolmen.
I took a quick look. It is more complicated than I expected because we also need to be able to type the builtins, which I think the right way to do would be to register typing extensions, but typing extensions can only be registered after instantiated the Dolmen_loop.Typer.Make
functor has been instanciated, which is done by the binary, so the plugins would have to depend on the binary.
Alternatively, typing extensions could be moved out of the functor. This would mean that they are global rather than per-instantiation; I'd say that this is OK but will let you be the judge.
(One advantage of going global is that the extensions can be shared between multiple users of the functor; for instance for Alt-Ergo we could have a single plugin for Dolmen_loop
that would provide the Alt-Ergo builtins to both Alt-Ergo and Dolmen which would be a nice user experience as users would just need to have Alt-Ergo installed to have access to the Alt-Ergo builtins in Dolmen).
from dolmen.
Related Issues (20)
- 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
- Question regarding BV logic in SMT files HOT 14
- Support `bv2nat` as a "relaxed mode" HOT 2
- Attributes in nested quantifiers HOT 2
- RDL check is a bit too lenient HOT 1
- Can we get a formal 1.0 release please HOT 4
- Confusing error message with pattern matching on polymorphic type in ae's native language
- Support for `get-assignment` HOT 2
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.