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

6276 commits

Author SHA1 Message Date
Dan Liew 0e1343e78d [CMake] Add support for link time optimization (LTO).
This analogous to the `--optimize` flag in the Python/Makefile
build system except that we now support doing LTO with Clang/GCC
as well. However it is probably best to avoid doing LTO with
Clang or GCC for now because I see a bunch of warnings about
ODR violations when building with LTO.

LTO can be enabled with the new `LINK_TIME_OPTIMIZATION` option
which is off by default.
2017-04-29 16:22:46 +01:00
Dan Liew fb403229bd [CMake] CMake's default value for CMAKE_CXX_FLAGS includes /W3
remove this so we can have fine grained control of warnings.
2017-04-29 16:22:46 +01:00
Dan Liew fe1af4bcdb [CMake] Teach build system to pass /fp:precise to compiler when
using MSVC. This is set by the old build system but we weren't setting
it. This actually MSVC's default but in an effort to try to behave
more like the old build system we will set it anyway.
2017-04-29 16:22:46 +01:00
Dan Liew f568b2478f [CMake] Report the various values of CMAKE_CXX_FLAGS,
CMAKE_CXX_FLAGS_<CONFIG>, CMAKE_<TYPE>_LINKER_FLAGS, and
CMAKE_<TYPE>_LINKER_FLAGS_<CONFIG>.

This is useful for debugging where some flags come from. Now that
we don't explicitly set the defaults it useful to see which default
values we are getting from CMake.
2017-04-29 16:22:46 +01:00
Dan Liew 4cc2b292c0 [CMake] Remove compiler flag overrides and support for C language.
The setting of overrides was broken (the CXX flags were not set but
the C flags were) and we aren't even using the C compiler any more.

The C compiler is used by the example C project but that is built
as an external project now so we don't need C support anymore.

The setting of defaults was also very fragile. CMake has quite
complicated support here (e.g. MSVC with a clang based tool chain) which
would likely not work properly with the override approach as it existed.

This means we loose some of the custom linker flags we were setting for
MSVC but we were never doing a great job of replicating the exact set of
flags used in the old build system anyway. Subsequent commits will
gradually fix this.
2017-04-29 16:22:46 +01:00
Nikolaj Bjorner 9f99a58569 Merge pull request #992 from mtrberzi/theory_str-static-features
theory_str static features and cmd_context
2017-04-28 11:23:23 -07:00
Murphy Berzish 88147f7047 theory_str static features and cmd_context 2017-04-28 14:14:28 -04:00
Nikolaj Bjorner 62a36189d5 Merge pull request #988 from mtrberzi/theory_str-frontend
Frontend changes for theory_str
2017-04-28 08:21:18 -07:00
Murphy Berzish 05958193ab revert change to String sort declaration 2017-04-27 22:30:02 -04:00
Murphy Berzish 12dd6d786b remove redundant is_seq() check 2017-04-27 21:24:40 -04:00
Murphy Berzish 7811a91bad fix is_string_term() 2017-04-27 13:59:02 -04:00
Nikolaj Bjorner 69aa5ca877 Merge pull request #984 from delcypher/cmake_doxygen
[CMake][Doxygen] Support building/installing API documentation and fix lots of bugs
2017-04-27 06:58:32 -07:00
Nikolaj Bjorner d3b30968fa added chunk based backbone utility
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-04-26 16:55:56 -07:00
Murphy Berzish 46ac718790 theory_str frontend changes 2017-04-26 17:24:05 -04:00
Nikolaj Bjorner a048d74bae adding interval designator to output of non-optimal objectives, fix python doc test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-04-26 14:05:33 -07:00
Nikolaj Bjorner 8032217fd1 tuning and fixing consequence finding, adding dimacs evaluation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-04-26 13:53:37 -07:00
Dan Liew d4b7b489d0 [CMake] Teach CMake to build the documentation for the API bindings
and install them. The target for building the documentation is
`api_docs`.

This is off by default but can be enabled with the
`BUILD_DOCUMENTATION` option. The C and C++ API documentation
is always built but the Python, ".NET", and Java documentation are
only built if they are enabled in the build system. The rationale
for this is that it would be confusing to install documentation
for API bindings that are not installed.

By default `ALWAYS_BUILD_DOCS` is on which will slow down builds
significantly but will ensure that when the `install` target is
invoked the documentation is up-to-date. Unfortunately I couldn't
find a better way to do this. `ALWAYS_BUILD_DOCS` can be disabled
to get faster builds and still have the `api_docs` target available.
2017-04-26 11:02:36 +01:00
Dan Liew a6a6a9c29f [Doxygen] Fix link to ".NET" documentation it should point to the
"Microsoft.Z3" namespace, not the "Microsoft.Z3.Context" class.

This mirrors the link provided for the Java API.
2017-04-26 11:02:36 +01:00
Dan Liew 121fd06cc2 [Doxygen] Fix mk_api_doc.py so it is not required that the current
working directory be the `doc` directory in the source tree.
2017-04-26 10:44:01 +01:00
Dan Liew e4bec1572a [Doxygen] Teach mk_api_doc.py to allow multiple search paths
for the ".NET" and "Java" bindings. The CMake build system needs
this because the generated files exist in a different directory
to the source files.

Multiple paths can be specified using the `--dot-search-paths` and
`--java-search-paths` options.
2017-04-26 10:42:57 +01:00
Dan Liew 09d7ebf1ad [Doxygen] Fix bug where temporary directory and output directory
paths were not handled properly if paths contained spaces.
2017-04-26 10:42:57 +01:00
Dan Liew fa8f6f20a5 [Doxygen] Teach mk_api_doc.py to prevent ".NET", "Z3py" and "Java"
bindings from appearing in the generated documentation. This can
be enabled with `--no-dotnet`, `--no-z3py`, and `--no-java`
respectively.

