mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Code Activity
19591 commits 23 branches 48 tags 157 MiB
Commit graph

1799 commits

Author SHA1 Message Date
Nikolaj Bjorner 2912c355e2 remove reinterpret_cast. Issue #229, issue #24 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-04 10:54:19 -07:00
Christoph M. Wintersteiger f11502e0ac reinterpret_cast fixes for the Windows compiler. 2015-10-04 16:41:28 +01:00
Christoph M. Wintersteiger 4626196907 Eliminated reinterpret_casts. Partially fixes #24, #229. 2015-10-04 15:52:20 +01:00
Nikolaj Bjorner 50993582ec put break statement in else branh. Issue #230 (broken loop) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:15:54 -07:00
Nikolaj Bjorner 89f1541d83 put break statement in else branh. Issue #230 (broken loop) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:15:45 -07:00
Nikolaj Bjorner d9b6623400 include rlimit in nlsat, include dedicated error message, for issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 09:16:46 -07:00
Nikolaj Bjorner 1f9d5249a3 fix build break regarind z3test.py and added rlimit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 14:05:57 -07:00
Nikolaj Bjorner f3b8fe130a adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities. This is to address issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:40:54 -07:00
Nikolaj Bjorner 9b3e242990 adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:37:59 -07:00
Christoph M. Wintersteiger 04266fccc9 Bugfix for mpf sqrt. 
Fixes #222.
 2015-09-21 20:56:07 +01:00
Christoph M. Wintersteiger 0b15fc9402 Bugfix for mpf sqrt. 
Fixes #222.
 2015-09-21 19:44:53 +01:00
Christoph M. Wintersteiger f3441c6a9b tabs and indentation 2015-09-17 13:25:22 +01:00
Christoph M. Wintersteiger e9565d6a7f Fixed warning message 2015-09-17 12:18:44 +01:00
Christoph M. Wintersteiger 2115ea8bb8 Bugfix for fp.sqrt. 
Fixes #220.
 2015-09-17 12:13:04 +01:00
Christoph M. Wintersteiger 79d69cd5f0 Added FP to_ieee_bv to fpa_rewriter to enable model evaluation. 2015-09-16 12:57:05 +01:00
Christoph M. Wintersteiger d6e2fa6a60 Bugfix for MPF fma. 2015-09-14 14:07:11 +01:00
Christoph M. Wintersteiger 25f75b60fe Bugfix for fp.mul and fp.fma for small numbers of e/s bits. 
Fixes #215.
 2015-09-10 11:37:06 +01:00
Nikolaj Bjorner 4be3926daa use signed character type declarations for cross platform compilation. Fixes issue #210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-05 16:30:58 -07:00
Nikolaj Bjorner b4d0e6076e change behavior on allocation excess to process exit to avoid memory smashes on exception unsafe code blocks. Fixes issue #175 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-02 16:12:19 -07:00
Nuno Lopes f62a192357 remove __in/__out SAL annotations. 
They break the build with recent glibc versions and apparently noone is using them.

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-07-15 13:46:32 +01:00
Nikolaj Bjorner 4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Nikolaj Bjorner 940fed16e1 enforce stringstream formatting to avoid default format routine. fixes issue #149 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-06 09:11:52 -07:00
Nuno Lopes eeef4d29d6 remove the optimization for 0-byte allocations 
I wasn't able to trigger with any SMT or API benchmark
Removing it ensures the function never returns null and enables further optimizations.
I get an amazing avg speedup of 0.9%

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-07-01 14:38:33 +01:00
Nikolaj Bjorner 1544105bd5 set undo trail after set-watches to avoid crash during exception handling (the relevancy trail is scoped so ends up traversing the trail if allocating the watch throws an exception). Fixes crash.smt in issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:20 +01:00
Nikolaj Bjorner 158a5dd2db add count of memory allocations and way to limit allocations globally. Fix purification in nlsat_smt to fix regressions on QF_UFNRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:12 +01:00
Christoph M. Wintersteiger 9a62d989e6 Revert "Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable" 
This reverts commit d3db21ccde, reversing
changes made to e463d5d899.
 2015-06-24 17:06:04 +01:00
