mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
update README
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e4338f085b
commit
f5b988aead
|
@ -1,2 +1,12 @@
|
|||
muZ: routines related to solving satisfiability of Horn clauses and
|
||||
solving Datalog programs.
|
||||
|
||||
- base - contains base routines and the main context for
|
||||
maintaining fixedpoint solvers
|
||||
- transforms - common rule transformations
|
||||
- rel - relational algebra based Datalog engine
|
||||
- pdr - PDR based Horn clause solver
|
||||
- clp - Dart/Symbolic execution-based solver
|
||||
- tab - Tabulation based solver
|
||||
- bmc - Bounded model checking based solver
|
||||
- fp - main exported routines
|
Loading…
Reference in a new issue