mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity
z3/src/muz
History
Alex Horn e576ca50bf Fix typo in documentation 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
2015-05-12 14:24:59 +01:00
..
base Fix typo in documentation 2015-05-12 13:18:51 +01:00
bmc move some configuration parameters into dl_context, add notes to udoc_relation 2014-09-26 08:22:25 -07:00
clp pull unstable 2015-04-01 14:57:11 -07:00
ddnf update ddnf experiment code 2015-05-11 17:11:21 -07:00
duality merge with unstable 2015-04-30 10:40:03 -07:00
fp pull unstable 2015-04-01 14:57:11 -07:00
pdr Codeplex issue 191: inconsistent results from PDR engine. The report exposed bugs in the implementation of the priority queue leaving unexplored leaves durin search. The priority queue has now been revised to address the exposed bugs 2015-04-01 16:27:15 -07:00
rel Fix typo in documentation 2015-05-12 14:24:59 +01:00
tab pull unstable 2015-04-01 14:57:11 -07:00
transforms pull unstable 2015-04-01 14:57:11 -07:00
README update README 2013-08-28 22:15:16 -07:00

README 

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