- proofs are output into file `proof.dot` if `(get-proof-graph)` is
in the input
- use `dot -Txlib proof.dot` to see the proof
- use `dot -Tsvg proof.dot` to get a svg file
removing dependencies on simplifier, support SMTLIB2 parametric algebraic datatypes.
This is a breaking change. It introduces two substantial changes:
1. The legacy simplifier is removed. It was obsoleted with the introduction of the rewriter facilities, but many dependencies made it a major change to remove the legacy simplifier. All uses of the legacy simplifier have now been replaced by corresponding calls to the rewriter. It means that some normalization may behave differently. At this point, Z3 passes regressions and passes performance tests without regressing.
2. Algebraic datatypes in the form of SMT-LIB2.6 are now supported. These generalize the datatypes supported so far as parametric datatype constructors may be applied to different arguments within a recursive definition.
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.
