3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Commit graph

503 commits

Author SHA1 Message Date
Nikolaj Bjorner
bc8ae21ebe missing parameters for OSX/Linus
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-18 15:14:47 -07:00
Nikolaj Bjorner
a8e7974011 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-18 14:57:54 -07:00
Nikolaj Bjorner
7a977f0106 ensure that timeouts are distinguished from other cancel events #848
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-18 14:54:54 -07:00
Nikolaj Bjorner
66b24a6c18 change typename to class in optional to deal with compilation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-17 21:00:14 -07:00
Nikolaj Bjorner
ff47c8632b remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-17 20:28:49 -07:00
Nuno Lopes
4b00bc636b revert the patch to remove no-strict-aliasing
VS 2012 doesnt support C++11 unions..
2017-08-14 23:00:59 +01:00
Nuno Lopes
632c2d8ebf use static_assert in COMPILE_TIME_ASSERT 2017-08-14 20:10:17 +01:00
Nuno Lopes
2473c69679 Drop no-strict-aliasing and fix 2 places where it was violated 2017-08-14 20:09:49 +01:00
Nikolaj Bjorner
19bb55e396 recognize theory_i_arith to fix #1200
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-13 10:22:36 -07:00
Lev Nachmanson
95f86ae2c0 more efficient lar_solver::get_model
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2017-08-03 11:03:52 -07:00
Lev Nachmanson
712619a9cf fix a but in adjusting term indices for implied_bounds 2017-08-03 10:09:00 -07:00
Arie Gurfinkel
88a35119b9 moved obj_equiv_class to ast 2017-08-01 19:24:50 -04:00
Christoph M. Wintersteiger
4ff938f2c1 Fixed MPF fp.rem(0,0,0). Relates to #872. 2017-08-01 16:46:10 +01:00
Christoph M. Wintersteiger
79ab8a5a5a Fixed cmake build 2017-08-01 16:16:17 +01:00
Christoph M. Wintersteiger
e315d063c5 renamed LP bound propagator to avoid linker name clashes 2017-08-01 16:07:51 +01:00
Christoph M. Wintersteiger
6bc5209e26 Fixed build problems with .vcxproj 2017-08-01 15:53:55 +01:00
Nikolaj Bjorner
063b6e9ea5 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 13:24:57 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Christoph M. Wintersteiger
bbf0ebcb74 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 20:18:53 +01:00
Christoph M. Wintersteiger
ecfd241e19 Injected 3 missing bits of precision into fp.rem. Relates to #872. 2017-07-31 19:53:44 +01:00
Arie Gurfinkel
1d5713c376 move semantics for ref 2017-07-31 14:21:30 -04:00
Christoph M. Wintersteiger
a59907170d Fixed renormalization in fp.mul. Relates to #872. 2017-07-31 18:34:46 +01:00
Christoph M. Wintersteiger
175f042db8 Fixed renormalization in fp.fma. Relates to #872. 2017-07-28 23:01:01 +01:00
Christoph M. Wintersteiger
e677030b74 Fixed sign bug in mpf fp.fma. Relates to #872. 2017-07-28 21:39:44 +01:00
Christoph M. Wintersteiger
a30c343d7a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-28 20:24:35 +01:00
Christoph M. Wintersteiger
0610392a05 Bugfix for fp.fma. Fixes #872. 2017-07-28 20:16:13 +01:00
Christoph M. Wintersteiger
33ebdc8adc Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872. 2017-07-27 23:08:35 +01:00
Nikolaj Bjorner
6558999cef fixes #1171
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-27 08:46:20 -07:00
Nikolaj Bjorner
b1298d7bde ensure that assertions within the unit tests are exercised in all build modes, remove special handling of SASSERT for release mode #1163
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-26 20:28:55 -07:00
Nikolaj Bjorner
9f9c575451 fix bug exposed when running test-z3.exe /a in debug mode, #1159. Add assertions to heap interaction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-25 16:26:45 -07:00
Christoph M. Wintersteiger
75b533f050 Fixed normalization shift in MPF rounder. Relates to #872. 2017-07-25 20:29:10 +01:00
Christoph M. Wintersteiger
f1c0ac72e7 Fix for fp.fma encoding. Relates to #872. 2017-07-25 20:29:10 +01:00
Nikolaj Bjorner
70f6280bf1 fix regression reported in #1159
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-25 10:18:21 -07:00
Nikolaj Bjorner
a94f5fb04a fix compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-24 12:15:10 -07:00
Nikolaj Bjorner
253870c6d7 fix compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 13:08:23 -07:00
Nikolaj Bjorner
031d7e1b59 use iterators, update build icon for osx
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-01 16:58:40 -07:00
Lev Nachmanson
dfe15adf7e fix maybe non initialized warning
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2017-06-26 16:32:44 -07:00
Nikolaj Bjorner
7db1847f51 fix bitrot in maxsat example reference management #1116
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-26 09:36:53 -07:00
Christoph M. Wintersteiger
2fceac04d4 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-25 22:19:54 +01:00
Christoph M. Wintersteiger
c395516058 Adjusted rlimit increments in theory_arith to avoid non-termination issues 2017-06-25 22:19:42 +01:00
Lev Nachmanson
2a5f1d6e93 add a template instantination
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-06-22 10:32:35 -07:00
Dan Liew
d00892c9a6 [CMake] Fix dependencies for generating mem_initializer.cpp.
Previously CMake was not aware of which headers files the generation
of `mem_initializer.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declare memory initializers/finalizers change.
* New headers are added that declare memory initializers/finalizer.

Now the `z3_add_component()` CMake function has been modifed so that
it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument
which allows the headers that declare memory initializers/finalizers
to be explicitly listed.

With this information CMake will now regenerate `mem_initializer.cpp`
correctly.

This required the `mk_mem_initializer_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
2017-06-21 23:56:53 +01:00
Dan Liew
6f48a145aa [CMake] Fix dependencies for generating gparams_register_modules.cpp.
Previously CMake was not aware of which headers files the generation
of `gparams_register_modules.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared module description/parameters change.
* New headers are added that declare module description/parameters.
* `.pyg` files that generate header files that declare module
  description/parameters change

Now the `z3_add_component()` CMake function has been modifed so that

* All header files that are generated from `.pyg` files are added as
dependencies and are scanned from module description/parameter
declarations. This implicit dependency of `gparams_register_modules.cpp`
depending on other generated header files seems unnecessary complex. We
should revisit this design decision once the Python/Makefile build
system is deprecated.

* The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS`
argument which allows the headers that declare module
description/paramters to be explicitly listed.

With this information CMake will now regenerate `gparams_register_modules.cpp`
correctly.

This required the `mk_gparams_register_modules_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
2017-06-21 23:56:46 +01:00
Arie Gurfinkel
372e8b3c49 expose iterator api of obj_hashtable 2017-06-20 21:07:38 -04:00
Arie Gurfinkel
f3019a3de9 api to accumulate stopwatches 2017-06-20 21:07:38 -04:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Christoph M. Wintersteiger
596652ed36 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-31 18:35:52 +01:00
Christoph M. Wintersteiger
a7d5bb7b36 Tabs 2017-05-31 12:18:00 +01:00
Nikolaj Bjorner
23ff580a67 get rid of timeb dependencies, pull request #1040
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-23 12:16:43 -07:00
Nikolaj Bjorner
2834fea9b3 fix x64 warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-23 08:58:21 -07:00