3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Commit graph

462 commits

Author SHA1 Message Date
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
Lev Nachmanson 1b62592015 change in a comment
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-05-18 13:44:00 -07:00
Nikolaj Bjorner 79a8e9aab0 fix build break #1029
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-18 12:09:51 -07:00
Nikolaj Bjorner 4069e76ab0 remove unused column function field, #1021
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-16 21:27:43 -07:00
Nikolaj Bjorner 3290a933b5 remove spurious include file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-14 14:09:42 -07:00
Nikolaj Bjorner a0efdc21c3 add missing locks around mpz operations that access object allocator. Use internal skolem constant for theory assumption to hide it from models
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-14 14:04:00 -07:00
Lev Nachmanson 07f2fd43bb Merge remote-tracking branch 'upstream/master' 2017-05-11 17:49:33 -07:00
Lev Nachmanson d0d71a0907 allow more failures in d_solver
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2017-05-11 17:49:27 -07:00
Nikolaj Bjorner a9e2a1204e add this qualifier for build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 16:58:29 -07:00
Nikolaj Bjorner 7b35eacf63 add this qualifier for build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 16:52:54 -07:00
Nikolaj Bjorner 2ab0f281f3 add this qualifier for build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 16:50:39 -07:00
Nikolaj Bjorner 29a49f4427 convert static random fields to non-static
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 16:46:07 -07:00
Lev Nachmanson cf8b35a6f3 fix init reorder warning
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2017-05-11 10:54:18 -07:00
Nikolaj Bjorner 431feab1bf fix build warnings part 8
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 09:37:01 -07:00
Nikolaj Bjorner 7e004fe331 fix build warnings part 7, disable LRA for regression t201.smt2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 09:28:59 -07:00
Nikolaj Bjorner 49d2b86d35 fix build warnings part 6
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 08:57:17 -07:00
Nikolaj Bjorner b9a695633d fix build issues part 4 2017-05-11 08:18:20 -07:00
Nikolaj Bjorner 6e021781cd fix build issues part 3
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 07:49:41 -07:00
Nikolaj Bjorner fcfaedd9ec fix build issues part 2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 07:39:56 -07:00
Nikolaj Bjorner 2a905e02c8 fix build issues part 1
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 07:38:52 -07:00
Nikolaj Bjorner 714dfaded3 Merge pull request #1017 from levnach/123
123
2017-05-11 07:31:40 -07:00
Lev Nachmanson b08f094620 merging with the lp fork
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-05-10 16:53:25 -07:00
Nikolaj Bjorner f03f471f02 fix for #1016
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-10 15:13:04 -07:00
Lev Nachmanson cf695ab876 taking changes from the fork
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-05-10 10:43:01 -07:00
Nikolaj Bjorner 74ac58de2b enable generic parameters with smt-tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-10 10:18:50 -07:00
Nikolaj Bjorner f572c79cdb add instances
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 19:55:24 -07:00
Nikolaj Bjorner f4544eb060 disambiguating arguments to unordered map erase and dealing with unused and uninitialized variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 15:35:00 -07:00
Nikolaj Bjorner d43c12413d add disambiguation, avoid uninitialzed variable passing in debug mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 15:27:42 -07:00
Nikolaj Bjorner f12f83af83 fix warnings, avoid class qualification in static function
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:56:38 -07:00
Nikolaj Bjorner c5f1f8ba59 missing files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:14:58 -07:00
Nikolaj Bjorner 905cf08e5d missing files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:11:33 -07:00
Nikolaj Bjorner 911b24784a merge LRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 10:46:11 -07:00
Nikolaj Bjorner 085d31dca2 mpq/mpz features from LRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 09:18:59 -07:00
Nikolaj Bjorner 60725f5384 use vector fixes from LRA branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 09:13:27 -07:00
Nikolaj Bjorner 42ea2d1ea5 LRA changes to rational
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 09:06:41 -07:00
Murphy Berzish ede6d7bb2b add iterator accessors to obj_pair_set 2017-05-03 14:55:22 -04:00
Christoph M. Wintersteiger f8d022a180 Non-windows build fix 2017-03-24 15:25:18 +00:00
Christoph M. Wintersteiger fb105afac2 Windows build fix 2017-03-24 15:22:33 +00:00
Christoph M. Wintersteiger 7f9c37e19d VS2017 SSE4 intrinsics build fix 2017-03-24 14:23:39 +00:00
Christoph M. Wintersteiger e9cd4d1057 Build fix for systems that don't come with SSE4.1 support by default 2017-03-24 11:51:36 +00:00
Nikolaj Bjorner e47e8c67c0 introducing scoped detacth/attach of clauses to enforce basic sat solver invariants. Part of investigating #939:
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-03-22 14:12:47 -07:00
Nuno Lopes 8ac060c549 fix build with VS 2017 2017-03-20 09:12:41 +00:00