Robin Freyler
Robin Freyler
No ideas so far but would be a nice generalization.
Stevia requires support for SMTLib2 parsing to make it work with SMTLib2 inputs. ## Implementation Status - Raw Lexer: **done** - Simple Lexer: **done** - Parser: **in progress** - SMTLib...
Stevia could profit greatly from fuzz testing. This could be more or less easily implemented at least for SMTLib2 parsing once implemented and for the word-level simplifier. Maybe later even...
Stevia could profit by implementing or at least providing `Nand`, `Nor` and `Xnor` in addition to `And`, `Or` and `Xor` that currently exist. This could make some simplifications involving negation...
The current Read-over-Write simplification might expand its input exponentially. This could impose significant performance penalties and should be avoided. By the newly introduced `SymbolProxy` in `Context` proxy symbols can be...
Stevia should handle complex array expressions and thus be able to word-level simplify those together with array abstraction refinement. To be implemented are: 1. Array-Read-Elimination: Eliminates `ArrayRead` expressions by replacing...
For stevia to be a more or less complete SMT solver the following high-level modules will need to be implemented in one form or another: - [x] **AST:** Data structures...
Find out what scopes `push` & `pop` in STP are and how to incorporate them into this SMT solver. **Note:** STP has a stack of vectors that acts as assertion...
Find and depend on decent library implementation similar or equal to STP's [ABC library](https://people.eecs.berkeley.edu/~alanmi/abc/abc.htm) for [and-inverter-graph](https://en.wikipedia.org/wiki/And-inverter_graph) (AIG) computation. A pure Rust implementation is favoured over any other implementation to avoid...
Currently the `stevia_ast` module interface is extremely polluted because every item is exported on global scope. Only the actual `expression` items have their own module. We could need further modules...