mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

add parameter incremental to ensure preprocessing does not interefere with adding constraints during search

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-07-05 08:09:49 -07:00
parent 2cf0c8173b
commit ac822acb0f
3 changed files with 14 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/opt/opt_context.cpp
View file

@ -137,9 +137,6 @@ namespace opt {
m_model_fixed(), m_model_fixed(),
m_objective_refs(m), m_objective_refs(m),
m_core(m), m_core(m),
m_enable_sat(false),
m_is_clausal(false),
m_pp_neat(false),
m_unknown("unknown") m_unknown("unknown")
{ {
params_ref p; params_ref p;
@ -196,6 +193,8 @@ namespace opt {
void context::add_hard_constraint(expr* f) { void context::add_hard_constraint(expr* f) {
if (m_calling_on_model) { 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); get_solver().assert_expr(f);
for (auto const& [k, v] : m_maxsmts) for (auto const& [k, v] : m_maxsmts)
v->reset_upper(); v->reset_upper();
@ -838,19 +837,14 @@ namespace opt {
} }
goal_ref g(alloc(goal, m, true, !asms.empty())); goal_ref g(alloc(goal, m, true, !asms.empty()));
for (expr* fml : fmls) { for (expr* fml : fmls)
g->assert_expr(fml); g->assert_expr(fml);
} for (expr * a : asms)
for (expr * a : asms) {
g->assert_expr(a, a); g->assert_expr(a, a);
}
tactic_ref tac0 = tactic_ref tac0 =
and_then(mk_simplify_tactic(m, m_params), and_then(mk_simplify_tactic(m, m_params),
mk_propagate_values_tactic(m), mk_propagate_values_tactic(m),
mk_solve_eqs_tactic(m), m_incremental ? mk_skip_tactic() : 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
mk_simplify_tactic(m)); mk_simplify_tactic(m));
opt_params optp(m_params); opt_params optp(m_params);
tactic_ref tac1, tac2, tac3, tac4; tactic_ref tac1, tac2, tac3, tac4;
@ -861,7 +855,7 @@ namespace opt {
m.linearize(core, deps); m.linearize(core, deps);
has_dep |= !deps.empty(); 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); tac1 = mk_dt2bv_tactic(m);
tac2 = mk_lia2card_tactic(m); tac2 = mk_lia2card_tactic(m);
tac3 = mk_eq2bv_tactic(m); tac3 = mk_eq2bv_tactic(m);
@ -1568,6 +1562,7 @@ namespace opt {
m_maxsat_engine = _p.maxsat_engine(); m_maxsat_engine = _p.maxsat_engine();
m_pp_neat = _p.pp_neat(); m_pp_neat = _p.pp_neat();
m_pp_wcnf = _p.pp_wcnf(); m_pp_wcnf = _p.pp_wcnf();
m_incremental = _p.incremental();
} }
std::string context::to_string() { std::string context::to_string() {

11
src/opt/opt_context.h
View file

@ -194,11 +194,12 @@ namespace opt {
func_decl_ref_vector m_objective_refs; func_decl_ref_vector m_objective_refs;
expr_ref_vector m_core; expr_ref_vector m_core;
tactic_ref m_simplify; tactic_ref m_simplify;
bool m_enable_sat { true } ; bool m_enable_sat = true;
bool m_enable_sls { false }; bool m_enable_sls = false;
bool m_is_clausal { false }; bool m_is_clausal = false;
bool m_pp_neat { true }; bool m_pp_neat = false;
bool m_pp_wcnf { false }; bool m_pp_wcnf = false;
bool m_incremental = false;
symbol m_maxsat_engine; symbol m_maxsat_engine;
symbol m_logic; symbol m_logic;
svector<symbol> m_labels; svector<symbol> m_labels;

1
src/opt/opt_params.pyg
View file

@ -15,6 +15,7 @@ def_module_params('opt',
('enable_core_rotate', BOOL, False, 'enable core rotation to both sample cores and correction sets'), ('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'), ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
('elim_01', BOOL, True, 'eliminate 01 variables'), ('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'), ('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)'), ('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'), ('pp.wcnf', BOOL, False, 'print maxsat benchmark into wcnf format'),