mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
tuning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f1c8754527
commit
3ef05ced2f
|
@ -1,11 +1,12 @@
|
|||
def_module_params('lp',
|
||||
export=True,
|
||||
description='Parameters for the LP arithmetic solver core',
|
||||
params=(
|
||||
('rep_freq', UINT, 0, 'the report frequency, in how many iterations print the cost and other info '),
|
||||
('min', BOOL, False, 'minimize cost'),
|
||||
('print_stats', BOOL, False, 'print statistic'),
|
||||
('simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
|
||||
('enable_hnf', BOOL, True, 'enable hnf cuts'),
|
||||
('enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'),
|
||||
('bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'),
|
||||
('nla', BOOL, False, 'call nonlinear integer solver with incremental linearization'),
|
||||
('print_ext_var_names', BOOL, False, 'print external variable names')
|
||||
|
|
|
@ -1,5 +1,6 @@
|
|||
def_module_params('nla',
|
||||
export=True,
|
||||
description='Parameters for non-linear arithmetic solving',
|
||||
params=(
|
||||
('order', BOOL, True, 'run order lemmas'),
|
||||
('tangents', BOOL, True, 'run tangent lemmas'),
|
||||
|
|
|
@ -455,7 +455,8 @@ void asserted_formulas::propagate_values() {
|
|||
|
||||
unsigned num_prop = 0;
|
||||
unsigned num_iterations = 0;
|
||||
while (!inconsistent() && ++num_iterations < 2) {
|
||||
unsigned delta_prop = m_formulas.size();
|
||||
while (!inconsistent() && m_formulas.size()/20 < delta_prop) {
|
||||
m_expr2depth.reset();
|
||||
m_scoped_substitution.push();
|
||||
unsigned prop = num_prop;
|
||||
|
@ -478,9 +479,7 @@ void asserted_formulas::propagate_values() {
|
|||
m_scoped_substitution.pop(1);
|
||||
flush_cache();
|
||||
TRACE("propagate_values", tout << "after:\n"; display(tout););
|
||||
if (num_prop == prop) {
|
||||
break;
|
||||
}
|
||||
delta_prop = prop - num_prop;
|
||||
num_prop = prop;
|
||||
}
|
||||
TRACE("asserted_formulas", tout << num_prop << "\n";);
|
||||
|
@ -493,7 +492,6 @@ unsigned asserted_formulas::propagate_values(unsigned i) {
|
|||
expr_ref new_n(m);
|
||||
proof_ref new_pr(m);
|
||||
m_rewriter(n, new_n, new_pr);
|
||||
TRACE("propagate_values", tout << n << "\n" << new_n << "\n";);
|
||||
if (m.proofs_enabled()) {
|
||||
proof * pr = m_formulas[i].get_proof();
|
||||
new_pr = m.mk_modus_ponens(pr, new_pr);
|
||||
|
@ -504,7 +502,7 @@ unsigned asserted_formulas::propagate_values(unsigned i) {
|
|||
m_inconsistent = true;
|
||||
}
|
||||
update_substitution(new_n, new_pr);
|
||||
return n != new_n ? 1 : 0;
|
||||
return (n != new_n) ? 1 : 0;
|
||||
}
|
||||
|
||||
bool asserted_formulas::update_substitution(expr* n, proof* pr) {
|
||||
|
|
|
@ -1387,7 +1387,7 @@ namespace smt {
|
|||
else if (d.is_theory_atom()) {
|
||||
theory * th = m_theories.get_plugin(d.get_theory());
|
||||
SASSERT(th);
|
||||
th->assign_eh(v, val == l_true);
|
||||
th->assign_eh(v, val == l_true);
|
||||
}
|
||||
else if (d.is_quantifier()) {
|
||||
// Remark: when RELEVANCY_LEMMA is true, a quantifier can be asserted to false and marked as relevant.
|
||||
|
@ -1804,7 +1804,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
bool_var var;
|
||||
lbool phase;
|
||||
lbool phase = l_undef;
|
||||
m_case_split_queue->next_case_split(var, phase);
|
||||
|
||||
if (var == null_bool_var) {
|
||||
|
@ -1836,13 +1836,13 @@ namespace smt {
|
|||
// assigning a quantifier to false is equivalent to make it irrelevant.
|
||||
phase = l_false;
|
||||
}
|
||||
literal l(var, false);
|
||||
|
||||
if (phase != l_undef) {
|
||||
is_pos = phase == l_true;
|
||||
}
|
||||
else {
|
||||
bool_var_data & d = m_bdata[var];
|
||||
|
||||
if (d.try_true_first()) {
|
||||
is_pos = true;
|
||||
}
|
||||
|
@ -1851,21 +1851,25 @@ namespace smt {
|
|||
case PS_THEORY:
|
||||
if (m_phase_cache_on && d.m_phase_available) {
|
||||
is_pos = m_bdata[var].m_phase;
|
||||
break;
|
||||
}
|
||||
else if (!m_phase_cache_on && d.is_theory_atom()) {
|
||||
if (!m_phase_cache_on && d.is_theory_atom()) {
|
||||
theory * th = m_theories.get_plugin(d.get_theory());
|
||||
lbool ph = th->get_phase(var);
|
||||
if (ph != l_undef) {
|
||||
is_pos = ph == l_true;
|
||||
}
|
||||
else {
|
||||
is_pos = m_phase_default;
|
||||
lbool th_phase = th->get_phase(var);
|
||||
if (th_phase != l_undef) {
|
||||
is_pos = th_phase == l_true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
else {
|
||||
TRACE("phase_selection", tout << "setting to false\n";);
|
||||
is_pos = m_phase_default;
|
||||
if (m_lit_occs[l.index()] == 0) {
|
||||
is_pos = false;
|
||||
break;
|
||||
}
|
||||
if (m_lit_occs[(~l).index()] == 0) {
|
||||
is_pos = true;
|
||||
break;
|
||||
}
|
||||
is_pos = m_phase_default;
|
||||
break;
|
||||
case PS_CACHING:
|
||||
case PS_CACHING_CONSERVATIVE:
|
||||
|
@ -1889,8 +1893,7 @@ namespace smt {
|
|||
is_pos = (m_random() % 2 == 0);
|
||||
break;
|
||||
case PS_OCCURRENCE: {
|
||||
literal l(var);
|
||||
is_pos = m_lit_occs[l.index()].size() > m_lit_occs[(~l).index()].size();
|
||||
is_pos = m_lit_occs[l.index()] > m_lit_occs[(~l).index()];
|
||||
break;
|
||||
}
|
||||
default:
|
||||
|
@ -1900,10 +1903,9 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
TRACE("decide", tout << "case split " << (is_pos?"pos":"neg") << " p" << var << "\n"
|
||||
<< "activity: " << get_activity(var) << "\n";);
|
||||
|
||||
assign(literal(var, !is_pos), b_justification::mk_axiom(), true);
|
||||
if (!is_pos) l.neg();
|
||||
TRACE("decide", tout << "case split " << l << "\n" << "activity: " << get_activity(var) << "\n";);
|
||||
assign(l, b_justification::mk_axiom(), true);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -1989,19 +1991,18 @@ namespace smt {
|
|||
/**
|
||||
\brief Update the index used for backward subsumption.
|
||||
*/
|
||||
void context::remove_lit_occs(clause * cls) {
|
||||
unsigned num_lits = cls->get_num_literals();
|
||||
for (unsigned i = 0; i < num_lits; i++) {
|
||||
literal l = cls->get_literal(i);
|
||||
m_lit_occs[l.index()].erase(cls);
|
||||
void context::remove_lit_occs(clause const& cls) {
|
||||
int nbv = get_num_bool_vars();
|
||||
for (literal l : cls) {
|
||||
if (l.var() < nbv)
|
||||
dec_ref(l);
|
||||
}
|
||||
}
|
||||
|
||||
void context::remove_cls_occs(clause * cls) {
|
||||
remove_watch_literal(cls, 0);
|
||||
remove_watch_literal(cls, 1);
|
||||
if (lit_occs_enabled())
|
||||
remove_lit_occs(cls);
|
||||
remove_lit_occs(*cls);
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -2254,19 +2255,9 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
unsigned num = cls->get_num_literals();
|
||||
unsigned num = cls->get_num_literals();
|
||||
|
||||
if (lit_occs_enabled()) {
|
||||
for (unsigned j = 0; j < num; j++) {
|
||||
literal l = cls->get_literal(j);
|
||||
if (l.var() < static_cast<int>(num_bool_vars)) {
|
||||
// This boolean variable was not deleted during backtracking
|
||||
//
|
||||
// So, remove it from lit_occs.
|
||||
m_lit_occs[l.index()].erase(cls);
|
||||
}
|
||||
}
|
||||
}
|
||||
remove_lit_occs(*cls);
|
||||
|
||||
unsigned ilvl = 0;
|
||||
(void)ilvl;
|
||||
|
@ -2297,8 +2288,7 @@ namespace smt {
|
|||
add_watch_literal(cls, 0);
|
||||
add_watch_literal(cls, 1);
|
||||
|
||||
if (lit_occs_enabled())
|
||||
add_lit_occs(cls);
|
||||
add_lit_occs(*cls);
|
||||
|
||||
literal l1 = cls->get_literal(0);
|
||||
literal l2 = cls->get_literal(1);
|
||||
|
@ -2342,7 +2332,6 @@ namespace smt {
|
|||
v.reset();
|
||||
}
|
||||
CASSERT("reinit_clauses", check_clauses(m_lemmas));
|
||||
CASSERT("reinit_clauses", check_lit_occs());
|
||||
TRACE("reinit_clauses_bug", display_watch_lists(tout););
|
||||
}
|
||||
|
||||
|
@ -2498,23 +2487,24 @@ namespace smt {
|
|||
|
||||
unsigned i = 2;
|
||||
unsigned j = i;
|
||||
bool is_taut = false;
|
||||
for(; i < s; i++) {
|
||||
literal l = cls[i];
|
||||
switch(get_assignment(l)) {
|
||||
case l_false:
|
||||
if (m.proofs_enabled())
|
||||
simp_lits.push_back(~l);
|
||||
if (lit_occs_enabled())
|
||||
m_lit_occs[l.index()].erase(&cls);
|
||||
dec_ref(l);
|
||||
break;
|
||||
case l_true:
|
||||
is_taut = true;
|
||||
// fallthrough
|
||||
case l_undef:
|
||||
if (i != j) {
|
||||
cls.swap_lits(i, j);
|
||||
}
|
||||
j++;
|
||||
break;
|
||||
case l_true:
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -2524,6 +2514,10 @@ namespace smt {
|
|||
SASSERT(j >= 2);
|
||||
}
|
||||
|
||||
if (is_taut) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if (m.proofs_enabled() && !simp_lits.empty()) {
|
||||
SASSERT(m_scope_lvl == m_base_lvl);
|
||||
justification * js = cls.get_justification();
|
||||
|
|
|
@ -170,7 +170,7 @@ namespace smt {
|
|||
ptr_vector<expr> m_bool_var2expr; // bool_var -> expr
|
||||
signed_char_vector m_assignment; //!< mapping literal id -> assignment lbool
|
||||
vector<watch_list> m_watches; //!< per literal
|
||||
vector<clause_set> m_lit_occs; //!< index for backward subsumption
|
||||
unsigned_vector m_lit_occs; //!< occurrence count of literals
|
||||
svector<bool_var_data> m_bdata; //!< mapping bool_var -> data
|
||||
svector<double> m_activity;
|
||||
clause_vector m_aux_clauses;
|
||||
|
@ -637,8 +637,6 @@ namespace smt {
|
|||
|
||||
void remove_watch_literal(clause * cls, unsigned idx);
|
||||
|
||||
void remove_lit_occs(clause * cls);
|
||||
|
||||
void remove_cls_occs(clause * cls);
|
||||
|
||||
void del_clause(bool log, clause * cls);
|
||||
|
@ -841,9 +839,13 @@ namespace smt {
|
|||
|
||||
void mk_ite_cnstr(app * n);
|
||||
|
||||
bool lit_occs_enabled() const { return m_fparams.m_phase_selection==PS_OCCURRENCE; }
|
||||
void dec_ref(literal l) { SASSERT(m_lit_occs[l.index()] > 0); m_lit_occs[l.index()]--; }
|
||||
|
||||
void add_lit_occs(clause * cls);
|
||||
void inc_ref(literal l) { m_lit_occs[l.index()]++; }
|
||||
|
||||
void remove_lit_occs(clause const& cls);
|
||||
|
||||
void add_lit_occs(clause const& cls);
|
||||
public:
|
||||
|
||||
void ensure_internalized(expr* e);
|
||||
|
@ -1423,9 +1425,6 @@ namespace smt {
|
|||
|
||||
bool check_missing_diseq_conflict() const;
|
||||
|
||||
bool check_lit_occs(literal l) const;
|
||||
|
||||
bool check_lit_occs() const;
|
||||
#endif
|
||||
// -----------------------------------
|
||||
//
|
||||
|
@ -1571,6 +1570,8 @@ namespace smt {
|
|||
|
||||
void get_guessed_literals(expr_ref_vector & result);
|
||||
|
||||
bool split_binary(app* o, expr*& a, expr_ref& b, expr_ref& c);
|
||||
|
||||
void internalize_assertion(expr * n, proof * pr, unsigned generation);
|
||||
|
||||
void internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy);
|
||||
|
|
|
@ -32,10 +32,8 @@ namespace smt {
|
|||
bool context::check_clause(clause const * cls) const {
|
||||
SASSERT(is_watching_clause(~cls->get_literal(0), cls));
|
||||
SASSERT(is_watching_clause(~cls->get_literal(1), cls));
|
||||
if (lit_occs_enabled()) {
|
||||
for (literal l : *cls) {
|
||||
SASSERT(m_lit_occs[l.index()].contains(const_cast<clause*>(cls)));
|
||||
}
|
||||
for (literal l : *cls) {
|
||||
SASSERT(m_lit_occs[l.index()] > 0);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
@ -84,37 +82,6 @@ namespace smt {
|
|||
return true;
|
||||
}
|
||||
|
||||
bool context::check_lit_occs(literal l) const {
|
||||
clause_set const & v = m_lit_occs[l.index()];
|
||||
for (clause * cls : v) {
|
||||
unsigned num = cls->get_num_literals();
|
||||
unsigned i = 0;
|
||||
for (; i < num; i++)
|
||||
if (cls->get_literal(i) == l)
|
||||
break;
|
||||
CTRACE("lit_occs", !(i < num), tout << i << " " << num << "\n"; display_literal(tout, l); tout << "\n";
|
||||
display_clause(tout, cls); tout << "\n";
|
||||
tout << "l: " << l.index() << " cls: ";
|
||||
for (unsigned j = 0; j < num; j++) {
|
||||
tout << cls->get_literal(j).index() << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
display_clause_detail(tout, cls); tout << "\n";);
|
||||
SASSERT(i < num);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool context::check_lit_occs() const {
|
||||
if (lit_occs_enabled()) {
|
||||
unsigned num_lits = get_num_bool_vars() * 2;
|
||||
for (unsigned l_idx = 0; l_idx < num_lits; ++l_idx) {
|
||||
check_lit_occs(to_literal(l_idx));
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool context::check_enode(enode * n) const {
|
||||
SASSERT(n->check_invariant());
|
||||
bool is_true_eq = n->is_true_eq();
|
||||
|
@ -136,7 +103,6 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool context::check_invariant() const {
|
||||
check_lit_occs();
|
||||
check_bin_watch_lists();
|
||||
check_clauses(m_aux_clauses);
|
||||
check_clauses(m_lemmas);
|
||||
|
|
|
@ -182,7 +182,29 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
bool context::split_binary(app* o, expr*& a, expr_ref& b, expr_ref& c) {
|
||||
expr* x = nullptr, *y = nullptr, *ny = nullptr, *z = nullptr, *u = nullptr;
|
||||
if (m.is_or(o, x, y) &&
|
||||
m.is_not(y, ny) &&
|
||||
m.is_or(ny, z, u)) {
|
||||
a = x;
|
||||
b = m.is_not(z, z) ? z : m.mk_not(z);
|
||||
c = m.is_not(u, u) ? u : m.mk_not(u);
|
||||
return true;
|
||||
}
|
||||
if (m.is_or(o, y, x) &&
|
||||
m.is_not(y, ny) &&
|
||||
m.is_or(ny, z, u)) {
|
||||
a = x;
|
||||
b = m.is_not(z, z) ? z : m.mk_not(z);
|
||||
c = m.is_not(u, u) ? u : m.mk_not(u);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
#define DEEP_EXPR_THRESHOLD 1024
|
||||
|
||||
|
||||
/**
|
||||
\brief Internalize an expression asserted into the logical context using the given proof as a justification.
|
||||
|
@ -226,6 +248,19 @@ namespace smt {
|
|||
}
|
||||
case OP_OR: {
|
||||
literal_buffer lits;
|
||||
expr* a = nullptr;
|
||||
expr_ref b(m), c(m);
|
||||
// perform light-weight rewriting on clauses.
|
||||
if (!relevancy() && split_binary(to_app(n), a, b, c)) {
|
||||
internalize(a, true);
|
||||
internalize(b, true);
|
||||
internalize(c, true);
|
||||
literal lits2[2] = { get_literal(a), get_literal(b) };
|
||||
literal lits3[2] = { get_literal(a), get_literal(c) };
|
||||
mk_root_clause(2, lits2, pr);
|
||||
mk_root_clause(2, lits3, pr);
|
||||
break;
|
||||
}
|
||||
for (expr * arg : *to_app(n)) {
|
||||
internalize(arg, true);
|
||||
lits.push_back(get_literal(arg));
|
||||
|
@ -882,11 +917,9 @@ namespace smt {
|
|||
SASSERT(m_assignment.size() == m_watches.size());
|
||||
m_watches[l.index()] .reset();
|
||||
m_watches[not_l.index()] .reset();
|
||||
if (lit_occs_enabled()) {
|
||||
m_lit_occs.reserve(aux);
|
||||
m_lit_occs[l.index()] .reset();
|
||||
m_lit_occs[not_l.index()] .reset();
|
||||
}
|
||||
m_lit_occs.reserve(aux, 0);
|
||||
m_lit_occs[l.index()] = 0;
|
||||
m_lit_occs[not_l.index()] = 0;
|
||||
bool_var_data & data = m_bdata[v];
|
||||
unsigned iscope_lvl = m_scope_lvl; // record when the boolean variable was internalized.
|
||||
data.init(iscope_lvl);
|
||||
|
@ -1357,11 +1390,14 @@ namespace smt {
|
|||
if (j && !j->in_region())
|
||||
m_justifications.push_back(j);
|
||||
assign(lits[0], j);
|
||||
inc_ref(lits[0]);
|
||||
return nullptr;
|
||||
case 2:
|
||||
if (use_binary_clause_opt(lits[0], lits[1], lemma)) {
|
||||
literal l1 = lits[0];
|
||||
literal l2 = lits[1];
|
||||
inc_ref(l1);
|
||||
inc_ref(l2);
|
||||
m_watches[(~l1).index()].insert_literal(l2);
|
||||
m_watches[(~l2).index()].insert_literal(l1);
|
||||
if (get_assignment(l2) == l_false) {
|
||||
|
@ -1425,8 +1461,7 @@ namespace smt {
|
|||
assign(cls->get_literal(0), b_justification(cls));
|
||||
}
|
||||
|
||||
if (lit_occs_enabled())
|
||||
add_lit_occs(cls);
|
||||
add_lit_occs(*cls);
|
||||
|
||||
TRACE("add_watch_literal_bug", display_clause_detail(tout, cls););
|
||||
TRACE("mk_clause_result", display_clause_detail(tout, cls););
|
||||
|
@ -1435,9 +1470,9 @@ namespace smt {
|
|||
}}
|
||||
}
|
||||
|
||||
void context::add_lit_occs(clause * cls) {
|
||||
for (literal l : *cls) {
|
||||
m_lit_occs[l.index()].insert(cls);
|
||||
void context::add_lit_occs(clause const& cls) {
|
||||
for (literal l : cls) {
|
||||
inc_ref(l);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -37,7 +37,7 @@ namespace smt {
|
|||
// try first sequential with a low conflict budget to make super easy problems cheap
|
||||
ctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, 40u);
|
||||
result = ctx.check(asms.size(), asms.c_ptr());
|
||||
if (result != l_undef || ctx.m_num_conflicts < max_conflicts) {
|
||||
if (result != l_undef || (result == l_undef && ctx.m_num_conflicts < ctx.get_fparams().m_max_conflicts)) {
|
||||
return result;
|
||||
}
|
||||
#else
|
||||
|
|
|
@ -2189,32 +2189,6 @@ public:
|
|||
|
||||
nla::lemma m_lemma;
|
||||
|
||||
// lp::lar_term mk_term(nla::polynomial const& poly) {
|
||||
// lp::lar_term term;
|
||||
// for (auto const& mon : poly) {
|
||||
// SASSERT(!mon.empty());
|
||||
// if (mon.size() == 1) {
|
||||
// term.add_var(mon[0]);
|
||||
// }
|
||||
// else {
|
||||
// // create the expression corresponding to the product.
|
||||
// // internalize it.
|
||||
// // extract the theory var representing the product.
|
||||
// // convert the theory var back to lpvar
|
||||
// expr_ref_vector mul(m);
|
||||
// for (lpvar v : mon) {
|
||||
// theory_var w = lp().local_to_external(v);
|
||||
// mul.push_back(get_enode(w)->get_owner());
|
||||
// }
|
||||
// app_ref t(a.mk_mul(mul.size(), mul.c_ptr()), m);
|
||||
// VERIFY(internalize_term(t));
|
||||
// theory_var w = ctx().get_enode(t)->get_th_var(get_id());
|
||||
// term.add_var(lp().external_to_local(w));
|
||||
// }
|
||||
// }
|
||||
// return term;
|
||||
// }
|
||||
|
||||
void false_case_of_check_nla() {
|
||||
literal_vector core;
|
||||
for (auto const& ineq : m_lemma.ineqs()) {
|
||||
|
|
Loading…
Reference in a new issue