Skip to content

Commit 2517b5a

Browse files
NikolajBjornerNikolajBjorner
committed
port improvements from ilana branch to master regarding nla
Signed-off-by: Nikolaj Bjorner <[email protected]>
1 parent 5d91294 commit 2517b5a

File tree

7 files changed

+73
-61
lines changed

7 files changed

+73
-61
lines changed

‎src/CMakeLists.txt‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -204,27 +204,27 @@ set(Z3_API_HEADERS
204204
)
205205

206206
# Create custom target to copy headers
207-
add_custom_target(z3_headers_copy ALL
208-
COMMENT "Copying Z3 API headers to build include directory"
209-
)
210-
211-
foreach(header_file ${Z3_API_HEADERS})
212-
get_filename_component(header_name "${header_file}" NAME)
213-
set(src_file "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}")
214-
set(dst_file "${Z3_BUILD_INCLUDE_DIR}/${header_name}")
215-
216-
add_custom_command(
217-
TARGET z3_headers_copy POST_BUILD
218-
COMMAND ${CMAKE_COMMAND} -E copy_if_different
219-
"${src_file}"
220-
"${dst_file}"
221-
COMMENT "Copying ${header_name} to include directory"
222-
VERBATIM
223-
)
224-
endforeach()
207+
#add_custom_target(z3_headers_copy ALL
208+
# COMMENT "Copying Z3 API headers to build include directory"
209+
#)
210+
#
211+
#foreach(header_file ${Z3_API_HEADERS})
212+
# get_filename_component(header_name "${header_file}" NAME)
213+
# set(src_file "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}")
214+
# set(dst_file "${Z3_BUILD_INCLUDE_DIR}/${header_name}")
215+
#
216+
# add_custom_command(
217+
# TARGET z3_headers_copy POST_BUILD
218+
# COMMAND ${CMAKE_COMMAND} -E copy_if_different
219+
# "${src_file}"
220+
# "${dst_file}"
221+
# COMMENT "Copying ${header_name} to include directory"
222+
# VERBATIM
223+
# )
224+
#endforeach()
225225

226226
# Make libz3 depend on header copying
227-
add_dependencies(libz3 z3_headers_copy)
227+
#add_dependencies(libz3 z3_headers_copy)
228228

