3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Commit graph

82 commits

Author SHA1 Message Date
Nikolaj Bjorner 21033790be add parameter documentation to nightly 2022-08-16 15:07:19 -07:00
Nikolaj Bjorner fe00e95f72 remove \r from output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-16 09:20:50 -07:00
Nikolaj Bjorner 498b6de3a7 finish parameter help
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-16 08:29:24 -07:00
Nikolaj Bjorner b169292743 add parameter descriptions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-16 08:26:53 -07:00
Bruce Mitchener 42f5047463 cmake: Cleanup remnants of workaround for USES_TERMINAL.
In older versions, this was dependent upon the version of cmake,
but when it was updated for newer cmake, these remnants were
left.
2022-08-02 17:39:10 +03:00
Bruce Mitchener 059b795faa Fix warning about \ref when building website.dox 2022-08-01 18:51:20 +03:00
Bruce Mitchener c682ec1135 Remove remaining references to Z3_bool_opt. 2022-07-30 05:48:27 +02:00
Nikolaj Bjorner b5a89eb4ab add missing generation of z3.z3 for pydoc and add some explanations to logging function declaration 2022-07-17 11:03:55 -07:00
Nikolaj Bjorner 2e797045fa remove space
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-11 20:33:12 -07:00
Nikolaj Bjorner 3c94083a23 fix doc errors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-01 15:29:44 -07:00
Olaf Tomalka 7fdcbbaee9
Add high level bindings for js (#6048)
* [Draft] Added unfinished code for high level bindings for js

* * Rewrote structure of js api files
* Added more high level apis

* Minor fixes

* Fixed wasm github action

* Fix JS test

* Removed ContextOptions type

* * Added Ints to JS Api
* Added tests to JS Api

* Added run-time checks for contexts

* Removed default contexts

* Merged Context and createContext so that the api behaves the sames as in other constructors

* Added a test for Solver

* Added Reals

* Added classes for IntVals and RealVals

* Added abillity to specify logic for solver

* Try to make CI tests not fail

* Changed APIs after a round of review

* Fix test

* Added BitVectors

* Made sort into getter

* Added initial JS docs

* Added more coercible types

* Removed done TODOs
2022-06-14 09:55:58 -07:00
Nikolaj Bjorner 4953b95baa cleanup pre-processor for z3_api.h
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 12:19:39 -07:00
Nikolaj Bjorner 8d980ea704 remove internal configuration
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 12:13:18 -07:00
Andreas 4f4e9a9963
fix a tiny typo (#5960)
A dot.
2022-04-11 08:40:03 +02:00
Nikolaj Bjorner 2b71d8bc08 doc macros 2022-03-03 14:59:38 -08:00
Nikolaj Bjorner c99b805c14 mld
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-29 18:37:38 -08:00
Nikolaj Bjorner 34c34b68ee one more nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-29 16:40:59 -08:00
Nikolaj Bjorner 2ead209d40 indentation and updated links to default landing pages 2021-01-11 13:21:52 -08:00
Nikolaj Bjorner bcbda45298 updates to doc 2021-01-11 13:03:55 -08:00
Nikolaj Bjorner 5cbabb20ac align readme-cmake and cmakelists.txt according to current state #2732
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-23 15:59:16 -08:00
Jerry James 8db0429809 Fix "Unbound module Z" error when invoking ocamldoc. 2019-11-21 16:04:17 -08:00
Nikolaj Bjorner b50f8508f2 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:50:53 -08:00
Nikolaj Bjorner e9d9792524 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:39:04 -08:00
Nikolaj Bjorner 8c8a8cee7a add build step to generate doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-10-11 13:12:14 -07:00
Charlie Barto 167f968fa8 Change from BINARY_DIR to PROJECT_BINARY_DIR 2019-05-15 11:25:40 -07:00
Nikolaj Bjorner ccca063e54 Merge branch 'master' of https://github.com/Z3Prover/z3 into csp 2018-10-21 12:26:53 -07:00
Florian Pigorsch 326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Nikolaj Bjorner c7d0d4e191 add c-cube's recursive function theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-17 04:56:58 -07:00
Nikolaj Bjorner 8eeaa27cf3 remove interp from documentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 07:33:43 -07:00
Simon Cruanes d5e134dd94 wip: add recursive functions 2017-12-25 22:51:39 +01:00
Simon Cruanes fba22d2fac design document for handling recursive functions 2017-12-25 22:51:39 +01:00
Christoph M. Wintersteiger c3c06d756c Documentation fixes. 2017-12-18 20:12:19 +00:00
Dan Liew 1a0bff7480 [CMake] When invoking mk_api_doc.py pass the build directory.
This change was requested by @wintersteiger as an alternative way
to unbreak the TravisCI builds.
2017-11-13 22:31:05 +00:00
Christoph M. Wintersteiger d44d918414 API doc build fix. Related to #1350. 2017-11-11 14:19:38 +00:00
Christoph M. Wintersteiger a173b0faf7 Fixed API doc build 2017-11-09 13:34:32 +00:00
Max ulidtko ce6e26043a fix Python API doxygen (make api_docs) 2017-09-27 14:07:18 +03:00
Max ulidtko f07b89df86 fix pydoc part of make api_docs 2017-09-27 14:07:02 +03:00
Nikolaj Bjorner 2b0106c199 doc fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-09 11:26:27 +02: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
Dan Liew 903709b9c1 [Doxygen] Fix bug where some header files were not being scanned. 2017-06-07 17:09:01 +01:00
Dan Liew 6261a5c27b Fix bug in mk_api_doc.py where the Z3 python package path would be
checked when building the Z3 python package documentation was disabled.
2017-05-04 15:28:20 +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 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