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

213 commits

Author SHA1 Message Date
Nuno Lopes
912a729097 fix build of unit tests 2017-10-16 00:54:30 +01:00
Nuno Lopes
d1c13f17b0 remove noexcept since MSVC 2012 doest support it 2017-10-16 00:54:30 +01:00
Nuno Lopes
9b54b4e784 fix vector<> to support non-POD types
adjust code to std::move and avoid unnecessary/illegal
2017-10-16 00:54:29 +01:00
Nikolaj Bjorner
8cf0c94e5f address some ASan leaks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-12 14:34:04 -07:00
Nikolaj Bjorner
da2b876acb fix #1303
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-12 07:39:27 -07:00
Murphy Berzish
9b01a5153e fix generation of symbolic automata with no moves but accepting initial state 2017-09-18 14:44:05 -04:00
Christoph M. Wintersteiger
00651f8f21 Tabs, formatting. 2017-09-17 14:54:09 +01:00
Nikolaj Bjorner
059bad909a prune dead states from automata
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-31 07:33:55 -07:00
Nikolaj Bjorner
4d8290ebc2 update to theory_seq following examples from PJLJ
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-30 14:04:02 -07:00
Nikolaj Bjorner
feac705cb8 include epsilon closure in initial state set, streamline final configuration computation #1224
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-28 13:47:19 -07:00
Nikolaj Bjorner
0ebb917268 complement regular expressions when used in negated membership constraints #1224
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-28 01:40:15 -07:00
Nikolaj Bjorner
974eaab01c complement regular expressions when used in negated membership constraints #1224
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-28 01:38:23 -07:00
Nikolaj Bjorner
2b82fd5d0c updated include directives
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-01 10:51:47 -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
Nikolaj Bjorner
6558999cef fixes #1171
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-27 08:46:20 -07:00
Nikolaj Bjorner
1a07c6c188 address ASAN bug report #1160
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-26 20:48:49 -07: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
Dan Liew
229fd3dc3e [CMake] Fix dependencies for generating install_tactic.cpp.
Previously CMake was not aware of which headers files the generation
of `install_tactic.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared tactics/probes changed.
* New tactics/probes were added to new header files.

Now the `z3_add_component()` CMake function has been modifed to take an
optional `TACTIC_HEADERS` argument which allows the headers that declare
tactics/probes to be explicitly listed. The necessary component
declarations have been modified to declare their tactic/probe header
files.

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

This required the `mk_install_tactic_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:03:48 +01: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
Nikolaj Bjorner
331658f208 remove polynomial factorization as suggested by issue #852
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-01-09 21:30:54 -08:00
Nikolaj Bjorner
e092232f67 add virtual destructors, fix operator code for API methods complement and intersection per note by Loris d'Antoni
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-09 23:17:52 +01:00
Nikolaj Bjorner
82d0310d94 remove repeated default argument, remove tabs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-28 21:13:12 -07:00
Nikolaj Bjorner
fa48703445 fix build for non C++11
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-28 17:04:47 -07:00
Nikolaj Bjorner
0055254f4c fix build for non C++11
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-28 17:04:06 -07:00
Christoph M. Wintersteiger
2e362aa6c0 build fix 2016-07-29 01:02:48 +01:00
Loris D'Antoni
73bd4acfc5 added symbolic automata complement for sequences 2016-07-28 13:50:05 -07:00
Nikolaj Bjorner
67c6f9be91 have the classifier revert to full arithmetic on non-difference logic, reported on 38596187 (3)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-26 10:32:54 -07:00
Nikolaj Bjorner
64674386de fix ubuntu build failure
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-15 13:39:50 -07:00
Fabian Wolff
6eaab00e83 Fix spelling errors 2016-07-09 11:46:43 +02:00
Nikolaj Bjorner
84aec95eda fix up use-list in 3x3 resolution case. Regression RND_3_24.smt2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-28 11:41:57 -07:00
Nikolaj Bjorner
b66d457b19 move arithmetical mbp functionality to model_based_opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-26 16:12:14 -07:00
Nikolaj Bjorner
7fc294d329 move arithmetical mbp functionality to model_based_opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-26 14:30:35 -07:00
Nikolaj Bjorner
5b497b6249 reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-22 20:25:47 -07:00
Nikolaj Bjorner
9c099d6b1b fix mb maximization logic, so far not accessible
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-20 16:39:03 -07:00
Johannes Kanig
9bfa73ee06 Take into account number of monomials for rlimit counting
Should fix issue #611
2016-06-08 11:17:26 +09:00
Nikolaj Bjorner
339cd6e537 mbo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-20 13:45:50 -07:00
Nikolaj Bjorner
5e7db2e3e2 disable mk_array_eq as it breaks model evaluation/validation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-18 08:29:24 -07:00
Nikolaj Bjorner
40f8e16273 removing warnings for unused variables, #579
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-17 14:00:30 -07:00
Nikolaj Bjorner
96e157e201 fix warnings for unused variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-17 13:54:22 -07:00
Nikolaj Bjorner
42726171b5 add limit checks in Grobner. Issue #599
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-15 11:34:48 -07:00
Nikolaj Bjorner
67e49b4adc fixing model-based-opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-01 17:15:20 -07:00
Nikolaj Bjorner
22507281cf fix model generation in opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-30 12:23:46 -07:00
Nikolaj Bjorner
e29adbf304 fix issues #581: nested timeouts canceled each-other
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-30 11:18:34 -07:00
Nikolaj Bjorner
2428bf18f1 add model correction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-29 19:08:10 -07:00
Nikolaj Bjorner
c75fd02c95 qsat-opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-28 21:31:16 -07:00
Nikolaj Bjorner
932ef442ae model based opt dev
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-28 09:47:55 -07:00
Nikolaj Bjorner
6aa6102891 factor out model-based-opt code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-27 15:08:10 -07:00
Nikolaj Bjorner
68c7d64d00 adding model-based opt facility
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-27 11:18:20 -07: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
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