Christoph M. Wintersteiger 3a49223076 Merge branch 'unstable' of https://github.com/wintersteiger/z3 into unstable 2015-06-14 19:00:09 -07:00
Christoph M. Wintersteiger 0caf3bd18c Bugfix for mpf.is_regular 2015-06-14 18:59:46 -07:00
Nikolaj Bjorner b08ccc7816 added missing Copyright forms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:54:02 -07:00
Nuno Lopes 6217804ed5 fix another UB in bit_vector 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-07 12:07:24 +01:00
Christoph M. Wintersteiger 49a4df0de1 MPF min/max -+0.0 special cases changed to +0.0 instead of second argument. 
Another piece of fix #68
 2015-05-28 12:54:57 +01:00
Christoph M. Wintersteiger f1cc1842e1 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-23 13:25:00 +01:00
Christoph M. Wintersteiger 98f33c3f8b Bug/build fix for hwf::fma 2015-05-23 13:10:07 +01:00
Nuno Lopes 08b5635327 fix unaligned load in hash_string() 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-23 12:13:39 +01:00
Christoph M. Wintersteiger d5c39798ea Bugfix for hwf 2015-05-23 12:02:53 +01:00
Nuno Lopes c577ab361b fix assorted undefined behaviors caught by clang 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-23 11:45:12 +01:00
Christoph M. Wintersteiger 6f6cd61817 Bugfix for float-to-float conversion. 
Fixes #77
 2015-05-22 20:30:12 +01:00
Christoph M. Wintersteiger 891073d3fe typo 2015-05-22 12:01:10 +01:00
Christoph M. Wintersteiger ffbbf08d20 Fixed warning message about unused lock when OpenMP is not available. 2015-05-22 11:59:31 +01:00
Christoph M. Wintersteiger 54cde7cabb Bugfix for hwf::round_to_integral 2015-05-22 11:39:58 +01:00
Christoph M. Wintersteiger 759d9f2dda bugfix for hwf::fma 2015-05-22 11:39:28 +01:00
Christoph M. Wintersteiger 705ace6f0a Naming consistency 2015-05-22 11:39:08 +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
Christoph M. Wintersteiger 8c18bdcca9 Bugfix for fp.roundToIntegral. 
Fixes #69
 2015-05-21 18:12:14 +01:00
Christoph M. Wintersteiger c422b48bf4 Bugfix for hwf_manager::round_to_integral 2015-05-21 15:06:47 +01:00
Christoph M. Wintersteiger 51040d3e19 Bugfix for fp.isNormal 2015-05-20 18:32:40 +01:00
Henning Günther 33ddf0bcdf Expose insert_if_not_there_core method in map class 
Signed-off-by: Henning Günther <t-hennig@microsoft.com>
 2015-05-20 14:33:46 +01:00
Nuno Lopes 66e6e67395 fix build on CentOS 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-19 16:52:47 +01:00
Christoph M. Wintersteiger 32fb679066 tabs 2015-05-19 11:01:15 +01:00
Christoph M. Wintersteiger 25f37c8a0c Resolved mpf merge conflicts. 2015-05-19 11:00:34 +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
Nikolaj Bjorner e6b8af402f fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-15 15:56:21 +01:00
Nikolaj Bjorner ab5022888c Merge branch 'opt' of https://github.com/Z3Prover/z3 into unstable 2015-05-14 12:11:17 +01:00
Christoph M. Wintersteiger a6bb7d2d0f Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-12 10:24:31 +01:00
Nuno Lopes 379ce66391 fix a few undefined behaviors exposed by the unit tests 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-11 06:30:24 +01:00
Nuno Lopes 091ae37c06 Fix bug in my previous patch in bit_vector::operator=() 
Signed-off-by: Nuno Lopes <nuno@linux.Home>
 2015-05-11 04:44:11 +01:00
Nuno Lopes 6645358fed fix issue #57: undefined behavior in bit_vector.h 2015-05-10 22:30:07 +00:00
Christoph M. Wintersteiger 31e78cd178 Bugfix for fp.rem(0, 0). 
Fixes #70.
 2015-05-08 22:49:14 +01:00
