* Initial plan
* Add [[nodiscard]] to AST factory functions and modernize iterator loops
- Added [[nodiscard]] attribute to key factory functions in ast.h:
- All mk_app() variants for creating application nodes
- All mk_func_decl() variants for creating function declarations
- All mk_const() variants for creating constants
- All mk_sort() variants for creating sorts
- mk_var() for creating variables
- mk_quantifier(), mk_forall(), mk_exists(), mk_lambda() for quantifiers
- mk_label(), mk_pattern() and related functions
- Converted iterator loops to range-based for loops in:
- src/util/region.cpp: pop_scope()
- src/util/dec_ref_util.h: dec_ref_key_values(), dec_ref_keys(), dec_ref_values()
- src/util/mpf.h: dispose()
- src/util/numeral_buffer.h: reset()
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Modernize additional iterator loops to range-based for loops
- Converted iterator loops to range-based for loops in:
- src/api/api_ast_map.cpp: Z3_ast_map_keys() and Z3_ast_map_to_string()
- src/api/c++/z3++.h: optimize copy constructor and add() method
- src/opt/wmax.cpp: mk_assumptions()
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert changes to z3++.h for C++ version compatibility
Revert the range-based for loop changes in src/api/c++/z3++.h to maintain
compatibility with older C++ versions that users may rely on. The C++ API
wrapper must support down-level C++ standards for backward compatibility.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Trigger CI build
[skip ci] is not used to ensure CI runs
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Fix DEL character encoding in string literals
Change condition from `ch >= 128` to `ch >= 127` to include the DEL
character (U+007F, 127) in escaped output. This ensures that the
non-printable DEL control character is properly escaped as \u{7f}
instead of being printed directly.
Also add test cases for DEL and other control characters.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960)
* draft attempt at optimizing cube tree with resolvents. have not tested/ran yet
* adding comments
* fix bug about needing to bubble resolvent upwards to highest ancestor
* fix bug where we need to cover the whole resolvent in the path when bubbling up
* clean up comments
* close entire tree when sibling resolvent is empty
* integrate asms directly into cube tree, remove separate tracking
* try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function
* separate the logic again to avoid mutual recursion
* Refactor search tree closure and resolution logic
Refactor close_with_core to simplify logic and remove unnecessary parameters. Update sibling resolvent computation and try_resolve_upwards for clarity.
* apply formatting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Refactor close_with_core to use current node in lambda
* Fix formatting issues in search_tree.h
* fix build issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update smt_parallel.cpp
* Change loop variable type in unsat core processing
* Change method to retrieve unsat core from root
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* 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).
Add this option, so that the z3 library can be used in programs that do
signal handling on their own.
Signed-off-by: Mikulas Patocka <mikulas@twibright.com>
scoped_timer::finalize is called from fork. However, it may race with
other threads creating or freeing timer threads.
This patch removes the loop in scoped_timer::finalize (because it is not
needed and it may spin) and also removes two unlocked assignments.
The idle thread is added to "available_workers" in
scoped_timer::~scoped_timer destructor.
If we call the "finalize" method as a part of total memory cleanup, all
the scoped_timers' destructors were already executed and all the worker
threads are already on "available_workers" vector. So, we don't need to
loop; the first loop iteration will clean all the threads.
If the "finalize" method is called from single-threaded program's fork(),
then all the scoped timers' destructors are already called and the case
is analogous to the previous case.
If the "finalize" method is called from multi-threaded program's fork(),
then it breaks down - the "num_workers" variable is the total amount of
workers (both sleeping and busy), and we loop until we terminated
"num_workers" threads - that means that if the number of sleeping workers
is less than "num_workers", the function just spins.
Then, there is unlocked assignment to "num_workers = 0" and
"available_workers.clear()" that can race with other threads doing z3
work and corrupt memory. available_workers.clear() is not needed, because
it was already cleared by std::swap(available_workers, cleanup_workers)
(and that was correctly locked).
Signed-off-by: Mikulas Patocka <mikulas@twibright.com>
