98 Commits

Author SHA1 Message Date
LeeYoungJoon
0a93ff515d Centralize and document TRACE tags using X-macros (#7657)
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros

* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md

* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled

* trace: improve trace tag handling system with hierarchical tagging

- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
  (class names and descriptions to be refined in a future update)

* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals

* trace : add cstring header

* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py

* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.

* trace : Add TODO comment for future implementation of tag_class activation

* trace : Disable code related to tag_class until implementation is ready (#7663).
2025-05-28 14:31:25 +01:00
Bruce Mitchener
9d1ceab1f2 cmake: Use FindPython3. (#7019)
`FindPythonInterp` has been deprecated for a long time and is more
verbal about that deprecation now.

The build system no longer uses `PYTHON_EXECUTABLE` but instead uses
`Python3_EXECUTABLE`.
2023-11-27 11:20:21 +01:00
Kevin Phoenix
1a9990a92f Use sys.getdefaultencoding() instead of sys.stdout.encoding (#6612) 2023-02-28 11:46:10 -08:00
Nikolaj Bjorner
e6f8fe359e remove empty file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-31 12:32:28 -08:00
Nikolaj Bjorner
d263b373ed update release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-31 12:19:33 -08:00
Nikolaj Bjorner
971b9d4081 fix #6564
fixes to simplifier command front-end
2023-01-31 09:32:34 -08:00
Nikolaj Bjorner
238d604a10 android 16 byte alignment for stack allocated memory?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-30 23:00:44 -08:00
Nikolaj Bjorner
5794d080b5 updated doc generation script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-30 22:52:32 -08:00
Nikolaj Bjorner
c07b6ab38f more tactic descriptions 2023-01-05 20:23:01 -08:00
Nikolaj Bjorner
e423fabf6a tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-15 20:35:36 -08:00
Nikolaj Bjorner
a9f52b0069 doc fixes 2022-12-11 10:04:01 -08:00
Nikolaj Bjorner
7e69dab8f6 distribute forall cpp code 2022-12-06 18:15:18 -08:00
Nikolaj Bjorner
80033e8744 cave in to supporting proofs (partially) in simplifiers, updated doc 2022-12-06 17:02:04 -08:00
Nikolaj Bjorner
1e06c7414a add doc 2022-12-06 15:44:21 -08:00
Nikolaj Bjorner
5a5758baaa add documentation to initial selection of tactics 2022-12-05 20:05:06 -08:00
Nikolaj Bjorner
0eea021dc3 include global parameters and fixup for HTML meta-characters 2022-08-22 14:25:18 -07:00
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