mirror of
https://github.com/Z3Prover/z3
synced 2026-03-20 03:53:10 +00:00
eb56ac48b0
* 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>
36 lines
859 B
CMake
36 lines
859 B
CMake
z3_add_component(params
|
|
SOURCES
|
|
context_params.cpp
|
|
dyn_ack_params.cpp
|
|
pattern_inference_params.cpp
|
|
preprocessor_params.cpp
|
|
qi_params.cpp
|
|
smt_params.cpp
|
|
theory_arith_params.cpp
|
|
theory_array_params.cpp
|
|
theory_bv_params.cpp
|
|
theory_pb_params.cpp
|
|
theory_seq_params.cpp
|
|
COMPONENT_DEPENDENCIES
|
|
util
|
|
ast
|
|
PYG_FILES
|
|
arith_rewriter_params.pyg
|
|
array_rewriter_params.pyg
|
|
bool_rewriter_params.pyg
|
|
bv_rewriter_params.pyg
|
|
fpa_rewriter_params.pyg
|
|
fpa2bv_rewriter_params.pyg
|
|
pattern_inference_params_helper.pyg
|
|
poly_rewriter_params.pyg
|
|
rewriter_params.pyg
|
|
sat_params.pyg
|
|
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
|
|
context_params.h
|
|
)
|