Skip to content

Comments

Added counters of already preprocessed assertions#889

Draft
Tomaqa wants to merge 1 commit intopreprocessfrom
preprocess-counters
Draft

Added counters of already preprocessed assertions#889
Tomaqa wants to merge 1 commit intopreprocessfrom
preprocess-counters

Conversation

@Tomaqa
Copy link
Member

@Tomaqa Tomaqa commented Nov 24, 2025

Only matters in incremental solving when it may happen that some assertions are preprocessed multiple times.

If not trackPartitions(), then we do not use the counters and always preprocess all frame formulas again in the hope that it will benefit from the new assertions.

If trackPartitions(), then we use the counters to ensure that every formula is preprocessed at most once.

Requires #888

@Tomaqa Tomaqa force-pushed the preprocess-counters branch from a646c8a to 223bed6 Compare November 24, 2025 10:30
@Tomaqa
Copy link
Member Author

Tomaqa commented Nov 24, 2025

As done in #888, I add a performance comparison in QF_LRA with the 2-minute timeout. This time I always exclude unsat cores and only include (non-)incremental.

Comparison before and after applying this PR:
2025-v2.9.2-23-g883d2889_v2.9.2-24-ga646c8af.scatter.pdf
.. confirms that when not tracking partitions, there is no effect.

Comparison before and after applying this PR when trackPartitions() is forced to true:
2025-v2.9.2-23-g883d2889-dirty_v2.9.2-24-ga646c8af-dirty.scatter.pdf
.. shows a beneficial trend, especially in the case of unsat benchmarks.

Comparison of the new version with and without tracking partitions:
2025-v2.9.2-24-ga646c8af_v2.9.2-24-ga646c8af-dirty.scatter.pdf
.. shows that in the case of unsat benchmarks, the overhead of the tracking is quite low.

@Tomaqa
Copy link
Member Author

Tomaqa commented Nov 24, 2025

I also tried the variant to preprocess formulas at most once when not tracking partitions:
2025-v2.9.2-24-ga646c8af_v2.9.2-25-g762b3b41.scatter.pdf
However, the results are not conclusive. For these benchmarks, it is beneficial for unsat cases, but not for sat cases. It may be worth, though, to allow configuring this option and leave it to the user.

@Tomaqa Tomaqa force-pushed the preprocess-counters branch from f492e9e to 5d64244 Compare December 6, 2025 13:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant