mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
3746 commits 49 branches 53 tags 182 MiB
Commit graph

3746 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
f9d38a97df Bugfix for array simplifier 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-08 17:49:30 +00:00
Christoph M. Wintersteiger
d7a37f246c More bugfixes for smt setup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-08 16:59:46 +00:00
Christoph M. Wintersteiger
4792c5fb7c Fixed bugs in static features and smt setup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-08 16:53:08 +00:00
Christoph M. Wintersteiger
72345026be Revert "propagate_ineqs synchronization fix" 
This reverts commit 73cebc24c8.
 2015-02-08 15:16:24 +00:00
Christoph M. Wintersteiger
73cebc24c8 propagate_ineqs synchronization fix 2015-02-08 13:25:40 +00:00
Christoph M. Wintersteiger
a78dd680fb MPN synchronization fix 2015-02-08 13:25:18 +00:00
Nikolaj Bjorner
ded635cd06 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-02-08 10:25:44 +01:00
Nikolaj Bjorner
8141dadc89 break on small cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-02-08 10:22:06 +01:00
Christoph M. Wintersteiger
7e579604e1 Eliminated the old MS-Bignum interface because it stood in the way of progress. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-07 19:39:15 +00:00
Christoph M. Wintersteiger
da01f237fd fixed memory leaks 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-07 18:06:13 +00:00
Christoph M. Wintersteiger
778dd997d3 formatting (tabs) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-07 18:05:52 +00:00
Christoph M. Wintersteiger
359c7e4da9 Removed unnecessary variables and added initialization to others to silence warnings. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-07 14:47:26 +00:00
Christoph M. Wintersteiger
b96551a1a2 .NET/Java/ML: Moved toggle_warning_messages to Global, added en/disable_trace. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-07 14:17:39 +00:00
Christoph M. Wintersteiger
941d1063dd FPA rewriter and MPF bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-06 18:48:14 +00:00
Christoph M. Wintersteiger
5e60bcd920 FPA: fixes for the fpa_rewriter to enable model extraction and validation. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-06 16:53:31 +00:00
Christoph M. Wintersteiger
0db973ab4b undid previous fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-05 19:02:35 +00:00
Christoph M. Wintersteiger
de35801117 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-05 18:34:23 +00:00
Christoph M. Wintersteiger
088dc411ba fixed potential handle leak 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-05 18:32:36 +00:00
Nuno Lopes
bbefc54bf5 add implementation of UNREACHABLE for MSVC in release mode. 
This reduces code size of Z3 by 0.1%  \o/

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-05 09:53:26 +00:00
Nuno Lopes
9d5bc024e4 add implementation of UNREACHABLE for MSVC in release mode. 
This reduces code size of Z3 by 0.1%  \o/

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-05 09:51:05 +00:00
Christoph M. Wintersteiger
a4c599a435 typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-04 18:25:32 +00:00
Christoph M. Wintersteiger
3478cdb756 Added smt kernel setup for QF_FP(BV). Thanks to codeplex user smccamant for reporting this performance problem. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-03 12:30:42 +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
Christoph M. Wintersteiger
4bed5183f8 Made DRQ objects public in Java and .NET APIs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-30 21:58:43 -06:00
Christoph M. Wintersteiger
07c945718b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-01-30 21:10:32 -06:00
Christoph M. Wintersteiger
d7a62baef4 Improved memory use of the Java API. Thanks to Joerg Pfaehler for reporting this issue! 
+ formatting

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-30 21:10:22 -06:00
Christoph M. Wintersteiger
b8b57a8a26 Improved memory use of the Java API. 
+ formatting
 2015-01-30 21:05:14 -06:00
Christoph M. Wintersteiger
3b78509d0a Improved memory use of the .NET API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-30 20:45:16 -06: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
unknown
f020b7c7b8 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-01-28 17:54:26 -08:00
Christoph M. Wintersteiger
635fbee2bc Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-01-28 15:38:19 -06:00
Christoph M. Wintersteiger
bcfefdd8ee Bugfix for the FPA theory. Thanks to codeplex user smccamant for reporting this one. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-28 15:38:08 -06:00
Christoph M. Wintersteiger
2fa35233f7 Bugfix for the FPA theor. Thanks to codeplex user smccamant for reporting this one. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-28 13:17:22 -06: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
Christoph M. Wintersteiger
88530c8b90 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-01-26 22:19:16 +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
Nikolaj Bjorner
37fca65517 fuse join with projection avoiding double insert (but at cost of double projection) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-25 04:37:42 -08:00
Nikolaj Bjorner
761c7d9a40 adding annotation to logging to show number of columns and rows, adding dual propagation sketch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-25 04:01:18 -08:00
Christoph M. Wintersteiger
b6c40c6c0e Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-01-24 19:13:09 +00:00
Christoph M. Wintersteiger
e1d469fcbf Update release notes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 19:12:55 +00:00
Christoph M. Wintersteiger
b92bdaeebe ML API readme fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 18:51:47 +00:00
Christoph M. Wintersteiger
2f3ea1f39d removed legacy ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 18:48:51 +00:00
Christoph M. Wintersteiger
e29abefb12 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 
Conflicts:
	scripts/mk_util.py

+ Cosmetics

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 18:44:59 +00:00