* 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).
prior data-structure could not represent
((1 + x) div 2) * 2
It is possible to have nested expressions with div.
To deal with this, replace original def by an expression tree data-structure.
- enable sat.smt in smt_tactic that
is invoked by default on first goals
add flatten-clauses
add push-ite
have tptp5 front-end pretty print SMT2 formulas a little nicer.
The example from #6404 results in an incorrect result. It uses integer division on private variables where MBQI support is new and not tested for substitutions.
crash due to not checking for dead rows.
non-termination due to solving div and mod separately.
To ensure termination one needs to at least process them simultaneously, otherwise the metric of number-of-terms x under number of mod/div does not decrease. Substituting in K*y + z under either a mod or div increases the number of terms under a mod/div when eliminating only one of the kinds.
Currently handling divides constraints separately because pre-existing solution uses the model to determine z as a constant between 0 and K-1. The treatment of mod/div is supposed to be more general and use a variable while at the same time reducing the mod/div terms where the eliminated variable is used (the variable z is not added under the mod/div terms, but instead the model is used to determine cut-offs to calculate mod/div directly.
elimination of mod/div should be applied to all occurrences of x under mod/div at the same time. It affects performance and termination to perform elimination on each occurrence since substituting in two new variables for eliminated x doubles the number of variables under other occurrences.
Also generalize inequality resolution to use div.
The new features are still disabled.
This update changes the handling of mod and adds support for nested div terms.
Simple use cases that are handled using small results are given below.
```
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (exists ((x Int)) (and (<= y (* 10 x)) (<= (* 10 x) z))))
(apply qe2)
(reset)
(declare-const y Int)
(assert (exists ((x Int)) (and (> x 0) (= (div x 41) y))))
(apply qe2)
(reset)
(declare-const y Int)
(assert (exists ((x Int)) (= (mod x 41) y)))
(apply qe2)
(reset)
```
The main idea is to introduce definition rows for mod/div terms.
Elimination of variables under mod/div is defined by rewriting the variable to multiples of the mod/divisior and remainder.
The functionality is disabled in this push.
strict inequality (over reals) require solving for least-upper/greatest-lower bounds that may coincide with non-strict inequalities (be epsilon stronger). Instead of using the coefficient 'a' to turn the inequality into an equality, add the slack value as a constant.
