forked from hoangmle/metaSMT
-
Notifications
You must be signed in to change notification settings - Fork 0
/
TODO
50 lines (43 loc) · 1.61 KB
/
TODO
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
= TODO List =
== features for metaSMT 4 (future release)==
* Type save
* Python Interface/bindings
* SMT-Lib 2
* Portfolio Solver (Any number of Solvers)
* Parallel/Distributed/Clustered solving [network]
* Typed Expression (automatic handling)
* extend documentation of available commands (SMT expressions, other)
== features for metaSMT 3 (next release)==
* CNF-Parser /Solver Frontend [done]
* extend documentation of available commands (SMT expressions, other)
* Portfolio Solver (2 Threads) [done]
* SMT-Lib 2 File output [done, for Z3 2.18]
* Typed Expression -> TypedSymbol [done]
* Explicit Features [partial]
* API declaration an checking [done]
== Future versions (maybe) ==
* Solver independent Syntax Trees
* SMT-LIB 1 Parser
* BitBlasting QF_BV to LIA (or other Logics)
* Pseudo Boolean SAT/Solvers
* Solver Checking (using a different Solver)
* Fuzzing
* eFMI ( easy Formal Methods Interface)
== Finished Features ==
* support for Boolector (QF_BV, Core Logic) [done]
* support for Z3 (QF_BV, Core Logic) [done]
* support for MiniSAT (Core Logic) [done]
* support for SWORD (QF_BV, Logic) [done]
* support for Picosat (Logic) [done]
* support for BitBlastig QF_BV to Logic [done]
* compile time Solver selection (same api, different solvers) [done]
* README for installation
* install scripts for Solvers (s.a.) [done]
* Example algorithm (Sudoku, Mastermind, etc) [done]
* Tool Paper [done]
* README/script to setup own projects [done]
* Cardinality Constraints [ done ]
* Constraint Groups [done]
* Constraint Stack [done]
* Array over Bitvector Theory [done]
* lazy expressions [done]