mirror of
https://github.com/Z3Prover/z3
synced 2025-07-23 12:48:53 +00:00
char value
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a0b7879dd9
commit
8ed1992029
3 changed files with 9 additions and 9 deletions
|
@ -224,8 +224,8 @@ namespace smt {
|
||||||
unsigned c = 0, d = 0;
|
unsigned c = 0, d = 0;
|
||||||
for (unsigned v = get_num_vars(); v-- > 0; ) {
|
for (unsigned v = get_num_vars(); v-- > 0; ) {
|
||||||
expr* e = get_expr(v);
|
expr* e = get_expr(v);
|
||||||
if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_value(v, c)) {
|
if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_char_value(v, c)) {
|
||||||
CTRACE("seq", seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_value(v, c) << "\n";);
|
CTRACE("seq", seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";);
|
||||||
enode* r = get_enode(v)->get_root();
|
enode* r = get_enode(v)->get_root();
|
||||||
m_value2var.reserve(c + 1, null_theory_var);
|
m_value2var.reserve(c + 1, null_theory_var);
|
||||||
theory_var u = m_value2var[c];
|
theory_var u = m_value2var[c];
|
||||||
|
@ -241,7 +241,7 @@ namespace smt {
|
||||||
u = n->get_th_var(get_id());
|
u = n->get_th_var(get_id());
|
||||||
if (u == null_theory_var)
|
if (u == null_theory_var)
|
||||||
continue;
|
continue;
|
||||||
if (get_value(u, d) && d != c) {
|
if (get_char_value(u, d) && d != c) {
|
||||||
enforce_ackerman(u, v);
|
enforce_ackerman(u, v);
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
@ -323,11 +323,11 @@ namespace smt {
|
||||||
++m_stats.m_num_ackerman;
|
++m_stats.m_num_ackerman;
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned theory_char::get_value(theory_var v) {
|
unsigned theory_char::get_char_value(theory_var v) {
|
||||||
return m_var2value[v];
|
return m_var2value[v];
|
||||||
}
|
}
|
||||||
|
|
||||||
bool theory_char::get_value(theory_var v, unsigned& c) {
|
bool theory_char::get_char_value(theory_var v, unsigned& c) {
|
||||||
if (!has_bits(v))
|
if (!has_bits(v))
|
||||||
return false;
|
return false;
|
||||||
auto const & b = get_bits(v);
|
auto const & b = get_bits(v);
|
||||||
|
@ -348,7 +348,7 @@ namespace smt {
|
||||||
}
|
}
|
||||||
|
|
||||||
model_value_proc * theory_char::mk_value(enode * n, model_generator & mg) {
|
model_value_proc * theory_char::mk_value(enode * n, model_generator & mg) {
|
||||||
unsigned ch = get_value(n->get_th_var(get_id()));
|
unsigned ch = get_char_value(n->get_th_var(get_id()));
|
||||||
app* val = seq.str.mk_char(ch);
|
app* val = seq.str.mk_char(ch);
|
||||||
m_factory->add_trail(val);
|
m_factory->add_trail(val);
|
||||||
return alloc(expr_wrapper_proc, val);
|
return alloc(expr_wrapper_proc, val);
|
||||||
|
|
|
@ -56,7 +56,7 @@ namespace smt {
|
||||||
|
|
||||||
void init_bits(theory_var v);
|
void init_bits(theory_var v);
|
||||||
|
|
||||||
bool get_value(theory_var v, unsigned& c);
|
bool get_char_value(theory_var v, unsigned& c);
|
||||||
|
|
||||||
void enforce_ackerman(theory_var v, theory_var w);
|
void enforce_ackerman(theory_var v, theory_var w);
|
||||||
|
|
||||||
|
@ -87,7 +87,7 @@ namespace smt {
|
||||||
void assign_le(theory_var v1, theory_var v2, literal lit);
|
void assign_le(theory_var v1, theory_var v2, literal lit);
|
||||||
void assign_lt(theory_var v1, theory_var v2, literal lit);
|
void assign_lt(theory_var v1, theory_var v2, literal lit);
|
||||||
void new_const_char(theory_var v, unsigned c);
|
void new_const_char(theory_var v, unsigned c);
|
||||||
unsigned get_value(theory_var v);
|
unsigned get_char_value(theory_var v);
|
||||||
|
|
||||||
void internalize_le(literal lit, app* term);
|
void internalize_le(literal lit, app* term);
|
||||||
};
|
};
|
||||||
|
|
|
@ -1992,7 +1992,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
|
||||||
return sv;
|
return sv;
|
||||||
}
|
}
|
||||||
else if (m_char.enabled() && m_util.is_char(e)) {
|
else if (m_char.enabled() && m_util.is_char(e)) {
|
||||||
unsigned ch = m_char.get_value(n->get_th_var(get_id()));
|
unsigned ch = m_char.get_char_value(n->get_th_var(get_id()));
|
||||||
app* val = m_util.str.mk_char(ch);
|
app* val = m_util.str.mk_char(ch);
|
||||||
m_factory->add_trail(val);
|
m_factory->add_trail(val);
|
||||||
return alloc(expr_wrapper_proc, val);
|
return alloc(expr_wrapper_proc, val);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue