mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-25 08:54:35 +00:00
Code Activity
19129 commits 44 branches 52 tags 176 MiB
Commit graph

1080 commits

Author SHA1 Message Date
Alex Horn
132f984d51 Add syntactical min checker 
The purpose of this patch is to find out more about the "shape" of
the constraints in our benchmarks. In particular, we would like to
determine whether aggregation and negation, together, appear in
recursive rules.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 20:19:14 +01:00
Alex Horn
9b7c5658c8 Ignore min aggregation functions in compiler for now 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-10 20:06:09 +01:00
Nikolaj Bjorner
b08ccc7816 added missing Copyright forms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:54:02 -07:00
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
6f42cbd325 remove std-out 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-01 09:22:19 -07:00
Nikolaj Bjorner
ed7e0e11a8 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-28 20:55:13 -07:00
Nuno Lopes
b10f79a941 dl_compiler: minor simplifications 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-27 17:07:18 +01:00
Nikolaj Bjorner
f100d4feda hoist out basic union find 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-21 11:10:42 -07:00
Nikolaj Bjorner
28f6adf79e disable hybrid relations pending overhaul/deletion of product relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-20 09:21:55 -07:00
Christoph M. Wintersteiger
32fb679066 tabs 2015-05-19 11:01:15 +01:00
Nikolaj Bjorner
203c5015c8 fix debian amd64 warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-18 15:17:21 -07:00
Nuno Lopes
d8dc86f558 Merge branch 'unstable' of https://github.com/mschlaipfer/z3 into unstable 2015-05-18 16:38:19 +01:00
Nikolaj Bjorner
5632900f35 fix gcc compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-16 12:04:10 +01:00
Nikolaj Bjorner
64bd62b17e fix gcc compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-16 11:56:04 +01:00
Nuno Lopes
6c22edc988 fix assorted compiler warnings 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-16 11:44:58 +01:00
Matthias Schlaipfer
c82319b358 Refactor count_vars and count_rule_vars 
ast_manager m was not used
 2015-05-14 17:04:38 +01:00
Alex Horn
e576ca50bf Fix typo in documentation 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-05-12 14:24:59 +01:00
Alex Horn
efaba8eb40 Fix negation in documentation 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-05-12 14:22:32 +01:00
Alex Horn
0f78238b7e Fix typo in documentation 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-05-12 13:18:51 +01:00
Nuno Lopes
c2ef566ddc Merge pull request #81 from ahorn/opt 
Fix g++ compile-time error
 2015-05-12 10:44:28 +01:00
U-EUROPE\t-alexh
b882a94f6a Fix g++ compile-time error 
Signed-off-by: U-EUROPE\t-alexh <t-alexh@microsoft.com>
 2015-05-12 10:23:25 +01:00
Nikolaj Bjorner
c96c4c7af7 Merge branch 'opt' of https://github.com/Z3Prover/z3 into opt 2015-05-11 17:12:04 -07:00
Nikolaj Bjorner
bf6ab3fc03 local state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-11 17:11:52 -07:00
Nikolaj Bjorner
e53462c1c1 update ddnf experiment code 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-11 17:11:21 -07:00
Nikolaj Bjorner
839e3fbb7c add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-09 19:40:34 -07:00
Nikolaj Bjorner
9377779e58 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-30 10:40:03 -07:00
Nikolaj Bjorner
ffc3a36dcb checked ite-expressions as shared for bounds detection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-23 19:59:33 +02:00
Ken McMillan
af444beb2e re-indenting interp and duality 2015-04-15 12:22:50 -07:00
Nikolaj Bjorner
9978cba5a8 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 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 16:27:15 -07:00
Nikolaj Bjorner
52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Nikolaj Bjorner
9c55be14fb change print parameters to use hyphen instead of namespace dots 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 10:56:40 -07:00
Nikolaj Bjorner
10cdbb881f enable canceling simplex on interrupt, investigating PDR inconsistency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-25 12:13:57 -07:00
Christoph M. Wintersteiger
b76d588c28 Renamed the soft_timeout option to just timeout. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-21 16:10:30 +00:00
Nikolaj Bjorner
64e2011d42 fix crash in explanation generation. Codeplex issue 181 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-02-24 17:34:38 -08:00
Nikolaj Bjorner
dffb0ff844 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-02-24 17:04:01 -08:00
Nikolaj Bjorner
b8fbc32689 fix crash in explanation generation. Codeplex issue 181 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-02-24 17:03:34 -08:00
nikolajbjorner
fcb4962016 add patch suggested by Arie Gurfinkel 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
 2015-02-23 11:18:24 -08:00
Nuno Lopes
d3fb5f2a4c fix misc compiler warnings 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-15 11:53:24 +00:00
Nuno Lopes
0c4d82de58 datalog: optimize previous commit 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-02 11:49:58 +00:00
Nuno Lopes
5548ecc853 Datalog: fix bug with the following 2 scenarios: 
A(#x00) :- not B().
A() :- not B().

The first case can be further optimized, but committing this for correctness

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-02 11:29:49 +00:00
Nuno Lopes
2444440edc DoC: implement get_size_estimate_bytes() 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-02 11:28:57 +00: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
6017dcace3 datalog: fix compilation for rules like a(X) :- not b(X). 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-01-29 20:41:22 +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
Nuno Lopes
2e083ab9c2 DoC: specialize union for the case dst=empty and/or delta=empty 
this avoids O(n^2) insert and becomes O(n)

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-01-29 08:50:12 +00:00
Nuno Lopes
1701af9dc9 DoC: fix fast_empty() for tables without columns 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-01-28 11:38:26 +00:00
Nuno Lopes
9e447281ed Datalog: fix bug in compilation of negated queries that referenced vars not in the head. 
We will now first add unbounded columns for negation and for filtering
do filter_negation, and finally filter_interpret(_project)
 2015-01-27 14:21:34 +00:00
Nuno Lopes
83bae6c8aa DoC: fix bug filter_by_negation when negation table has 0 columns 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-01-27 13:42:14 +00:00
Nuno Lopes
6ab167f0c7 fix debug build 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-01-25 18:31:04 +00:00