* 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).
spacer would drop variables of sorts not handled by main loop.
- projection with witness needs to disable qel style preprocessing to ensure witnesses are returned.
- add euf plugin to handle uninterpreted sorts (and then uninterpreted functions)
Add API solve_for(vars).
It takes a list of variables and returns a triangular solved form for the variables.
Currently for arithmetic. The solved form is a list with elements of the form (var, term, guard).
Variables solved in the tail of the list do not occur before in the list.
For example it can return a solution [(x, z, True), (y, x + z, True)] because first x was solved to be z,
then y was solved to be x + z which is the same as 2z.
Add congruent_explain that retuns an explanation for congruent terms.
Terms congruent in the final state after calling SimpleSolver().check() can be queried for
an explanation, i.e., a list of literals that collectively entail the equality under congruence closure.
The literals are asserted in the final state of search.
Adjust smt_context cancellation for the smt.qi.max_instantiations parameter.
It gets checked when qi-queue elements are consumed.
Prior it was checked on insertion time, which didn't allow for processing as many
instantations as there were in the queue. Moreover, it would not cancel the solver.
So it would keep adding instantations to the queue when it was full / depleted the
configuration limit.
* qe_lite: cleanup and comment
no change to code
* mbp_arrays: refactor out partial equality (peq)
Partial array equality, PEQ, is used as an intermediate
expression during MBP for arrays. We need to factor it out
so that it can be shared between MBP-QEL and existing MBP.
Partial array equality (peq) is used in MBP for arrays.
Factoring this out to be used by multiple MBP implementations.
* rewriter: new rewrite rules
These rules are specializes for terms that are created in QEL.
QEL commit is comming later
* datatype_rw: new rewrite rule for ADTs
The rule handles this special case:
(cons (head x) (tail x)) --> x
* array_rewriter rules for rewriting PEQs
Special rules to simplify PEQs
* th_rewriter: wire PEQ simplifications
* spacer_iuc: avoid terms with default in IUC
Spacer prfers to not have a term representing default value of an array.
This guides IUC from picking such terms in interpolation
* mbp_term_graph: replace root with repr
* mbp_term_graph: formatting
* mbp_term_graph: class_props, getters, setters
Class properties allow to keep information for an equivalence class.
Getters and setters for terms allow accessing information
* mbp_term_graph: auxiliary methods for qel
QEL commit is comming later in the history
* mbp_term_graph: bug fix
* mbp_term_graph: pick, refine repr, compute cgrnd
* mbp_term_graph: internalize deq
* mbp_term_graph: constructor
* mbp_term_graph: optionally internalize equalities
Reperesent equalities explicitly by nodes in the term_graph
* qel
* formatting
* comments on term_lt
* get terms and other api for mbp_qel
* plugins for mbp_qel
* mbp_qel_util: utilities for mbp_qel
* qe_mbp: QEL-based mbp
* qel: expose QEL API
* spacer: replace qe_lite in qe_project_spacer by qel
This changes the default projection engine that spacer uses.
* cmd_context: debug commands for qel and mbp_qel
New commands are
mbp-qel -- MBP with term graphs
qel -- QEL with term graphs
qe-lite -- older qelite
* qe_mbp: model-based rewriters for arrays
* qe_mbp: QEL-based projection functions
* qsat: wire in QEL-based mbp
* qsat: debug code
* qsat: maybe a bug fix
Changed the code to follow the paper by adding all predicates above a given
level, not just predicates of immediately preceding level.
* chore: use new api to create solver in qsat
* mbp_term_graph use all_of idiom
* feat: solver for integer multiplication
* array_peq: formatting, no change to code
* mbp_qel_util: block comment + format
* mbt_term_graph: clang-format
* bug fix. Move dt rewrite to qe_mbp
* array_peq: add header
* run clang format on mbp plugins
* clang format on mul solver
* format do-while
* format
* format do-while
* update release notes
---------
Co-authored-by: hgvk94 <hgvk94@gmail.com>
Co-authored-by: Isabel Garcia <igarciac@uwaterloo.ca>
This update includes an experimental feature to access a congruence closure data-structure after search.
It comes with several caveats as pre-processing is free to eliminate terms. It is therefore necessary to use a solver that does not eliminate the terms you want to track for congruence of. This is partially addressed by using SimpleSolver or incremental mode solving.
```python
from z3 import *
s = SimpleSolver()
x, y, z = Ints('x y z')
s.add(x == y)
s.add(y == z)
s.check()
print(s.root(x), s.root(y), s.root(z))
print(s.next(x), s.next(y), s.next(z))
```
