3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 02:41:52 +00:00
z3/src/solver
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
..
check_sat_result.cpp old_params ==> front_end_params. Isolated abstract solver interface 2012-11-01 11:28:14 -07:00
check_sat_result.h tune consequence finding. Factor solver pretty-printing as SMT-LIB into top-level 2016-08-03 11:14:29 -07:00
CMakeLists.txt [CMake] Move CMake files into their intended location so the 2017-06-12 11:59:00 +01:00
combined_solver.cpp include recursive functions to models. Issue #898 2017-03-08 21:41:24 -08:00
combined_solver.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
combined_solver_params.pyg solver factories, cleanup solver API, simplified strategic solver, added combined solver 2012-12-11 17:47:27 -08:00
mus.cpp expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 2017-02-24 11:07:40 -08:00
mus.h extend constant folding for bit-vector overflow/underflow operators, #657 2016-06-24 07:43:05 -07:00
progress_callback.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
smt_logics.cpp add pb built in ops for logic ALL #1045 2017-05-29 10:08:50 -07:00
smt_logics.h smt_setup framework, all hooks to theory_str are redirected to theory_seq 2017-05-02 17:16:35 -04:00
solver.cpp adding preferred sat, currently disabled, to wmax. Fixing issue #815 2016-11-30 09:52:05 -08:00
solver.h fix bug in propagation of parameters to combined solvers 2017-01-31 17:17:58 -08:00
solver2tactic.cpp fix bug in propagation of parameters to combined solvers 2017-01-31 17:17:58 -08:00
solver2tactic.h 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 2016-10-25 20:32:13 -07:00
solver_na2as.cpp better encodings for at-most-1, #755 2016-10-10 23:46:03 -07:00
solver_na2as.h better encodings for at-most-1, #755 2016-10-10 23:46:03 -07:00
tactic2solver.cpp expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 2017-02-24 11:07:40 -08:00
tactic2solver.h reworking cancellation 2015-12-11 16:21:24 -08:00