3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-22 08:30:28 +00:00
Commit graph

32 commits

Author SHA1 Message Date
Lev Nachmanson
c37ab9b6a3 lp: rename cut_period->int_hammer_period, random_period->random_hammers
These knobs govern the integer cut/cube heuristics (the "hammers":
find_cube, lcube, hnf, gomory, dio), not just cuts, so the names now
reflect that. lp.int_hammer_period sets the shared firing period and
lp.random_hammers toggles random vs deterministic gating.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-19 07:47:24 -07:00
Lev Nachmanson
17de82a963 lp: rename cut_period_random to random_period
The toggle also gates the cube heuristics (find_cube, lcube), not just
cuts, so 'cut' in the name was misleading. random_period covers all the
periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-19 07:43:36 -07:00
Lev Nachmanson
74899eeb93 lp: rename random_cut_period to cut_period_random
Rename the toggle so it sits beside lp.cut_period and reads as a
modifier on it (cut_period + random) rather than burying "cut" in the
middle of the name.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-19 07:42:04 -07:00
Lev Nachmanson
30dc804d25 lp: add lp.random_cut_period to toggle randomized cut/cube gates
Introduce the boolean lp.random_cut_period parameter (default true).
When enabled, the periodic integer heuristic gates (find_cube, lcube,
hnf, gomory, dio) fire at random with the same 1/period expected rate;
when disabled they fall back to the deterministic every-k-th-call
modulus on m_number_of_calls. The shared hit_period() helper centralizes
this decision, and m_number_of_calls is restored for the deterministic
path.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-19 07:38:06 -07:00
Lev Nachmanson
35fea6f4d3 lp: expose integer cut/cube period as lp.cut_period parameter
The find_cube, hnf and gomory integer heuristics were all throttled by a
hardcoded period of 4 (m_int_find_cube_period, m_hnf_cut_period,
m_int_gomory_cut_period). Make this value tunable through the new
lp.cut_period parameter (default 4, preserving current behavior) so the
period can be swept (e.g. 3/4/5) for benchmarking. A value of 0 is clamped
to 1.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-18 12:23:10 -07:00
Lev Nachmanson
f508854fe5
Lcube (#9858)
Implemented the largest cube heuristic from Bromberger and Weidenbach's
paper on cubes. Also fixes an overflow bug in mzp.
Use vswhere to find the visual studio version on windows in the build's ymls.
---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-14 16:25:21 -07:00
Lev Nachmanson
f5b8dfc2f1 Revert "optionally throttle patch_basic_columns() especially useful in unsat cases"
This reverts commit bee2b45743.
2026-02-07 10:45:15 -10:00
Lev Nachmanson
bee2b45743 optionally throttle patch_basic_columns() especially useful in unsat cases
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2026-02-06 10:14:39 -10:00
Nikolaj Bjorner
2517b5a40a port improvements from ilana branch to master regarding nla
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-19 12:28:31 -07:00
Nikolaj Bjorner
c75b8ec752 add option to control epsilon #7791
#7791 reports on using model values during lex optimization that break soft constraints.
This is an artifact of using optimization where optimal values can be arbitrarily close to a rational.
In a way it is by design, but we give the user now an option to control the starting point for epsilon when converting infinitesimals into rationals.
2025-08-17 16:51:00 -07:00
Nikolaj Bjorner
c387b20ac6 move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
Lev Nachmanson
a1673f2bdd fallback to Gomory cuts and gcd conflicts if dio fails
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-21 17:10:32 -07:00
Lev Nachmanson
17af18fe31 make gcd call in dio optional
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
59edb81f86 Update lp_settings.cpp
white space change
2025-04-18 18:24:50 -07:00
Lev Nachmanson
8db9f52386 add parameter m_dio_calls_period
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
972f80188a throttle dio for big numbers
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
3e49d9fcfe reuse dio branch
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
a62d664ae4 testing! disable gomory cut in int_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
6f7b749ff9 improved dio handler
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
e920291393 fixing the default parameters of dio and rename m_gomory_cuts to m_cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-11 12:23:00 -10:00
Lev Nachmanson
134bed826a throttle the branching in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-11 12:23:00 -10:00
Lev Nachmanson
a19e10912f make dio less aggressive, allow other cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-11 12:23:00 -10:00
Lev Nachmanson
2ebb957cc8 enable cuts from proofs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-11 12:23:00 -10:00
Lev Nachmanson
097a25ebfe add parameter to control calling diophantine equations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-11 12:23:00 -10:00
Lev Nachmanson
2934618c50 remove simplify_inequality from gomory.cpp 2024-01-04 11:40:57 -10:00
Lev Nachmanson
0728b81e9e add parameter lp_settings.m_gomory_simplify 2023-12-28 06:00:57 -10:00
Lev Nachmanson
e091a2e775 remove the line with clang-format off 2023-07-10 12:05:59 -07:00
Lev Nachmanson
5ed2a82893
set clang format off for lp files (#6795)
* adding // clang-format off

* set clang-format off at the beginning of  lp files

* set clang-format off

* remove dead code
2023-07-03 17:35:16 -07:00
Lev Nachmanson
f351eb3ab2 remove many methods dealing with double
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-03-08 10:27:05 -08:00
Nikolaj Bjorner
87d4ce2659 working on #5614
there are some different sources for the performance regression illustrated by the example. The mitigations will be enabled separately:
- m_bv_to_propagate is too expensive
- lp_bound_propagator misses equalities in two different ways:
   - it resets row checks after backtracking even though they could still propagate
   - it misses equalities for fixed rows when the fixed constant value does not correspond to a fixed variable.

FYI @levnach
2021-11-02 14:55:39 -07:00
Nikolaj Bjorner
8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Lev Nachmanson
33cbd29ed0 mv util/lp to math/lp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Renamed from src/util/lp/lp_settings.cpp (Browse further)