Instead of asserting theory axioms lazily we create them on the fly and allow propagation eagerly.
The approach uses a waterfall model as follows:
- terms are created: they are inserted into an index for (set.in x S) axiom creation.
- two terms are merged by an equality.
Loop over all new opportunities for axiom instantiation
New axioms are added to a queue of recently created axioms.
- an atomic formula was asserted by the SAT solver.
Update the watch list to find new propagations.
During propagation recently created axioms are either inserted into a propagation queue, or inserted into a watch list.
They are inserted into a propagation queue all or all but one literal is assigned to false.
They are inserted into a watch list if at least two literals are unassigned
They are dropped if the axiom contains a literal that is assigned to true
The propagation queue is processed by by asserting the theory axiom to the core.
Also add some elementary statistics.
A breaking change is to change the datatype for undo-trail in smt_context to not use a custom data-structure.
This can likely cause regressions. For example, the region allocator now comes from the stack_trail instead of being
owned within smt_context with a different declaration order. smt_context could crash during destruction or maybe even pop.
We take the risk as the change is overdue.
Add swap method to ref_vector.
* 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>
The scoped_timer uses a std::therad. Spawning this thread fails in cases of WASM.
Instead of adapting builds and using async features at the level of WASM and the client, we expose a specialized version of z3 that doesn't use threads at all, neither for solvers nor for timers.
The tradeoff is that the periodic poll that checks for timeout directly queries the global clock each time.
We characterize it as based on polling.
