Copilot
2436943794
Standardize for-loop increments to prefix form (++i) ( #8199 )
...
* Initial plan
* Convert postfix to prefix increment in for loops
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix member variable increment conversion bug
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update API generator to produce prefix increments
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>
2026-01-14 19:55:31 -08:00
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
Nikolaj Bjorner
085b5e2588
port Jakob's update to union_find from polysat branch
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-12-18 09:25:24 -08:00
Jakob Rath
5d858da58a
union_find::reserve
2022-08-01 18:37:11 +03:00
Nuno Lopes
f1e0d5dc8a
remove a hundred implicit constructors/destructors
2021-05-23 14:25:01 +01:00
Nikolaj Bjorner
e5892e5e97
#5215
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-04-27 15:26:56 -07:00
Nikolaj Bjorner
15a7621e27
remove template dependency for trail objects
2021-03-19 11:15:05 -07:00
Nikolaj Bjorner
a152bb1e80
remove template Context dependency in every trail object
2021-02-08 15:41:57 -08:00
Nikolaj Bjorner
d02b0cde7a
running updates to bv_solver ( #4674 )
...
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* dbg
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* drat and fresh
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move ackerman functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debugability
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* towards debugability
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove csp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-07 20:35:32 -07:00
Nikolaj Bjorner
d0e20e44ff
booyah
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-04 15:56:30 -07:00
Simon Cruanes
5141f05e6d
fix(union-find): keep values and representative in consistent order
...
the merge handlers should be called with r1,r2,v1,v2 or r2,r1,v2,v1
but not a mix
2018-08-17 14:58:44 -05:00
Bruce Mitchener
7167fda1dc
Use override rather than virtual.
2018-02-10 09:56:33 +07:00
Nikolaj Bjorner
2e6ae8cfd2
fix crash
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-15 23:06:05 -08:00
Nikolaj Bjorner
b19f94ae5b
make include paths uniformly use path relative to src. #534
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
4bc044c982
update header guards to be C++ style. Fixes issue #9
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Nikolaj Bjorner
f100d4feda
hoist out basic union find
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-21 11:10:42 -07:00
Nikolaj Bjorner
4e686693ee
add declaration for w
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-06 08:39:48 -07:00
Nikolaj Bjorner
60d7872cc8
adding simple BCE
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-29 18:00:34 -07:00
Nikolaj Bjorner
989569b154
add bceq experiment
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-29 10:57:31 -07:00
