mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
2011 commits 46 branches 52 tags 178 MiB
Commit graph

2011 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
717f131942 fix warnings and errors from the mint64 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-01 19:54:40 +01:00
Christoph M. Wintersteiger
7053b7636b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-05-01 14:11:21 +01:00
Christoph M. Wintersteiger
e50a9e8dbf MPF: fused-mul-add fixes. Sometimes this is still off by a bit. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-05-01 14:10:50 +01:00
Christoph M. Wintersteiger
65af658fd7 FPA: min/max special cases fixed. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-05-01 14:08:53 +01:00
Nikolaj Bjorner
7cb9e7381d fix build errors on ubuntu and gcc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-01 02:35:57 -07:00
Ken McMillan
e939dd2bc5 still integrating duality 2013-04-30 13:07:49 -07:00
Nikolaj Bjorner
5098089ee1 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-30 13:07:38 -07:00
Nikolaj Bjorner
b4d0216728 try to fix gcc build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-30 13:06:59 -07:00
Nikolaj Bjorner
351cea1439 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-30 11:53:56 -07:00
Nikolaj Bjorner
21b0a4fcbb testing utvpi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-30 11:53:10 -07:00
Nuno Lopes
f40df22ccc enable COI transformation in datalog mode 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-30 10:29:41 -07:00
Ken McMillan
feb5360999 integrating duality 2013-04-28 16:29:55 -07:00
Nikolaj Bjorner
fbe4af6336 add backward propagation transformation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-28 13:39:26 -07:00
Nikolaj Bjorner
be64e4b238 add special procedures for UTVPI and horn arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-28 13:37:03 -07:00
Nikolaj Bjorner
e6d6c55df0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-28 13:20:49 -07:00
Nikolaj Bjorner
4471d929f7 fix linking error in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-28 13:20:31 -07:00
Nikolaj Bjorner
160a448823 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-28 12:51:58 -07:00
Nikolaj Bjorner
3ac7cbe1c5 fix build breaker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-28 12:51:33 -07:00
Nikolaj Bjorner
8abdefef6d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-28 12:48:10 -07:00
Nikolaj Bjorner
9158fb17c1 add special procedures for UTVPI and horn arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-28 12:47:55 -07:00
Nikolaj Bjorner
3f45782814 tidy up clp_context a bit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-26 17:22:06 -07:00
Nikolaj Bjorner
80f2b70e78 fix header information 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-26 16:12:52 -07:00
Nikolaj Bjorner
d1938ce972 add simple bounded CLP backend 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-26 16:11:07 -07:00
Nikolaj Bjorner
65b52ba3e9 add simple bounded CLP backend 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-26 16:10:46 -07:00
Nikolaj Bjorner
8038c719fb optimize rule preprocessing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-26 14:40:20 -07:00
Nikolaj Bjorner
b644fb9875 optimize rule processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-26 12:02:19 -07:00
Nikolaj Bjorner
c58b4f9a53 optimize rule processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-26 11:43:06 -07:00
Nikolaj Bjorner
83add2bd9b fix bugs reported by Filip Konecny <filip.konecny@epfl.ch> in PDR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-25 13:39:11 -07:00
Nikolaj Bjorner
780ad7cc17 fix seg-fault caused by neglecting to inherit output predicate in slice 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-25 09:30:51 -07:00
Nikolaj Bjorner
4f9247a28a Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-24 20:04:01 -07:00
Nuno Lopes
f58e8e961d fix the build 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-23 14:59:19 -07:00
Nuno Lopes
9c230941cc [datalog] improve performance of smt2 frontend 
- delay calls to make_annotations and process_costs untill needed
 - remove debug exception handler in join()

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-23 12:01:50 -07:00
Nuno Lopes
1917c909d8 delete garbage 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-23 11:28:09 -07:00
Nuno Lopes
12b092c45f [datalog] restore the old (linear) cycle breaker 
force the compiler to use all preds as global deltas for correctness.  This is a temporary fix.

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-23 11:27:27 -07:00
Nuno Lopes
08eb85fe3d minor cleanup 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-23 10:02:44 -07:00
Nikolaj Bjorner
6250a29602 resolved conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-23 10:02:37 -07:00
Nikolaj Bjorner
a1277a57ae resolved conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-23 10:01:50 -07:00
Nikolaj Bjorner
d849dbf21f remove pointer comparisons/hash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-23 09:58:30 -07:00
Nikolaj Bjorner
eead1bbc48 missing else 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-23 09:24:39 -07:00
Nikolaj Bjorner
e1d5f484f1 simplify result from tactics, remove unused features from difference logic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-23 08:46:46 -07:00
Nuno Lopes
db653a6e68 [datalog] merge changes from the hassel branch 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-22 09:05:27 -07:00
Nikolaj Bjorner
4ceb228583 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-21 18:17:56 -07:00
Nikolaj Bjorner
0fbdd37e89 working on horn difference logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-21 18:17:49 -07:00
Nuno Lopes
7ce88d4da9 fix a few compilation warnings 
- remove unused variables and class fields
 - add support for gcc 4.5 & clang's __builtin_unreachable
 - fix 2 bugs related to strict aliasing
 - remove a few unused function parameters

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-21 14:36:39 -07:00
Nikolaj Bjorner
17f0377c06 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-20 21:20:20 -07:00
Ken McMillan
8488ca24d2 first commit of duality 2013-04-20 18:18:45 -07:00
Nuno Lopes
0673f645c9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-18 11:23:33 -07:00
Nuno Lopes
63ece8278d [datalog] improve compilation to reuse total tables, and to reduce cloning/deallocs. 
this gives up to 40% in memory reduction and 10% speedup in test cases with many rules

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-18 11:23:21 -07:00
Nikolaj Bjorner
2afcc493e0 remove reference count debugging, add substitution to C++ header 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-18 10:18:26 -07:00
Nikolaj Bjorner
c78a2f5d20 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-17 16:50:51 -07:00