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
Christoph M. Wintersteiger 3131f29816 whitespace 2016-04-24 15:11:03 +01:00
Nuno Lopes 417c80edbc fix mem leak in quantifier_info::insert_qinfo on timeout 2016-04-19 02:17:12 -07:00
Nikolaj Bjorner c3f4124a9f trace down recent exposed regression in goal2sat, incorporate Scott's suggestion on making vector<std::string inaccessible 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 14:50:10 -07:00
Nuno Lopes 83e34638e6 add support to build with MSVC /Gr (fastcall mode for x86) 
not enabled by default nor exposed at the moment
 2016-03-24 15:39:18 +00:00
Nikolaj Bjorner f175f864ec merge useful utilities from qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:01:44 -07:00
Christoph M. Wintersteiger 371573cbff More implementation of fp.to_ieee_bv for unspecified input/output 
Relates to #507
 2016-03-15 15:11:37 +00:00
Nikolaj Bjorner 71fff8ffa2 fix boundary case according to analysis #477, e.g., size = 252, PTR_ALIGNMENT=2, slot_id = 64 = NUM_SLOTS 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-09 00:42:50 -08:00
Nikolaj Bjorner 49d0e28621 allow parameters to overwrite logic, fixes bug report by Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-07 10:44:06 -08:00
Dan Liew a3e0eae9ec Move CMakeLists.txt files (other than the one in the repository root) 
and the cmake directory into a new directory ``contrib/cmake`` that
mirrors the directory structure of the root. This is a comprimise
between me and Christoph Wintersteiger that was suggested by Arie
Gurfinkel that allows the CMake build system to live in the Z3
repository but not impact the Z3 developers that want to avoid the CMake
build system. The build system will not work in its new location
and a bootstrap script will soon be provided that allows a developer
to copy the files back to their correct location.
 2016-03-04 15:26:09 +00:00
Dan Liew 251527603d Implement a CMake build system. 
This is a large rework of my first attempt at this (#459).

This implementation calls into the recently implemented python scripts
to generate the necessary generated ``.h`` and ``.cpp`` files but is
independent from Python building system otherwise.  Unlike the Python
build system, the generated files are emitted into the build tree to
avoid polluting the source tree. The build system is setup to refuse to
configure if it detects generated files in the source tree. If your
source tree is dirty you can run ``git clean -fx`` to clean your working
directory.

Currently the build succeeds on Linux using CMake 3.4.3 using
the "Unix Makefiles" generator with gcc or clang.

The following notable features are implemented:

* Building of the C and C++ examples and the ``test-z3`` executable.
  These are included from the ``all`` target so you have to tell the
  build system (e.g. make) to build them manually.

* Install (``make install``) and uninstall (``make uninstall``) of libz3
  and its header files. This supports ``DESTDIR`` out of the box because
  CMake supports it.

* An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library.

* Support for using/not using OpenMP (``USE_OPENMP``)

* Support for using/not using libgmp (``USE_LIB_GMP``)

* Setting the SOVERSION for libz3. I'm not sure if I'm setting the
* number correctly though. This is required by Linux distrubtions that
  wills ship libz3. This needs discussion.

The following notable features are currently not implemented
and are left for future work.

* Support for ARM.
* Support for the foci2 library.
* Support for creating/installing/uninstalling the dotnet, java, python and ml
  bindings.
* Full support for MSVC. Although I've tried to write the CMake code
  with MSVC in mind not all the correct flags are passed to it.
* Support for using the git hash.

This new build system has several advantages other the old build system.

* It is easier for outside contributors to contribute to Z3 when the
  build system is something more standard.
* Incremental builds work properly. With the old build system when
  new code is pulled down the old build directory would need to thrown
  out and a new fresh build had to be performed because the build system
  didn't know how to correctly rebuild the project (e.g. couldn't handle
  new sources being added/removed, compiler flags changing, generated
  files changing, etc...). This is a MASSIVE boost to productivity!
* We now have access rich array of features that CMake provides for
  building C/C++ projects. This means less time spent implementing
  custom build system logic in Python that is already supported by
  CMake.
* CMake supports many IDEs out of the box so it should be fairly
  straight forward to build Z3 with Visual Studio (once support for MSVC
  is added), Xcode, Eclipse CDT, CLion, ..etc.
 2016-03-04 15:26:09 +00:00
Christoph M. Wintersteiger c171170bed Fixed FP string input conversions. 
Fixes #464
 2016-03-01 15:31:33 +00:00
Nikolaj Bjorner 6cf76f2113 remove references to _DEBUG use Z3DEBUG instead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 20:23:20 -08:00
Michael Sullivan fa598edf43 Fix gcc build failure on ARM caused by including <emmintrin.h> 
src/util/hwf.cpp tries to use <emmintrin.h> to directly use SSE
intrinsics. Make sure to only use those when actually on x86 or
x86_64.
 2016-02-10 20:47:08 +00:00
Nikolaj Bjorner 5ce85aba40 removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 22:23:37 +00:00
Jonathan Wakely f02d273ee3 Convert stream to bool explicitly 
In C++11 there is no implicit conversion from iostream classes to `void*`, just an explicit conversion to bool.
 2016-02-02 23:39:11 +00:00
