mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-09-20 11:28:01 -07:00
commit 37ad1f9807
4 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/proto_model/datatype_factory.cpp
View file

@ -67,6 +67,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
value_set * set = get_value_set(s);
if (set->empty()) {
expr * val = get_some_value(s);
SASSERT(val);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, val);
return val;
@ -185,10 +186,16 @@ expr * datatype_factory::get_fresh_value(sort * s) {
if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
found_sibling = true;
expr * maybe_new_arg = get_almost_fresh_value(s_arg);
if (!maybe_new_arg) {
maybe_new_arg = m_model.get_some_value(s_arg);
found_sibling = false;
}
SASSERT(maybe_new_arg);
args.push_back(maybe_new_arg);
}
else {
expr * some_arg = m_model.get_some_value(s_arg);
SASSERT(some_arg);
args.push_back(some_arg);
}
}

13
src/smt/proto_model/value_factory.h
View file

@ -184,18 +184,17 @@ public:
sort_size const* sz = s_info?&s_info->get_num_elements():0;
bool has_max = false;
Number max_size;
if (sz && sz->is_finite()) {
if (sz->size() < UINT_MAX) {
unsigned usz = static_cast<unsigned>(sz->size());
max_size = Number(usz);
has_max = true;
}
if (sz && sz->is_finite() && sz->size() < UINT_MAX) {
unsigned usz = static_cast<unsigned>(sz->size());
max_size = Number(usz);
has_max = true;
}
Number start = set->m_next;
Number & next = set->m_next;
while (!is_new) {
result = mk_value(next, s, is_new);
next++;
if (has_max && next >= max_size) {
if (has_max && next > max_size + start) {
return 0;
}
}

1
src/tactic/sls/sls_tactic.cpp
View file

@ -1343,6 +1343,7 @@ class sls_tactic : public tactic {
m_zero(m_mpz_manager.mk_z(0)),
m_one(m_mpz_manager.mk_z(1)),
m_two(m_mpz_manager.mk_z(2)),
m_cancel(false),
m_bv_util(m),
m_tracker(m, m_bv_util, m_mpz_manager, m_powers)
{

2
src/test/qe_arith.cpp
View file

@ -106,7 +106,7 @@ static void test2(char const *ex) {
sorts.push_back(m.get_sort(vars[i].get()));
}
expr_abstract(m, 0, bound.size(), bound.c_ptr(), fml, fml2);
fml2 = m.mk_exists(boud.size(), sorts.c_ptr(), names.c_ptr(), fml2);
fml2 = m.mk_exists(bound.size(), sorts.c_ptr(), names.c_ptr(), fml2);
qe::expr_quant_elim qe(m, params);
expr_ref pr1 = qe::arith_project(*md, vars, lits);
qe(m.mk_true(), fml2, pr2);