This fine-grained control is being added for the CMake build system
which will need this control.
2017-04-26 10:42:57 +01:00
Dan Liew cb6baa8bcb [Doxygen] Put the path to the directory containing the Z3py package
at the beginning of the search path so it is picked up first. This
is to try to avoid picking an installed copy of Z3py.
2017-04-26 10:42:57 +01:00
Dan Liew e309174ec9 [Doxygen] Add --z3py-package-path command line option to
`mk_api_doc.py` so that the location of the z3py package can
be specified. This is needed by the CMake build system because
the complete Z3py package is not emitted in the source tree.

Also fix a bug in the path added to the module/package search path.
The directory containing the `z3` package needs to be added not
the `z3` package directory itself.
2017-04-26 10:42:57 +01:00
Dan Liew fe702d7782 [Doxygen] Fix warning about non-existent functions.
`Z3_push` and `Z3_pop` should be `Z3_solver_push` and `Z3_solver_pop`
respectively.
2017-04-26 10:42:57 +01:00
Dan Liew 7242a77a3f [Doxygen] Fix typo found with Doxygen warning
```
warning: Found unknown command `\s'
```
2017-04-26 10:42:57 +01:00
Dan Liew eb1c985a94 [Doxygen] Fixed malformed code blocks in z3_api.h.
These malformed `\code` blocks caused broken documentation to
be generated.
2017-04-26 10:42:57 +01:00
Dan Liew 33af478ce2 [Doxygen] Fix some indentation in doxygen configuration file template. 2017-04-26 10:42:57 +01:00
Dan Liew c78bf66df3 [Doxygen] Fix bug in mk_api_doc.py where the generated
doxygen configuration would not point at the correct path to
the temporary directory.
2017-04-26 10:42:57 +01:00
Dan Liew 5a66f05384 [Doxygen] Teach mk_api_doc.py to use @ style substitutions
to control whether OCaml documentation link is emitted.
2017-04-26 10:42:57 +01:00
Dan Liew b4f8b001ce [Doxygen] Teach mk_api_doc.py a new command line option
(`--output-dir`) to control where output files are emitted.

This is implemented by making `z3api.dox` a template file
(renamed `z3api.cfg.in`) and populating the template at build
time with the required settings.
2017-04-26 10:42:57 +01:00
Dan Liew 5f7ae920c6 [Doxygen] Teach mk_api_doc.py a new command line option (--temp-dir)
which allows the location of the temporary directory to be controlled.

While I'm here also write `website.dox` into the temporary directory
where it belongs instead of in the source tree and simplify the logic
that deletes the temporary directory and its contents.
2017-04-26 10:42:48 +01:00
Nikolaj Bjorner dedc130e98 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-25 10:30:16 -07:00
Nikolaj Bjorner bd8b0186d6 make SMT consequence finding work with compound terms and formulas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-04-25 10:30:10 -07:00
Nikolaj Bjorner 48b62d34b7 make sure consequence generation works with interpreted atoms/terms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-04-24 18:08:52 -07:00
Dan Liew 8a1df3df62 [Doxygen] Add --doxygen-executable command line option to
`mk_api_doc.py`. This allows a custom path to Doxygen to be specified.
2017-04-24 21:52:59 +01:00
Dan Liew 2cdb45605d [Doxygen] Switch to using argparse to parse command line arguments
in `mk_api_doc.py`. Given that we need to add a bunch of new command
line options it makes sense to use a less clumsy and concise API.
2017-04-24 21:48:34 +01:00
Nikolaj Bjorner 34acaa8f56 update license for space/quotes per #982
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-04-24 13:34:10 -07:00
Nikolaj Bjorner 049cb957ea Merge pull request #983 from Baltoli/fixpoint-no-return
Return check result in fixedpoint object
2017-04-24 08:33:13 -07:00
Dan Liew ca678c3675 [Doxygen] Fix bug where def_Type directives in z3.h would appear
in generated doxygen documentation.
2017-04-24 15:45:57 +01:00
Dan Liew 81ba729aab [Doxygen] Fix script --help functionality. 2017-04-24 15:25:45 +01:00
Bruce Collie ce67c8277c Return check result in fixedpoint object
This is a small change to fix a missing return statement.
2017-04-24 12:59:44 +00:00
Nikolaj Bjorner 5068d2083d tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-04-22 11:36:03 -07:00
Nikolaj Bjorner 4f455c7a3c Merge pull request #981 from mtrberzi/theory-assumptions
pre-init assumptions and unsat core validation for smt theories
2017-04-22 11:27:57 -07:00
Murphy Berzish 367cc4b77f check result of unsat core validation 2017-04-22 13:36:09 -04:00
Murphy Berzish a1bb1f2a13 pre-init assumptions and unsat core validation for smt theories 2017-04-22 13:15:00 -04:00
Nikolaj Bjorner 2642ef47ce Merge pull request #980 from delcypher/readme_tweak
Readme tweak to fix #979
2017-04-20 11:04:09 -07:00
Dan Liew 2badef9d0b Be more explicit about using Clang as the compiler as noted in #979.
Referring to the ``mk_make.py`` line might lead someone to think they
need to modify the ``mk_make.py`` file rather than change the command
line invocation.
2017-04-20 17:25:00 +01:00
Dan Liew 4b0f7bc222 Fix typo noted in #979. g++ is the default compiler rather than the gcc binary. 2017-04-20 17:22:05 +01:00
Christoph M. Wintersteiger 0a0b17540f Added rlimit.inc() for expensive interval exponentiation in the non-linear arithmetic theory. 2017-04-19 13:07:04 +01:00