3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-20 18:20:22 +00:00
Commit graph

28 commits

Author SHA1 Message Date
Nikolaj Bjorner
394d54fa8b fix missin clause generation for ad-hoc handling of conjunction #1245 2017-09-05 09:54:52 -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
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
189d449cff fix generation of wcnf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-18 14:49:45 -08:00
Nikolaj Bjorner
f61600d1d8 fixing unsat core extraction for tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-11-02 14:14:55 +00:00
Nikolaj Bjorner
305e080239 enable unsat core extraction in nlsat_tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-11-01 17:57:28 +01:00
Nikolaj Bjorner
461e88e34c additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-10-25 20:32:13 -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
Nikolaj Bjorner
d614fedde2 more merges with qsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 12:41:41 -07:00
Nikolaj Bjorner
a7e2fb31e3 updates to resource exceptions, update master possibly handle pull request issue
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 11:36:49 -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
baee4225a7 reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 16:21:24 -08: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
Nikolaj Bjorner
cc5d719d9e enable incremental bit-vector solving
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-09-01 09:48:35 -07: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
203c5015c8 fix debian amd64 warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-18 15:17:21 -07:00
Nikolaj Bjorner
18b491eee0 fixes to maxres/mss
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-03 10:03:56 -07:00
Nikolaj Bjorner
ee1a1b1135 refactor sat/sls interface. Remove wpm2 and bvsls dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-08-15 10:40:44 -07:00
Nikolaj Bjorner
39414d8b8d testing inc_sat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-07-31 22:29:47 -07:00
Nikolaj Bjorner
365f05b41a testing inc-sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-07-30 17:49:51 -07:00
Nikolaj Bjorner
4f0de9a0cf implement user scopes for sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-07-30 09:27:03 -07:00
Nikolaj Bjorner
2b1af8fd50 updated sat solver for cores
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-07-29 14:38:17 -07:00
Nikolaj Bjorner
e98acf4ece working on adding basic cores to efficient SAT solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-07-29 07:22:59 -07:00
Christoph M. Wintersteiger
e8dde34353 removed unnecessary changes for bvsls
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-03-26 13:10:06 +00:00
Andreas Froehlich
853ce522cc plenty of new stuff 2014-03-09 15:42:51 +00: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
a274cac2a0 bindings --> api; and moved nlsat/sat/subpaving tactics 2012-10-31 13:25:36 -07:00