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

branch selection updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-01 10:19:27 -08:00
parent 74fc8cfde7
commit 1e92165690
1 changed files with 34 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
src/smt/theory_arith_int.h
View file

@ -102,10 +102,8 @@ namespace smt {
numeral new_range;
numeral small_range_thresold(1024);
unsigned n = 0;
typename vector<row>::const_iterator it = m_rows.begin();
typename vector<row>::const_iterator end = m_rows.end();
for (; it != end; ++it) {
theory_var v = it->get_base_var();
for (row const& row : m_rows) {
theory_var v = row.get_base_var();
if (v == null_theory_var)
continue;
if (!is_base(v))
@ -120,26 +118,19 @@ namespace smt {
numeral const & u = upper_bound(v).get_rational();
new_range = u;
new_range -= l;
if (new_range > small_range_thresold)
continue;
if (result == null_theory_var) {
if (new_range > small_range_thresold) {
//
}
else if (result == null_theory_var || new_range < range) {
result = v;
range = new_range;
n = 1;
continue;
}
if (new_range < range) {
n = 1;
result = v;
range = new_range;
continue;
}
if (new_range == range) {
else if (new_range == range) {
n++;
if (m_random() % n == 0) {
result = v;
range = new_range;
continue;
}
}
}
@ -166,25 +157,41 @@ namespace smt {
#define SELECT_VAR(VAR) if (r == null_theory_var) { n = 1; r = VAR; } else { n++; SASSERT(n >= 2); if (m_random() % n == 0) r = VAR; }
typename vector<row>::const_iterator it = m_rows.begin();
typename vector<row>::const_iterator end = m_rows.end();
for (; it != end; ++it) {
theory_var v = it->get_base_var();
if (v != null_theory_var && is_base(v) && is_int(v) && !get_value(v).is_int()) {
SELECT_VAR(v);
numeral small_value(1024);
if (r == null_theory_var) {
for (auto const& row : m_rows) {
theory_var v = row.get_base_var();
if (v != null_theory_var && is_base(v) && is_int(v) && !get_value(v).is_int()) {
if (abs(get_value(v)) < small_value) {
SELECT_VAR(v);
}
else if (upper(v) && small_value > upper_bound(v) - get_value(v)) {
SELECT_VAR(v);
}
else if (lower(v) && small_value > get_value(v) - lower_bound(v)) {
SELECT_VAR(v);
}
}
}
}
if (r == null_theory_var) {
it = m_rows.begin();
for (; it != end; ++it) {
theory_var v = it->get_base_var();
for (auto const& row : m_rows) {
theory_var v = row.get_base_var();
if (v != null_theory_var && is_base(v) && is_int(v) && !get_value(v).is_int()) {
SELECT_VAR(v);
}
}
}
if (r == null_theory_var) {
for (auto const& row : m_rows) {
theory_var v = row.get_base_var();
if (v != null_theory_var && is_quasi_base(v) && is_int(v) && !get_value(v).is_int()) {
quasi_base_row2base_row(get_var_row(v));
SELECT_VAR(v);
}
}
if (r == null_theory_var)
return null_theory_var;
}
CASSERT("arith", wf_rows());
CASSERT("arith", wf_columns());