3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-16 01:16:39 +00:00
Commit graph

27 commits

Author SHA1 Message Date
Nikolaj Bjorner
d00ffdda82 strengthen filter for specialized tactic conditions, add flag to disable hnf to lp_params
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-07-15 22:35:47 -07:00
Nuno Lopes
8791f61aa7 reduce mem allocation in tactic API 2018-07-02 13:41:44 +01:00
Nikolaj Bjorner
335d672bf1 fix #1675, regression in core processing in maxres
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-19 23:23:19 -07:00
Nikolaj Bjorner
ff0f257102 remove iff
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
c513f3ca09 merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-25 14:57:01 -07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
b7d1753843 Use override rather than virtual. 2018-02-09 21:19:27 +07:00
Nikolaj Bjorner
79a9dfd8fd adding pre-processing to nlsat for equations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-12-30 20:35:33 -08:00
Nikolaj Bjorner
2f218b0bdc remove also cores as arguments to tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-19 12:18:50 -08:00
Nikolaj Bjorner
4bbece6616 re-organize proof and model converters to be associated with goals instead of external
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-18 16:33:54 -08:00
Nikolaj Bjorner
df6b1a707e remove proof_converter from tactic application, removing nlsat_tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-17 23:32:29 -08: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
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
3989d238c0 fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-13 20:32:18 -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
92b5aac12a adjusting new tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-20 10:13:23 -07:00
Nikolaj Bjorner
c4472ce717 include more qsat features
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 12:29:23 -07: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
035f2bb0da disable unsound simplification of root objects, and incorrect evaluation of negative even roots
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-09 08:41:59 -08: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
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
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