Nuno Lopes ee2bae898a remove unused exceeded_memory_allocations class 2016-01-27 18:09:24 +00:00
Christoph M. Wintersteiger 357ec9e7d1 Changed FP significand/exponent functions to return non-normalized results. Clarified function remarks. Relates to #383. 2016-01-13 16:32:32 +00:00
Christoph M. Wintersteiger f093ebe44c Optimization for initialization of mpf's from tiny reals. 2016-01-12 19:06:53 +00:00
Christoph M. Wintersteiger d4efa3753c Optimization for real to float conversion. Relates to #383. 2016-01-11 18:54:07 +00:00
Christoph M. Wintersteiger e53b580cb4 added compiler macro to disable invocation of the debugger upon failure. 2016-01-07 15:58:10 +00:00
Christoph M. Wintersteiger 8b47a84598 Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 11:34:35 +00:00
Christoph M. Wintersteiger 677ff221f8 Internal consistency: FP exponents are always passed before significands. 2016-01-04 18:57:15 +00:00
Nikolaj Bjorner 8e80fb830b merge fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-03 14:12:45 -08:00
Nikolaj Bjorner e2fab0a555 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-28 18:15:48 -08:00
Nikolaj Bjorner 65d147106e automata 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-24 12:01:59 -08:00
Nikolaj Bjorner 995d66c6f2 remove print statements 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 10:46:33 -08:00
Nikolaj Bjorner 9c6271dded add debugging facilities for github issues #384 #367 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 10:43:18 -08:00
Nikolaj Bjorner 65da0f9f3a updated seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-21 06:07:50 -08:00
Nikolaj Bjorner 284fcc2c04 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-20 09:43:56 +02:00
Nikolaj Bjorner f3d94db889 bild on gcc #376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-13 23:47:45 -08:00
Nikolaj Bjorner 72883df134 fix build, add seq features 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-13 16:02:17 -08:00
Nikolaj Bjorner 2ecbe26be1 ensure limit children are safe for race conditions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-12 10:24:19 -08:00
Nikolaj Bjorner 54ac71cada ensure limit children are safe for race conditions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-12 10:23:56 -08:00
Nikolaj Bjorner 4132fc2d91 ensure limit children are safe for race conditions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-12 10:18:51 -08:00
Nikolaj Bjorner 2a051719d8 cleanup deprecated critical sections, fix cancellation for par_or_else tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-12 09:43:00 -08:00
Nikolaj Bjorner 521271e559 moving to resource managed cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 17:46:22 -08:00
Nikolaj Bjorner 32b6b2da44 moving to resource managed cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 13:13:11 -08:00
Nikolaj Bjorner 61dbb6168e cleanup cancelation logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 12:35:35 -08:00
Nuno Lopes 4b0f2cae0d fix compiler warning in scoped_timer.cpp on linux 
2 secs in nanosec representation still fit in 31 bits, so no need for ULL

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-12-08 17:03:18 +00:00
Nikolaj Bjorner 485ac9c39d add macro for converting std::vectors to pointers (leaking abstraction) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-01 16:35:03 -08:00
Nuno Lopes 2739930900 fix build with clang 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-27 12:13:44 +00:00
Nuno Lopes d9bafc3fba rewrite scoped_timer for linux 
The previous version was racy and could lead to crashes.
The timer could be deleted before the callback was called, making it execute on already freed memory

This new version is similar to Mac's. It spawns its own thread and uses pthread_cond_wait.
Care is taken for small timeouts to avoid races in the thread creation and timer destruction.

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-22 11:40:52 +00:00
Nikolaj Bjorner 9cba63c31f remove deprecated iz3 example. Remove deprecated process control 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 12:32:15 -08:00
Nikolaj Bjorner fc592fc856 fix for #291. The root issue is that the set of antecedents is recycled as a fixed object between routines. Antecedents that were already allocated for a Gomory cut got reset by the internalizer. This causes unsound bounds axioms to be created 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-05 15:08:42 -08:00
Nikolaj Bjorner ac3edbbaaa add line/position information to unsupported command reports per zeph pull request 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-30 19:23:31 -07:00
Christoph M. Wintersteiger 6749c19ab1 Merge branch 'static_analysis' of https://github.com/daniel-j-h/z3 
# Conflicts:
#	src/ast/ast.h
#	src/interp/iz3foci.cpp
#	src/muz/duality/duality_dl_interface.cpp
#	src/util/hwf.h
 2015-10-19 15:14:45 +01:00
Nuno Lopes 0e387b2abe use Z3_fallthrough instead of __falthrough directly to avoid messing with reserved identifiers 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-10-09 18:06:49 +01:00
Christoph M. Wintersteiger b60f30c802 Merge pull request #236 from wintersteiger/i68 
Fixes for issue #68
 2015-10-07 20:56:35 +01:00
Christoph M. Wintersteiger 8a026c355f Corrected unspecified behavior of corner cases in fp.min/fp.max. 
Partially addresses #68.
 2015-10-07 20:39:36 +01:00
Christoph M. Wintersteiger fcf036695e Bugfix for mpf to_ieee_bv 2015-10-07 20:37:12 +01:00
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