From ac822acb0f8bb6d5d1aabf10e1ca70fbd0bc622e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Jul 2022 08:09:49 -0700 Subject: [PATCH] add parameter incremental to ensure preprocessing does not interefere with adding constraints during search Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 19 +++++++------------ src/opt/opt_context.h | 11 ++++++----- src/opt/opt_params.pyg | 1 + 3 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index fa2903c35..8c4ec6ed9 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -137,9 +137,6 @@ namespace opt { m_model_fixed(), m_objective_refs(m), m_core(m), - m_enable_sat(false), - m_is_clausal(false), - m_pp_neat(false), m_unknown("unknown") { params_ref p; @@ -196,6 +193,8 @@ namespace opt { void context::add_hard_constraint(expr* f) { if (m_calling_on_model) { + if (!m_incremental) + throw default_exception("Set opt.incremental = true to allow adding constraints during search"); get_solver().assert_expr(f); for (auto const& [k, v] : m_maxsmts) v->reset_upper(); @@ -838,19 +837,14 @@ namespace opt { } goal_ref g(alloc(goal, m, true, !asms.empty())); - for (expr* fml : fmls) { + for (expr* fml : fmls) g->assert_expr(fml); - } - for (expr * a : asms) { + for (expr * a : asms) g->assert_expr(a, a); - } tactic_ref tac0 = and_then(mk_simplify_tactic(m, m_params), mk_propagate_values_tactic(m), - mk_solve_eqs_tactic(m), - // NB: cannot ackermannize because max/min objectives would disappear - // mk_ackermannize_bv_tactic(m, m_params), - // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints + m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m), mk_simplify_tactic(m)); opt_params optp(m_params); tactic_ref tac1, tac2, tac3, tac4; @@ -861,7 +855,7 @@ namespace opt { m.linearize(core, deps); has_dep |= !deps.empty(); } - if (optp.elim_01() && m_logic.is_null() && !has_dep) { + if (optp.elim_01() && m_logic.is_null() && !has_dep && !m_incremental) { tac1 = mk_dt2bv_tactic(m); tac2 = mk_lia2card_tactic(m); tac3 = mk_eq2bv_tactic(m); @@ -1568,6 +1562,7 @@ namespace opt { m_maxsat_engine = _p.maxsat_engine(); m_pp_neat = _p.pp_neat(); m_pp_wcnf = _p.pp_wcnf(); + m_incremental = _p.incremental(); } std::string context::to_string() { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index c02689a38..49cc6adcd 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -194,11 +194,12 @@ namespace opt { func_decl_ref_vector m_objective_refs; expr_ref_vector m_core; tactic_ref m_simplify; - bool m_enable_sat { true } ; - bool m_enable_sls { false }; - bool m_is_clausal { false }; - bool m_pp_neat { true }; - bool m_pp_wcnf { false }; + bool m_enable_sat = true; + bool m_enable_sls = false; + bool m_is_clausal = false; + bool m_pp_neat = false; + bool m_pp_wcnf = false; + bool m_incremental = false; symbol m_maxsat_engine; symbol m_logic; svector m_labels; diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index df3ab0925..893b4bfd6 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -15,6 +15,7 @@ def_module_params('opt', ('enable_core_rotate', BOOL, False, 'enable core rotation to both sample cores and correction sets'), ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), + ('incremental', BOOL, False, 'set incremental mode. It disables pre-processing and enables adding constraints in model event handler'), ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'), ('pp.wcnf', BOOL, False, 'print maxsat benchmark into wcnf format'),