This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.
This is a second version of https://github.com/Z3Prover/z3/pull/9957. I
address @NikolajBjorner 's comments about not changing the semicolons
after macro invocations, because some editors work better with them
present. It now, to the best of my ability, only deletes semis:
* after the closing brace of namespace decl.
* after the closing brace of an extern "C" decl.
* after a function definition.
This PR is very large, but it consists entirely of deletions of
semicolons in these situations.
(If there was a way to update the previous PR, which had been closed,
and that is preferable, please let me know. I couldn't figure it out.)
Add new parallel algorithm as a tactic (parallel_tactical2.cpp)
Don't port over old experiments from smt_parallel that we aren't using
(sls, inprocessing, failed_literal_mode for bb detection)
Fix bugs: lease cancellation/reslimit race condition, involves changing
lease epoch to simple boolean flag
Also, now there is a single shared set of params for the tactic and
smt_parallel
**Test runs for the parallel_tactical2 vs old smt_parallel version:**
run-2747-Z3-threads-4-qflia-30s-stats.md
run-2746-Z3-threads-4-qflia-30s-parallel_tactic-stats.md
run-2745-Z3-threads-1-qfbv-30s-stats.md
run-3013-Z3-threads-4-qfbv-30s-parallel_tactic-stats.md --> note this is
indeed run-3013, I reran after a bugfix in inc_sat_solver
run-2743-Z3-threads-4-qfnia-30s-stats.md
run-2742-Z3-threads-4-qfnia-30s-parallel_tactic-stats.md
**Test runs for the new smt_parallel with bugfixes:**
run-2801-Z3-threads-4-qflia-30s-smtparallel-bugfixes-stats.md,
run-2800-Z3-threads-4-qflia-30s-smtparallel-bugfixes-stats.md
run-2797-Z3-threads-4-qfnia-30s-smtparallel-bugfixes-stats.md
compare to old smt_parallel:
run-2747-Z3-threads-4-qflia-30s-stats.md
run-2743-Z3-threads-4-qfnia-30s-stats.md
Note that there is a slight regression on lia in run-2800. The source of
this appears to be the new new LP largest-cube LIA heuristic param,
which is enabled by default. disabling this param in run-2801 restored
performance (I didn't change this in this PR though, just something to
note)
http://mtzguido.tplinkdns.com:8081/z3/compare_stats.html
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation
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.
this will allow copying the solver state within a scope.
The new solver state has its state at level 0. It is not possible to pop scopes from the new solver (you can still pop scopes from the original solver). The reason for this semantics is the relative difficulty of implementing (getting it right) of a state copy that preserves scopes.
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))
```
