mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
6254 commits 49 branches 53 tags 182 MiB
Commit graph

6254 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
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
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
Christoph M. Wintersteiger
a02a7f4443 Whitespace 2017-04-19 13:04:04 +01:00
Christoph M. Wintersteiger
71da36f85c Added core.extend_nonlocal_patterns parameter to improve unsat cores. 2017-04-18 15:13:11 +01:00
Nikolaj Bjorner
66e61b8a31 issues #963 #912 2017-04-17 03:06:38 -07:00
Nikolaj Bjorner
8b5627e361 additional API per #977 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-16 12:13:30 +09:00
Nikolaj Bjorner
9933c36050 replace long by int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 17:06:03 +08:00
Nikolaj Bjorner
ab6abe901f replace long by int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:57:30 +08:00
Nikolaj Bjorner
87c3b5ee51 replace uint by long 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:29:02 +08:00
Nikolaj Bjorner
e4b9080165 include timeout/rlimit parameters in optmize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:04:13 +08:00
Nikolaj Bjorner
48638c6f1e fix for #975, add mask to ensure character encoding is unique within range of bits used for encoding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 09:34:13 +07:00
Nikolaj Bjorner
7bb5e72e07 add missing string/re operations #977 and adding Pseudo-Boolean operations to Java API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 09:09:30 +07:00
Nikolaj Bjorner
4140afa4cb add regular expression membership for range of int.to.str functions. Issue #957 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-11 10:49:42 +08:00
Nikolaj Bjorner
be3cc91323 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-11 07:40:30 +08:00
Nikolaj Bjorner
67513a2cf5 fix detection of bounds under conjunctions. Issue #971 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-11 07:40:09 +08:00
Christoph M. Wintersteiger
b67c1c5501 Fixed valgrind warning. Fixes #972 2017-04-10 16:28:41 +01:00
Christoph M. Wintersteiger
95cf1447ea Added maintainers.txt for qprofdiff 2017-04-10 13:18:45 +01:00
Nikolaj Bjorner
80c10d5833 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-07 21:22:48 -07:00
Nikolaj Bjorner
ec29a03c8f add facility to dispense with cancellation (not activated at this point). Address #961 by expanding recurisve function definitions that are not tautologies if the current model does not validate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-07 21:22:38 -07:00
Christoph M. Wintersteiger
27a1758857 Added rewriter.ignore_patterns_on_ground_qbody option to disable simplification of quantifiers that have their universals appear only in patterns, but otherwise have a ground body. 2017-04-07 21:19:20 +01:00
Christoph M. Wintersteiger
9a757ffffe Result ordering fix for qprofdiff 2017-04-07 18:12:33 +01:00
Christoph M. Wintersteiger
23f4a0c332 Build fix for qprofdiff 2017-04-07 18:12:26 +01:00
Christoph M. Wintersteiger
f3c990d356 Fixes for qprofdiff 2017-04-07 18:12:16 +01:00
Christoph M. Wintersteiger
d390885757 Added utility to compare quantifier instantiation profiles generated via smt.qi.profile=true 2017-04-06 18:37:29 +01:00