3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 09:56:39 +00:00
Commit graph

8 commits

Author SHA1 Message Date
Nikolaj Bjorner
4bbe1d4674 remove unused min-aggregate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-04 09:23:36 -08:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Alex Horn
8c097044e8 Add basic compiler support for min aggregation function
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
2015-06-11 16:23:26 +01:00
Nuno Lopes
b10f79a941 dl_compiler: minor simplifications
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-05-27 17:07:18 +01:00
Nuno Lopes
c0e0b39a1d Datalog: save memory in the compiler by using a union
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
2015-02-02 10:34:19 +00:00
Nuno Lopes
4be2f608f1 Datalog: make the compiler reuse registers in simple cases.
this also allows some code simplification

 dl_compiler.cpp |  133 +++++++++++++++++++-------------------------------------
 dl_compiler.h   |   16 +++---
 2 files changed, 54 insertions(+), 95 deletions(-)

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
2015-01-29 13:00:44 +00:00
Nikolaj Bjorner
c09903288f have free variable utility use a class for more efficient re-use
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-15 16:14:22 -07:00
Nikolaj Bjorner
0d56499e2d re-organize muz_qe into separate units
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-08-28 21:20:24 -07:00
Renamed from src/muz/dl_compiler.h (Browse further)