3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-18 06:36:24 +00:00
z3/src/math/lp
Lev Nachmanson edc2715aa8 try fixed int patch period
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2026-02-18 20:58:05 -08:00
..
bound_analyzer_on_row.h
CMakeLists.txt factor out coi, use polynomial elaboration for nlsat solver (#8039) 2026-02-18 20:55:57 -08:00
column.h
column_namer.h
core_solver_pretty_printer.cpp
core_solver_pretty_printer.h remove default destructors 2024-10-02 22:20:12 +01:00
core_solver_pretty_printer_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
cross_nested.h Fix 13 compiler warnings: sign-comparison and unused parameters (#8215) 2026-02-18 20:57:31 -08:00
dense_matrix.cpp
dense_matrix.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
dense_matrix_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
dioph_eq.cpp - When removing a fresh var xt, collect all fresh defs that transitively reference it 2026-02-18 20:57:59 -08:00
dioph_eq.h
emonics.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
emonics.h Migrate codebase to std::string_view (except z3++.h) (#8266) 2026-02-18 20:57:50 -08:00
explanation.h
factorization.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
factorization.h
factorization_factory_imp.cpp remove the line with clang-format off 2023-07-10 12:05:59 -07:00
factorization_factory_imp.h
general_matrix.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
gomory.cpp
gomory.h
hnf.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
hnf_cutter.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
hnf_cutter.h
horner.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
horner.h
implied_bound.h
incremental_vector.h
indexed_value.h delete more default constructors 2024-09-23 12:59:04 +01:00
indexed_vector.cpp
indexed_vector.h fix out of bounds bug 2025-02-11 12:23:00 -10:00
indexed_vector_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
int_branch.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
int_branch.h
int_cube.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
int_cube.h
int_gcd_test.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
int_gcd_test.h
int_solver.cpp try fixed int patch period 2026-02-18 20:58:05 -08:00
int_solver.h
lar_constraints.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
lar_core_solver.cpp
lar_core_solver.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
lar_core_solver_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
lar_solver.cpp [WIP] Find and update std::optional usage in code base (#8272) 2026-02-18 20:57:51 -08:00
lar_solver.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
lar_term.h Remove redundant non-virtual destructors with = default (#8462) 2026-02-18 20:58:01 -08:00
lia_move.h
lp_api.h Replace custom util/optional with std::optional (#8162) 2026-02-18 20:57:09 -08:00
lp_bound_propagator.h
lp_core_solver_base.cpp
lp_core_solver_base.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
lp_core_solver_base_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
lp_params_helper.pyg try fixed int patch period 2026-02-18 20:58:05 -08:00
lp_primal_core_solver.cpp remove the line with clang-format off 2023-07-10 12:05:59 -07:00
lp_primal_core_solver.h Fix implicit conversion warnings: use UINT_MAX instead of -1 for unsi… (#8342) 2026-02-18 20:57:55 -08:00
lp_primal_core_solver_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
lp_primal_core_solver_tableau_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
lp_settings.cpp optionally throttle patch_basic_columns() especially useful in unsat cases 2026-02-18 20:58:05 -08:00
lp_settings.h try fixed int patch period 2026-02-18 20:58:05 -08:00
lp_settings_def.h remove the line with clang-format off 2023-07-10 12:05:59 -07:00
lp_types.h
lp_utils.h [WIP] Find and update std::optional usage in code base (#8272) 2026-02-18 20:57:51 -08:00
matrix.cpp
matrix.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
matrix_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
mon_eq.cpp
monic.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
monomial_bounds.cpp port improvements from ilana branch to master regarding nla 2025-09-19 12:28:31 -07:00
monomial_bounds.h
nex.h
nex_creator.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nex_creator.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nla_basics_lemmas.cpp fix latent bug in factorization 2025-09-23 10:47:24 +03:00
nla_basics_lemmas.h
nla_coi.cpp factor out coi, use polynomial elaboration for nlsat solver (#8039) 2026-02-18 20:55:57 -08:00
nla_coi.h factor out coi, use polynomial elaboration for nlsat solver (#8039) 2026-02-18 20:55:57 -08:00
nla_common.cpp
nla_common.h
nla_core.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nla_core.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
nla_defs.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nla_divisions.cpp
nla_divisions.h
nla_grobner.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nla_grobner.h add option to reduce pseudo-linear monomials 2025-09-04 11:04:12 -07:00
nla_intervals.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nla_intervals.h
nla_monotone_lemmas.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nla_monotone_lemmas.h
nla_order_lemmas.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nla_order_lemmas.h
nla_powers.cpp evaluate unhandled arithmetic operators based on an initialized model #7876 2025-09-14 06:45:36 -07:00
nla_powers.h
nla_pp.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nla_solver.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
nla_solver.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
nla_tangent_lemmas.cpp
nla_tangent_lemmas.h
nla_throttle.cpp
nla_throttle.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
nla_throttle_example.cpp
nla_types.h following the review comments 2025-06-27 19:48:51 -07:00
nra_solver.cpp fix #8099 (again) 2026-02-18 20:57:03 -08:00
nra_solver.h factor out coi, use polynomial elaboration for nlsat solver (#8039) 2026-02-18 20:55:57 -08:00
numeric_pair.h
permutation_matrix.cpp remove the line with clang-format off 2023-07-10 12:05:59 -07:00
permutation_matrix.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
permutation_matrix_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
random_updater.cpp remove the line with clang-format off 2023-07-10 12:05:59 -07:00
random_updater.h u_set replaced by indexed_uint_set (#6841) 2023-08-03 16:01:27 -07:00
random_updater_def.h Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
stacked_vector.h
static_matrix.cpp debug dio 2025-02-11 12:23:00 -10:00
static_matrix.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
static_matrix_def.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
test_bound_analyzer.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
var_eqs.h Remove redundant default constructors when they're the only constructor (#8461) 2026-02-18 20:58:01 -08:00
var_register.h [WIP] Find and update std::optional usage in code base (#8272) 2026-02-18 20:57:51 -08:00