mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity
6297 commits 24 branches 48 tags 158 MiB
Commit graph

418 commits

Author SHA1 Message Date
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
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
034e4f469e Fixed memory leak 2015-01-22 18:43:23 +00:00
Christoph M. Wintersteiger
95300e801d fixed build errors and warnings 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 18:24:36 +00:00
Christoph M. Wintersteiger
052baaabe4 FPA API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 14:22:35 +00:00
Christoph M. Wintersteiger
e0bc704106 FPA API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-11 18:29:12 +00:00
Christoph M. Wintersteiger
007ecb4ab2 MPF bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-04 14:37:33 +00:00
Christoph M. Wintersteiger
09814128a6 Update MPF toString 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-02 18:57:38 +00:00
Christoph M. Wintersteiger
09247d2e29 FPA theory and API overhaul 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 18:44:41 +00:00
Christoph M. Wintersteiger
97df505dba MPF consistency fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 15:23:27 +00:00
Christoph M. Wintersteiger
2258988b37 MPF bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-31 14:48:06 +00:00
Christoph M. Wintersteiger
defb6158fe MPF: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-29 17:09:28 +00:00
Christoph M. Wintersteiger
96c8bd7e91 MPF conversion bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-28 17:57:21 +00:00
Christoph M. Wintersteiger
6ebeebde50 Added parameter to display floating point numerals as reals 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-28 13:32:34 +00:00
Christoph M. Wintersteiger
b30e61e528 FPA: bugfixes, leakfixes, added fp.to_real 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-13 19:34:55 +00:00
Nikolaj Bjorner
08cb8b8de8 address divergence in the case of shared theory symbols. Codeplex issue 147, thanks to George Karpenkov 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-09 16:04:25 +01:00
Christoph M. Wintersteiger
7d196201dc fixed warnings 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 12:33:20 +01:00
Ken McMillan
d815af9f0f merge duality changes with unstable 2014-10-22 10:14:05 -07:00
Nikolaj Bjorner
0e83a2b1af merge with latest unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-22 09:45:04 -07:00
Nikolaj Bjorner
301f441801 bypass simplifier if (m_is_clausal) { 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-22 09:02:08 -07:00
Nikolaj Bjorner
1059d226e4 add default statement instead of incomplete cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 13:25:19 -07:00
Nikolaj Bjorner
d77d6c6648 update parameter checking for doubles, and fix error reporting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 13:24:31 -07:00
Nikolaj Bjorner
7f04529080 validate types of parameter values that get set globally 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-21 09:11:38 -07:00
Nikolaj Bjorner
7767a23626 improve error messages on incorrect parameter passing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-15 21:37:37 -07:00
Nikolaj Bjorner
9d75babcda add more information to error messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-15 21:33:29 -07:00
Nikolaj Bjorner
ce18421a7a fix box 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-15 14:29:39 -07:00
Nikolaj Bjorner
bcd2d935a9 enable modular parameters from the parser 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-09 10:18:46 -07:00
Nikolaj Bjorner
2362e01a9f add unit test for join-project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 17:17:14 -07:00
Nikolaj Bjorner
f0c63e56f3 make module parameter validation and adjustment more flexible: you can use both module qualifiers and unqualified parameters from the API at local scope 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 16:27:40 -07:00
Nikolaj Bjorner
8cf21dc242 fix tactic parameter checking to API, deal with compiler warnings in api_interp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 13:47:55 -07:00
Nikolaj Bjorner
adb9117a9e move parameter checking to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 13:32:25 -07:00
Nikolaj Bjorner
00555def4d improve error handling of parameters and remove work notes from udoc_relation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 11:05:38 -07:00
Nikolaj Bjorner
335f9a9be1 add parameter validation to tactic parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 10:55:24 -07:00
Nikolaj Bjorner
fdc1452ac6 undef max/min on apple to avoid warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-06 10:13:31 -07:00
Nikolaj Bjorner
83c6043741 undef max/min on apple to avoid warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-06 10:13:10 -07:00
Christoph M. Wintersteiger
a77694d9a8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-06 18:10:13 +01:00
Christoph M. Wintersteiger
3222ecd992 tabs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-06 18:09:40 +01:00
Christoph M. Wintersteiger
929880e4fd Fix for bogus runtime reports on Linux. Thanks to Vladimir Klebanov for reporting this one. 2014-10-06 18:06:36 +01:00
Nikolaj Bjorner
4e686693ee add declaration for w 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-06 08:39:48 -07:00
Nikolaj Bjorner
c6683fd6fa to fix that timeout of 0 has different interpretations across platforms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 12:27:57 -07:00
Nikolaj Bjorner
c706e91019 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 10:37:55 -07:00
Nikolaj Bjorner
6a3f75822d fix format bug (issue 126) and smaller nits in sat solver (const annotation, disable elimination of external or already elimianted variables) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-04 18:35:18 -07:00
Nikolaj Bjorner
fbb01f3699 prevent usage that mixes E/e notation with division / for numerals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 23:58:52 -07:00
Ken McMillan
4763532501 adding compile-time option to replace arrays with maps in smt (define SPARSE_MAP) 2014-09-30 11:25:47 -07:00
Nikolaj Bjorner
60d7872cc8 adding simple BCE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-29 18:00:34 -07:00
Nikolaj Bjorner
5dc2afa33f add bceq experiment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-29 10:59:22 -07:00
Nikolaj Bjorner
989569b154 add bceq experiment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-29 10:57:31 -07:00
Nuno Lopes
97a5e6d326 assorted compiler warnings fixes 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-28 12:21:56 +01:00