mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-21 09:34:43 +00:00
Code Activity

Some changes to improve LIA performance (#8101)

Browse source 
* add user params

* inprocessing flag

* playing around with clause sharing with some arith constraints (complicated version commented out)

* collect shared clauses inside share units after pop to base level (might help NIA)

* dont collect clauses twice

* dont pop to base level when sharing units, manual filter

* clean up code

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
This commit is contained in:
Ilana Shapiro 2025-12-22 09:47:36 -08:00 • committed by GitHub
parent 97acdb85a2
commit eb56ac48b0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 22 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/CMakeLists.txt
View file

@ -28,6 +28,7 @@ z3_add_component(params
seq_rewriter_params.pyg
sls_params.pyg
smt_params_helper.pyg
smt_parallel_params.pyg
solver_params.pyg
tactic_params.pyg
EXTRA_REGISTER_MODULE_HEADERS

6
src/params/smt_parallel_params.pyg Normal file
View file

@ -0,0 +1,6 @@
def_module_params('smt_parallel',
export=True,
description='Experimental parameters for parallel solving',
params=(
('inprocessing', BOOL, True, 'integrate in-processing as a heuristic simplification'),
))