formulog
formulog copied to clipboard
HarvardPL
Datalog with support for SMT queries and first-order functional programming
Using `is_sat` in the body of a rule doesn't use any framing, so even if the solver has discharged the sat determination, it remains in memory within the solver and...
We could use a nice introduction to the language. Optimally, it would build up to an interesting example Formulog program (such as a symbolic evaluator for a simple input language).
We should support character literals like `'a'`. At a minimum, we could restrict support to the front end, where they could be converted to `i32`s.
We support different ways of interacting with the back-end SMT solver(s). These include strategies that reset the solver state between queries, as well as different approaches to caching queries to...
The Formulog-to-Souffle transpiler generates invalid query plans in the presence of the `CODEGEN_PROJECT` relation, which it seems to treat as being in the same stratum as the predicate being defined....
I'd like to create user-defined types to represent IP addresses. Specifically, a `bv[32]` to represent an IPv4 address and a `bv[128]` to represent an IPv6 address. Since `i32` is interchangeable...
Right now, the Formulog version is hard-coded into the CLI, which is easy to forget to update (see #25). Instead, the version should be stored in the JAR (and maybe...
Right now, Formulog is parameterized by a mix of system properties (like `-DdebugSmt`) and proper flags (like `--dump-idb`). For the sake of consistency and usability, we should convert user-relevant system...
As a convenience, allows users to specify options in a configuration file, instead of requiring them to list the options on the command line.