229229
# Update libz3 to also expose the build include directory
230230
target_include_directories(libz3 INTERFACE

‎src/math/lp/cross_nested.h‎

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,17 +19,20 @@
1919
--*/
2020
#pragma once
2121
#include <functional>
22+
#include "util/util.h"
23+
#include "util/rlimit.h"
2224
#include "math/lp/nex.h"
2325
#include "math/lp/nex_creator.h"
2426

2527
namespace nla {
2628
class cross_nested {
2729

2830
// fields
31+
reslimit& m_limit;
2932
nex * m_e = nullptr;
3033
std::function<bool (const nex*)> m_call_on_result;
3134
std::function<bool (unsigned)> m_var_is_fixed;
32-
std::function<unsigned ()> m_random;
35+
random_gen m_random;
3336
bool m_done = false;
3437
ptr_vector<nex> m_b_split_vec;
3538
int m_reported = 0;
@@ -45,11 +48,13 @@ class cross_nested {
4548

4649
cross_nested(std::function<bool (const nex*)> call_on_result,
4750
std::function<bool (unsigned)> var_is_fixed,
48-
std::function<unsigned ()> random,
49-
nex_creator& nex_cr) :
51+
reslimit& limit,
52+
unsigned random_seed,
53+
nex_creator& nex_cr) :
54+
m_limit(limit),
5055
m_call_on_result(call_on_result),
5156
m_var_is_fixed(var_is_fixed),
52-
m_random(random),
57+
m_random(random_seed),
5358
m_done(false),
5459
m_reported(0),
5560
m_mk_scalar([this]{return m_nex_creator.mk_scalar(rational(1));}),
@@ -58,6 +63,7 @@ class cross_nested {
5863

5964

6065
void run(nex *e) {
66+
6167
TRACE(nla_cn, tout << *e << "\n";);
6268
SASSERT(m_nex_creator.is_simplified(*e));
6369
m_e = e;
@@ -279,6 +285,8 @@ class cross_nested {
279285
TRACE(nla_cn, tout << "m_e=" << *m_e << "\nc=" << **c << "\nj = " << nex_creator::ch(j) << "\nfront="; print_front(front, tout) << "\n";);
280286
if (!split_with_var(*c, j, front))
281287
return;
288+
if (!m_limit.inc())
289+
return;
282290
TRACE(nla_cn, tout << "after split c=" << **c << "\nfront="; print_front(front, tout) << "\n";);
283291
if (front.empty()) {
284292
#ifdef Z3DEBUG

‎src/math/lp/horner.cpp‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,9 @@ bool horner::lemmas_on_row(const T& row) {
9090
cross_nested cn(
9191
[this, dep](const nex* n) { return c().m_intervals.check_nex(n, dep); },
9292
[this](unsigned j) { return c().var_is_fixed(j); },
93-
[this]() { return c().random(); }, m_nex_creator);
93+
c().reslim(),
94+
c().random(),
95+
m_nex_creator);
9496
bool ret = lemmas_on_expr(cn, to_sum(e));
9597
c().m_intervals.get_dep_intervals().reset(); // clean the memory allocated by the interval bound dependencies
9698
return ret;

‎src/math/lp/lp_settings.cpp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,4 +43,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
4343
m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums();
4444
m_dio_calls_period = lp_p.dio_calls_period();
4545
m_dio_run_gcd = lp_p.dio_run_gcd();
46+
m_max_conflicts = p.max_conflicts();
4647
}

‎src/math/lp/lp_settings.h‎

Lines changed: 32 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,7 @@ struct statistics {
103103
unsigned m_make_feasible = 0;
104104
unsigned m_total_iterations = 0;
105105
unsigned m_iters_with_no_cost_growing = 0;
106+
unsigned m_num_factorizations = 0;
106107
unsigned m_num_of_implied_bounds = 0;
107108
unsigned m_need_to_solve_inf = 0;
108109
unsigned m_max_cols = 0;
@@ -136,47 +137,45 @@ struct statistics {
136137
unsigned m_bounds_tightening_conflicts = 0;
137138
unsigned m_bounds_tightenings = 0;
138139
unsigned m_nla_throttled_lemmas = 0;
139-
unsigned m_nla_bounds_lemmas = 0;
140-
unsigned m_nla_bounds_propagations = 0;
140+
141141
::statistics m_st = {};
142142

143143
void reset() {
144144
*this = statistics{};
145145
}
146146
void collect_statistics(::statistics& st) const {
147-
st.update("arith-lp-make-feasible", m_make_feasible);
148-
st.update("arith-lp-max-columns", m_max_cols);
149-
st.update("arith-lp-max-rows", m_max_rows);
150-
st.update("arith-lp-offset-eqs", m_offset_eqs);
151-
st.update("arith-lp-fixed-eqs", m_fixed_eqs);
152-
st.update("arith-lia-patches", m_patches);
153-
st.update("arith-lia-patches-success", m_patches_success);
154-
st.update("arith-lia-gcd-calls", m_gcd_calls);
155-
st.update("arith-lia-gcd-conflict", m_gcd_conflicts);
156-
st.update("arith-lia-cube-calls", m_cube_calls);
157-
st.update("arith-lia-cube-success", m_cube_success);
158-
st.update("arith-lia-hermite-calls", m_hnf_cutter_calls);
159-
st.update("arith-lia-hermite-cuts", m_hnf_cuts);
160-
st.update("arith-lia-gomory-cuts", m_gomory_cuts);
161-
st.update("arith-lia-diophantine-calls", m_dio_calls);
162-
st.update("arith-lia-diophantine-tighten-conflicts", m_dio_tighten_conflicts);
163-
st.update("arith-lia-diophantine-rewrite-conflicts", m_dio_rewrite_conflicts);
164-
st.update("arith-lia-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
165-
st.update("arith-lia-bounds-tightenings", m_bounds_tightenings);
166-
st.update("arith-nla-horner-calls", m_horner_calls);
167-
st.update("arith-nla-horner-conflicts", m_horner_conflicts);
168-
st.update("arith-nla-horner-cross-nested-forms", m_cross_nested_forms);
169-
st.update("arith-nla-grobner-calls", m_grobner_calls);
170-
st.update("arith-nla-grobner-conflicts", m_grobner_conflicts);
147+
st.update("arith-factorizations", m_num_factorizations);
148+
st.update("arith-make-feasible", m_make_feasible);
149+
st.update("arith-max-columns", m_max_cols);
150+
st.update("arith-max-rows", m_max_rows);
151+
st.update("arith-gcd-calls", m_gcd_calls);
152+
st.update("arith-gcd-conflict", m_gcd_conflicts);
153+
st.update("arith-cube-calls", m_cube_calls);
154+
st.update("arith-cube-success", m_cube_success);
155+
st.update("arith-patches", m_patches);
156+
st.update("arith-patches-success", m_patches_success);
157+
st.update("arith-hnf-calls", m_hnf_cutter_calls);
158+
st.update("arith-hnf-cuts", m_hnf_cuts);
159+
st.update("arith-gomory-cuts", m_gomory_cuts);
160+
st.update("arith-horner-calls", m_horner_calls);
161+
st.update("arith-horner-conflicts", m_horner_conflicts);
162+
st.update("arith-horner-cross-nested-forms", m_cross_nested_forms);
163+
st.update("arith-grobner-calls", m_grobner_calls);
164+
st.update("arith-grobner-conflicts", m_grobner_conflicts);
165+
st.update("arith-offset-eqs", m_offset_eqs);
166+
st.update("arith-fixed-eqs", m_fixed_eqs);
171167
st.update("arith-nla-add-bounds", m_nla_add_bounds);
172168
st.update("arith-nla-propagate-bounds", m_nla_propagate_bounds);
173169
st.update("arith-nla-propagate-eq", m_nla_propagate_eq);
174170
st.update("arith-nla-lemmas", m_nla_lemmas);
175-
st.update("arith-nla-nra-calls", m_nra_calls);
176-
st.update("arith-nla-bounds-improvements", m_nla_bounds_improvements);
171+
st.update("arith-nra-calls", m_nra_calls);
172+
st.update("arith-bounds-improvements", m_nla_bounds_improvements);
173+
st.update("arith-dio-calls", m_dio_calls);
174+
st.update("arith-dio-tighten-conflicts", m_dio_tighten_conflicts);
175+
st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts);
176+
st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
177+
st.update("arith-bounds-tightenings", m_bounds_tightenings);
177178
st.update("arith-nla-throttled-lemmas", m_nla_throttled_lemmas);
178-
st.update("arith-nla-bounds-lemmas", m_nla_bounds_lemmas);
179-
st.update("artih-nla-bounds-propagations", m_nla_bounds_propagations);
180179
st.copy(m_st);
181180
}
182181
};
@@ -223,11 +222,13 @@ struct lp_settings {
223222
unsigned percent_of_entering_to_check = 5; // we try to find a profitable column in a percentage of the columns
224223
bool use_scaling = true;
225224
unsigned max_number_of_iterations_with_no_improvements = 2000000;
226-
double time_limit; // the maximum time limit of the total run time in seconds
225+
double time_limit; // the maximum time limit of the total run time in seconds
227226
// end of dual section
228227
bool m_bound_propagation = true;
229228
bool presolve_with_double_solver_for_lar = true;
230229
simplex_strategy_enum m_simplex_strategy;
230+
231+
unsigned m_max_conflicts = 0;
231232

232233
int report_frequency = 1000;
233234
bool print_statistics = false;

‎src/math/lp/monomial_bounds.cpp‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -378,7 +378,6 @@ namespace nla {
378378
bool monomial_bounds::add_lemma() {
379379
if (c().lra.get_status() != lp::lp_status::INFEASIBLE)
380380
return false;
381-
c().lp_settings().stats().m_nla_bounds_lemmas++;
382381
lp::explanation exp;
383382
c().lra.get_infeasibility_explanation(exp);
384383
lemma_builder lemma(c(), "propagate fixed - infeasible lra");
@@ -423,7 +422,6 @@ namespace nla {
423422
TRACE(nla_solver, tout << "propagate fixed " << m << " = 0, fixed_to_zero = " << fixed_to_zero << "\n";);
424423
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, rational(0), dep);
425424

426-
c().lp_settings().stats().m_nla_bounds_propagations++;
427425
// propagate fixed equality
428426
auto exp = get_explanation(dep);
429427
c().add_fixed_equality(m.var(), rational(0), exp);
@@ -433,7 +431,7 @@ namespace nla {
433431
auto* dep = explain_fixed(m, k);
434432
TRACE(nla_solver, tout << "propagate fixed " << m << " = " << k << "\n";);
435433
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
436-
c().lp_settings().stats().m_nla_bounds_propagations++;
434+
437435
// propagate fixed equality
438436
auto exp = get_explanation(dep);
439437
c().add_fixed_equality(m.var(), k, exp);
@@ -450,7 +448,6 @@ namespace nla {
450448

451449
if (k == 1) {
452450
lp::explanation exp = get_explanation(dep);
453-
c().lp_settings().stats().m_nla_bounds_propagations++;
454451
c().add_equality(m.var(), w, exp);
455452
}
456453
}

‎src/math/lp/nla_core.cpp‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
3939
m_grobner(this),
4040
m_emons(m_evars),
4141
m_use_nra_model(false),
42-
m_nra(s, m_nra_lim, *this),
42+
m_nra(s, m_nra_lim, *this, p),
4343
m_throttle(lra.trail(),
4444
lra.settings().stats()) {
4545
m_nlsat_delay_bound = lp_settings().nlsat_delay();
@@ -1366,6 +1366,9 @@ lbool core::check() {
13661366
if (no_effect() && params().arith_nl_nra()) {
13671367
scoped_limits sl(m_reslim);
13681368
sl.push_child(&m_nra_lim);
1369+
params_ref p;
1370+
p.set_uint("max_conflicts", lp_settings().m_max_conflicts);
1371+
m_nra.updt_params(p);
13691372
ret = m_nra.check();
13701373
lp_settings().stats().m_nra_calls++;
13711374
}
@@ -1400,7 +1403,7 @@ lbool core::bounded_nlsat() {
14001403
scoped_rlimit sr(m_nra_lim, 100000);
14011404
ret = m_nra.check();
14021405
}
1403-
p.set_uint("max_conflicts", UINT_MAX);
1406+
p.set_uint("max_conflicts", lp_settings().m_max_conflicts);
14041407
m_nra.updt_params(p);
14051408
lp_settings().stats().m_nra_calls++;
14061409
if (ret == l_undef)

0 commit comments

Comments
 (0)