mirror of
https://github.com/Z3Prover/z3
synced 2026-02-19 23:14:40 +00:00
6d61efa6b8
* 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>
6 lines
No EOL
298 B
Text
6 lines
No EOL
298 B
Text
def_module_params('smt_parallel',
|
|
export=True,
|
|
description='Experimental parameters for parallel solving',
|
|
params=(
|
|
('inprocessing', BOOL, True, 'integrate in-processing as a heuristic simplification'),
|
|
)) |