3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 17:29:21 +00:00
Commit graph

6 commits

Author SHA1 Message Date
Alex Horn
140fb7942d Add datalog infrastructure for min aggregation function
This patch adds an instruction to the datalog interpreter and
constructs a new AST node for min aggregation functions.

The compiler is currently still work in progress and depends on
changes made to the handling of simple joins and the preprocessor.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
2015-06-10 18:14:14 +01:00
Matthias Schlaipfer
bc94007207 Fixed non-deterministic behaviour in relation_map
Use of ptr_hash and subsequent iteration led to non-deterministic behaviour in Datalog engine.

Signed-off-by: Matthias Schlaipfer <t-matsch@microsoft.com>
2015-06-02 14:58:31 +01:00
Nikolaj Bjorner
16f80fce92 add check_relation for integrity checking of relational operations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-24 01:06:58 -07:00
Nikolaj Bjorner
9e7cef7d6b working on product sets
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-08-26 16:45:45 -07:00
Nikolaj Bjorner
716663b04a avoid creating full tables when negated variables are unitary, add lazy table infrastructure, fix coi_filter for relations, reduce dependencies on fixedpoing_parameters.hpp header file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-09-08 05:52:18 -07:00
Nikolaj Bjorner
c8f9535251 re-organize muz_qe into separate units
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-08-28 21:23:16 -07:00