Optimize SAT assumption handling and Saturation queue - #827

Closed

EpsilonPhoenix wants to merge 9 commits into

vprover:masterfrom

EpsilonPhoenix:master

Commits on Mar 18, 2026

avoid rebuilding SATSolver assumptions every iteration
EpsilonPhoenix
committed
a0eb56e
Optimize SAT and Minisat slightly & add tautology handling for the SAT test & premise minimization behavior handling test
EpsilonPhoenix
committed
349878d
optimize Saturation queue & bound ClauseQueue to MAX_HEIGHT & keep LRS from having zero denominators
EpsilonPhoenix
committed
90dda0e
optimize Saturation queue simulation and split queue indexing (precompile ClauseCodeTree literal matching)
EpsilonPhoenix
committed
e5dfe63
typo
EpsilonPhoenix
committed
3083ce9
Resolve comments:
EpsilonPhoenix
committed
1b362e4

Commits on Mar 20, 2026

Remove vector<CodeStack>, keep optimization
EpsilonPhoenix
committed
fdb64c1

Commits on Mar 24, 2026

bound h by _height
EpsilonPhoenix
committed
b7d32be

Commits on Apr 11, 2026

Merge branch 'master' into master
EpsilonPhoenix
authored
0de801a