Christoph M. Wintersteiger a63481de85 New implementations of fp.roundToIntegral in mpf and fpa2bv. 
Partially fixes #69
 2015-05-06 19:19:03 +01:00
Christoph M. Wintersteiger 53b479e1c3 Bugfix for fp.rem(0, 0). 
Fixes #70.
 2015-05-06 12:24:18 +01:00
Christoph M. Wintersteiger 73eb7cbf5c Bugfix for mpf roundToIntegral. 
Partially fixes #69
 2015-05-05 23:53:33 +01:00
Nikolaj Bjorner 9377779e58 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-30 10:40:03 -07:00
Christoph M. Wintersteiger b58d3f4335 Bugfix for MPF unpacking 2015-04-25 14:26:18 +01:00
Daniel J. Hofmann 6150083276 Wignored-qualifiers 2015-04-03 19:24:35 +02:00
Nikolaj Bjorner 52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Christoph M. Wintersteiger 99ea0a8c19 Bugfix for mpf is_normal. 
Fixes #17
 2015-03-30 08:02:57 +01:00
Christoph M. Wintersteiger 690eb8eaca Bugfix for fp.isSubnormal. 
Fixes #10
 2015-03-29 13:31:44 +01:00
Nuno Lopes 4ed062d54a fix missing memset in my previous commit 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-03-11 11:04:33 +00:00
Nuno Lopes 44e647e72b add reallocate() function and use it in bit_vector and vector containers 
give a speedup of 1-4%

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-03-10 16:53:47 +00:00
Nuno Lopes e64760abbd fix the build with VS 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-03-02 09:18:15 +00:00
Nikolaj Bjorner 8bcd6edd08 temporary build fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-01 15:19:57 -08:00
Nuno Lopes 8029e31ddd add compiler attributes to allocation functions 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-28 17:31:50 +00:00
Nuno Lopes 5676fbbc9e compiler love: make a few symbols static and avoid unneeded relocations 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-22 11:13:51 +00:00
Christoph M. Wintersteiger 83a90a9133 Fixed infinite loop when nightly tests crash while std::cin is attached to /dev/null 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-09 15:26:25 +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 778dd997d3 formatting (tabs) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-07 18:05:52 +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
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
Nuno Lopes 5f59dd1644 revert usage of popcnt is MSVC 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-28 11:37:11 +01:00
Nikolaj Bjorner e6725b2344 merge unstable into opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 12:12:24 -07:00
Nikolaj Bjorner 1111c0494f adding validation code to doc/udoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-23 17:10:00 -07:00
Nikolaj Bjorner 54506408f9 fix overflow bugs in doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 22:03:59 -07:00
Nikolaj Bjorner b57353eff2 fix bounds bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 18:06:18 -07:00
Nikolaj Bjorner 83e7107485 fix bugs in doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 17:45:01 -07:00
Nikolaj Bjorner 22808a039d working on udoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-21 20:25:11 -07:00
Nuno Lopes b243ac945f hoprfully fix the build for MSVC 2010 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-21 15:20:43 +01:00
Nikolaj Bjorner a50cbef877 testing doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-20 19:01:15 -07:00
Nuno Lopes d36cecc2f3 make use of count population intrinsincs on MSVC/gcc/clang 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-19 15:51:08 +01:00
Nuno Lopes 61d67dc2de fix a few compiler warnings 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-18 14:38:40 +01:00
Nikolaj Bjorner 4e4346576a move to managed tbvs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-15 22:01:13 -07:00
Nikolaj Bjorner d9dafe7b94 tbv utilities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-15 21:23:03 -07:00
Nikolaj Bjorner cd12fa8461 adding fixed size bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-15 20:00:45 -07:00
Nikolaj Bjorner 770d0d58fe bug fixes to sorting network 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-11 21:53:12 -07:00
Nikolaj Bjorner 019ff77613 fix sorting network bug, add network compilation,... 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-11 18:47:21 -07:00
Christoph M. Wintersteiger 23af977d68 Multi-threading bugfix, DLL could be used from other threads before the main thread initializes it. 
Thanks to user xor88 for reporting this one.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-09-03 17:49:10 +01:00
Nikolaj Bjorner 83a7d1a658 adding options to maxres for experiments, include option to pretty print module parameters in smt2 style 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-30 11:46:29 -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 20728535e8 remove extra qualifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-25 13:12:49 -07:00
Nikolaj Bjorner 34aa06b5a3 more ddnf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-21 21:57:44 -07:00
Nikolaj Bjorner b596828d23 add DDNF based engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-21 18:04:46 -07:00
Ken McMillan c007a5e5bd merged with unstable 2014-08-06 11:16:06 -07:00
Nikolaj Bjorner 960e8ea1d5 working on hitting sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-08 14:12:54 +01:00
Nikolaj Bjorner 05a39cb2cf fix wrong simplex backtracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-09 08:51:07 -07:00
Christoph M. Wintersteiger 581bbb58fb typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-02 18:04:32 +01:00
Christoph M. Wintersteiger 8150bd5617 OSX timeout handling bugfix 2014-05-02 17:58:17 +01:00
Nikolaj Bjorner 1db7e0a149 fix compiler warnings reported by Robert White 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-02 15:54:28 +02:00
Christoph M. Wintersteiger 3ab1766588 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt 2014-03-27 13:13:10 +00:00
Nikolaj Bjorner ede9549818 fix compilation errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-25 13:43:45 -07:00
Nikolaj Bjorner ea261c930d fix memory leak in scoped_numeral_vector 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-22 20:34:34 -07:00
Christoph M. Wintersteiger d1376343c7 Compilation fix. 
gcc 4.3.2 (on debian 5) did not like the definitions of gcd and abs in class rational, so I moved them outside of the class.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-22 16:42:11 +00:00
Nikolaj Bjorner f8348d0bc4 trying to fix build problems 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-21 14:45:12 -07:00
Nikolaj Bjorner 80ba830091 working on DL opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-05 15:43:15 -08:00
Nikolaj Bjorner 478b3160ac optimize theory pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-02-25 18:06:54 -08:00
Nikolaj Bjorner aff92f3ac1 Merge branch 'unstable' of https://git01.codeplex.com/z3 into opt 2014-01-27 11:19:19 -08:00
Nikolaj Bjorner c14c65465a working on stand-alone simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-26 19:46:42 -08:00
Christoph M. Wintersteiger 0e74362ecb Added support for the final draft of the FPA standard (and fpa2bv conversion). 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-01-24 15:36:23 +00:00
Christoph M. Wintersteiger 73a1dddc45 Bugfixes for the build on new OSX machines (XCode 5.0 on). 2014-01-21 17:06:13 +00:00
Nikolaj Bjorner 26a3d2ca31 add stand-alone simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-21 08:40:28 -08:00
Nikolaj Bjorner ff54b3d92b fix memory leak for scoped_numeral over trail objects 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-15 17:00:07 -08:00
Nikolaj Bjorner 236b2d2ff3 working on incremtal PB theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-13 10:12:45 -08:00
Nikolaj Bjorner 23e811d136 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-05 20:44:56 -08:00
Nikolaj Bjorner 81f1f7690d fix bug in rational.is_int32, it recognized rationals; fix bug reported by Anvesh for integer arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-31 15:59:56 -08:00
Nikolaj Bjorner 5965515385 bugfix to rational and working on adaptive sorting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-27 20:27:37 -08:00
Ken McMillan a318b0f104 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-12-16 12:45:52 -08:00
Ken McMillan 3764064e98 fixed some address dependencies 2013-12-13 18:41:35 -08:00
Nikolaj Bjorner 8c85ee6b7c fixing lex optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-13 23:36:42 +01:00
Nikolaj Bjorner 06ae0db116 working on pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-14 18:04:05 -08:00
Christoph M. Wintersteiger b77d408128 bugfix for FPA rounding when ebits is very small. 2013-11-14 19:11:19 +00:00
Christoph M. Wintersteiger 6a2f987fb7 optimizations for float to float conversions 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-11-14 16:56:13 +00:00
Christoph M. Wintersteiger 7a718d4e07 fixed tabs 2013-11-09 14:57:45 +00:00
Christoph M. Wintersteiger 2924b1acc6 fixed reference to _DEBUG 2013-11-09 14:51:44 +00:00
Nikolaj Bjorner dc78da4873 case analysis for commit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-08 23:29:31 -08:00
Christoph M. Wintersteiger 86f39cd4c1 Changed references to _DEBUG to Z3DEBUG. 
(gcc does not define _DEBUG for debug builds.)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-11-08 19:21:55 +00:00
Nikolaj Bjorner 759d80dfe3 fix regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 12:15:51 -08:00
Nikolaj Bjorner 8fb92e6312 tested network sorting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 10:49:36 -08:00
Nikolaj Bjorner c57594d463 tested network sorting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 10:47:12 -08:00
Nikolaj Bjorner 3ee8c3efb5 pb/car constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 00:53:08 -08:00
Nikolaj Bjorner c0de1e34ac working on upper bound optimziation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-03 14:54:42 -08:00
Nikolaj Bjorner 5106c74b3e preparing for inf extension of arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 02:13:24 -07:00
Nikolaj Bjorner 0b65aa83e8 preparing for inf extension of arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 02:02:37 -07:00
Nikolaj Bjorner bc44bcad10 push blocking code to optimizer context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-29 20:26:54 -07:00
Anh-Dung Phan b67d333cf9 First complete version of Network Simplex 2013-10-29 18:32:10 -07:00
Nikolaj Bjorner 9903c722af adding review notes to code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-26 16:24:21 +08:00
Nikolaj Bjorner 457b22b00e add TPTP example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-06 21:49:00 -07:00
Nikolaj Bjorner 878905c13c Adding overflow checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-02 19:43:22 -07:00
Christoph M. Wintersteiger 76c59cb85c MPF conversion bugfix. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 17:22:25 +01:00
Nikolaj Bjorner b6d9d8a601 fix bugs reported by Nuno Lopes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-04 12:55:35 -07:00
Nuno Lopes 9a66696639 merge hassel table code from branch 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-29 14:35:32 -07: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
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 c58b4f9a53 optimize rule processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-26 11:43:06 -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 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
Nuno Lopes adc8224dba use svector instead of vector where appropriate 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-16 09:02:40 -07:00
Nikolaj Bjorner a054b099c1 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-04-11 13:44:30 -07:00
Nikolaj Bjorner 18ea547cea compiler optimization and fixes to unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-11 13:44:23 -07:00
Leonardo de Moura dc77141dce Fix warning messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-10 19:14:10 -07:00
Leonardo de Moura f6f59ad6bc Fix memory allocation problems in RCF module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-10 19:03:25 -07:00
Leonardo de Moura 75ad174567 Initialize int64_min constant when using GMP 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-08 15:02:51 -07:00
Leonardo de Moura 3d34aa7f01 Fix is_int64 bug in mpz when compiling with GMP 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-08 14:50:17 -07:00
Leonardo de Moura 03c1b24dea Fix get_int64 and is_int64 methods in mpz. Fix INT64_MAX constant definition. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-08 14:25:25 -07:00
Leonardo de Moura 1c96a7d52f Add option smt.bv.enable_int2bv in the new parameter setting framework. This is the new name for the old parameter :bv-enable-int2bv-propagation. This modification addresses an issue reported at http://stackoverflow.com/questions/15798984/bv-enable-int2bv-propagation-option. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-03 15:51:09 -07:00
Nikolaj Bjorner 435c6dd365 convert mega-bytes to bytes in env_params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-29 09:05:36 -07:00
Nikolaj Bjorner c9109132da test hilbert-basis with fdds and checked integers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-26 17:33:44 -07:00
Nikolaj Bjorner 00e79e6b6b test hilbert-basis with fdds and checked integers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-26 17:31:11 -07:00
Nuno Lopes 25a41d48dc speedup bit_vector::num_words() 
Proof of equivalence w.r.t. previous code: http://rise4fun.com/Z3/aiLV

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-03-25 15:41:52 -07:00
Nikolaj Bjorner e61fa50dc3 fix build breaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-24 11:26:46 -07:00
Nikolaj Bjorner ee5d61bd60 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-24 11:26:07 -07:00
Nikolaj Bjorner 6084cbd065 fix build breaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-24 11:25:43 -07:00
Leonardo de Moura 9d0b0df985 Fix gcc compilation errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-24 09:07:51 -07:00
Nikolaj Bjorner 26f4d3be20 significant update to Horn routines: add module hnf to extract Horn normal form (removed from rule_manager). Associate proof objects with rules to track (all) rewrites, so that proof traces can be tracked back to original rules after transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-23 14:11:54 -07:00
Nuno Lopes c824178e7e bit_vector: fix operator==() for the case that num_bits is a multiple of 32 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-03-22 11:50:41 -07:00
Nuno Lopes b8598225bf fix definition of bit_vector::empty() 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-03-18 09:20:25 -07:00
Christoph M. Wintersteiger e5f03f999a FPA: Added conversion operator float -> float. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-04 20:21:14 +00:00
Christoph M. Wintersteiger 7822b86b53 FPA: multiple bugfixes for HWF, MPF and a bugfix for FPA2BV (many thanks to Gabriele Paganelli) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-01 19:06:01 +00:00
Nikolaj Bjorner a14f29a4eb add hilbert basis utility for extracting auxiliary invariants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-12 14:58:04 -08:00
Leonardo de Moura 4624919786 Improve html pretty printer for RCF package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-27 11:24:23 -08:00
Leonardo de Moura 77f58269ed Add html pretty printing mode for RCF package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-27 10:19:54 -08:00
Leonardo de Moura 7312f49f88 Fix Visual Studio warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-13 09:06:07 -08:00
Leonardo de Moura ef11ef61b5 Clean m_val field when switching to GMP bignum 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 17:55:52 -08:00
Leonardo de Moura 4a0b431cf4 Add mk_algebraic method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 11:13:21 -08:00
Leonardo de Moura 1712f0a33b Add goodies 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-09 18:43:32 -08:00
Leonardo de Moura ff809db16d Add get_int and get_uint to mpz_manager 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-08 15:40:19 -08:00
Leonardo de Moura 4d578b418f Fix bug in approx_div 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 21:15:37 -08:00
Leonardo de Moura 3ffda25350 Implement add, sub, mul, div, inv, neg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 18:43:57 -08:00
Leonardo de Moura 322d355290 Simplify data-structures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 11:51:58 -08:00
Leonardo de Moura 1ed275b801 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 22:08:32 -08:00
Leonardo de Moura ed5b106574 Add support for ref_buffers with different initial sizes. Add shrink and operator= methods. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 17:45:28 -08:00
Leonardo de Moura f324724abc Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 17:43:48 -08:00
Leonardo de Moura edf62481e9 Add skeleton for the realclosure package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-02 18:08:42 -08:00
Leonardo de Moura 9a523defa2 Add pp (debugging function) for params_ref 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-28 09:13:18 -08:00
Leonardo de Moura cec328cfdc Add get_sort(expr * n) function that does not depend on ast_manager. Move power_of_two to rational class. Add arith_recognizers and bv_recognizers classes. The two new classes contain the 'read-only' methods from arith_util and bv_util. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 14:44:51 -08:00
Leonardo de Moura 9674f511b3 Fix scoped_timer for Linux. Nested timers were misbehaving, and it was not possible to create timers in more than one thread 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 20:46:04 -08:00
Leonardo de Moura 607fab486c Fix incorrect uses of set_cancel() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 18:48:10 -08:00
Leonardo de Moura 589f2c6bb3 improved unknown parameter error msg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 18:46:02 -08:00
Leonardo de Moura 7f210d55be fixed warnings on Win64 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 07:52:33 -08:00
Leonardo de Moura 840d0aef6d fixed bug in generated code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 18:59:32 -08:00
Leonardo de Moura 47edff2076 fixed bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 08:32:06 -08:00
Leonardo de Moura 8d45de02c5 Fixed timer bug on freebsd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 06:07:57 -08:00
Leonardo de Moura 5e4d1151eb fixing clang compilation problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-05 15:20:16 -08:00
Leonardo de Moura 6f5f1b290e better error message for renamed parameter names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 15:33:21 -08:00
Leonardo de Moura 2eef4cc1e7 forgot synch 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 11:59:46 -08:00
Leonardo de Moura 92a29b1e43 added Z3_global_param_reset_all API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 11:55:12 -08:00
Leonardo de Moura 6d7d205e13 fixed more problems in the new param framework 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 15:02:34 -08:00
Leonardo de Moura 847c5f9691 fixing problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 11:55:24 -08:00
Leonardo de Moura a99b8fe797 exposed rewriter parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 22:03:30 -08:00
Leonardo de Moura 91096b638a better help 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 17:18:25 -08:00
Leonardo de Moura fa53b1eb92 added module descriptions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 13:15:56 -08:00
Leonardo de Moura ffb7e26c75 removed front-end-params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-02 10:05:29 -08:00
Leonardo de Moura 1c15e078a4 cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 23:00:06 -08:00
Leonardo de Moura f15de18c4a context params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 22:53:55 -08:00
Leonardo de Moura 02e763bb6b env params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 20:56:40 -08:00
Leonardo de Moura 29ec68284b Added better error message when old parameter name is used 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 18:34:53 -08:00
Leonardo de Moura 9374a4e20a removed ini_file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 16:30:39 -08:00
Leonardo de Moura 589f096e6e working on new parameter framework 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 15:54:34 -08:00
Leonardo de Moura 9246a7a673 checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-30 13:14:42 -08:00
Leonardo de Moura 722cce0cff checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-29 17:52:07 -08:00
Leonardo de Moura cf28cbab0a saved params work 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-29 17:19:12 -08:00
Leonardo de Moura e0c79c06bc removed class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 15:21:57 -08:00
Leonardo de Moura 8f2a17e20b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-18 00:14:08 -08:00
Leonardo de Moura b169963909 fixed FreeBSD support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-18 00:09:45 -08:00
Leonardo de Moura 1a3eb3a2ed Added support for FreeBSD 2012-11-18 00:05:32 -08:00
Leonardo de Moura ed5d154f78 broke dependency between components that need initialization and memory_manager 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-17 11:30:25 -08:00
Leonardo de Moura 570147e326 removed dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-17 10:33:09 -08:00
Leonardo de Moura e0fcbc101c Added support for clang++ on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-12 04:56:48 +00:00
Leonardo de Moura 683687b153 more cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-31 10:54:59 -07:00
Leonardo de Moura ffcb9741dc Fixed warnings reported by gcc 4.7.1 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-31 00:05:38 -07:00
Leonardo de Moura d8f627c6c8 Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-30 23:43:00 -07:00
Nikolaj Bjorner 6b2f31756b fix build of test-z3 for external release mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-29 11:49:22 -07:00
Leonardo de Moura ae71a4d514 fixed: missing library, more compilation errors in debug mode reported by g++ 4.7.1 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-27 22:51:03 -07:00
Leonardo de Moura 9fb25e7708 fixed more compilation errors reported by g++ 4.7.1 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-27 22:32:50 -07:00
Leonardo de Moura 3f6e3e543f fixed compilation errors reported by g++ 4.7.1 2012-10-27 22:07:27 -07:00
Leonardo de Moura deb5ee395a Fixing new build system for OSX 
Signed-off-by: Leonardo de Moura <leonardo@z3-mac.local>
 2012-10-26 18:28:49 +01:00
Leonardo de Moura 1d03eedeeb script for updating version numbers. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-25 11:52:51 -07:00
Leonardo de Moura f57d4b1b19 reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-25 11:28:03 -07:00
Leonardo de Moura efff6db567 checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-23 12:12:59 -07:00
Leonardo de Moura add684d8e9 checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-21 13:32:12 -07:00
Leonardo de Moura d8cd3fc3ab Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 19:54:08 -07:00
Leonardo de Moura c66b9ab615 Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 15:30:42 -07:00
Leonardo de Moura 8a6997960a Reorganizing code. Added script for generating VS project files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 15:16:37 -07:00
Leonardo de Moura 2c464d413d Reorganizing source code. Created util dir 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 10:19:38 -07:00