mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-28 10:28:43 -08:00
parent 071a654a9a
commit 739043e273
4 changed files with 213 additions and 157 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/ast/rewriter/seq_rewriter.cpp
View file

@ -25,6 +25,14 @@ Notes:
#include"automaton.h"
struct display_expr1 {
ast_manager& m;
display_expr1(ast_manager& m): m(m) {}
std::ostream& display(std::ostream& out, expr* e) const {
return out << mk_pp(e, m);
}
};
re2automaton::re2automaton(ast_manager& m): m(m), u(m) {}
@ -36,6 +44,7 @@ eautomaton* re2automaton::operator()(expr* e) {
return r;
}
eautomaton* re2automaton::re2aut(expr* e) {
SASSERT(u.is_re(e));
expr* e1, *e2;
@ -230,8 +239,8 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
result = m_util.str.mk_string(s1 + s2);
return BR_DONE;
}
if (m_util.str.is_concat(b, c, d)) {
result = m_util.str.mk_concat(m_util.str.mk_concat(a, c), d);
if (m_util.str.is_concat(a, c, d)) {
result = m_util.str.mk_concat(c, m_util.str.mk_concat(d, b));
return BR_REWRITE2;
}
if (m_util.str.is_empty(a)) {

20
src/math/automata/automaton.h
View file

@ -84,6 +84,12 @@ private:
mutable uint_set m_visited;
mutable unsigned_vector m_todo;
struct default_display {
std::ostream& display(std::ostream& out, T* t) {
return out << t;
}
};
public:
// The empty automaton:
@ -216,7 +222,7 @@ public:
mvs.push_back(move(m, 0, a.init() + offset1));
append_moves(offset1, a, mvs);
for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
mvs.push_back(move(m, a.m_final_states[i], b.init()));
mvs.push_back(move(m, a.m_final_states[i], b.init() + offset2));
}
append_moves(offset2, b, mvs);
append_final(offset2, b, final);
@ -278,7 +284,7 @@ public:
for (unsigned j = 0; found && j < mvs.size(); ++j) {
found = (mvs[j].dst() == m_init) && mvs[j].is_epsilon();
}
if (!found) {
if (!found && state != m_init) {
add(move(m, state, m_init));
}
}
@ -301,7 +307,7 @@ public:
if (src == dst) {
// just remove this edge.
}
else if (1 == in_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
else if (1 == in_degree(src) && 1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
move const& mv0 = m_delta_inv[src][0];
unsigned src0 = mv0.src();
T* t = mv0.t();
@ -311,8 +317,9 @@ public:
}
add(move(m, src0, dst, t));
remove(src0, src, t);
}
else if (1 == out_degree(dst) && init() != dst && (!is_final_state(dst) || is_final_state(src))) {
else if (1 == out_degree(dst) && 1 == in_degree(dst) && init() != dst && (!is_final_state(dst) || is_final_state(src))) {
move const& mv1 = m_delta[dst][0];
unsigned dst1 = mv1.dst();
T* t = mv1.t();
@ -322,6 +329,7 @@ public:
}
add(move(m, src, dst1, t));
remove(dst, dst1, t);
}
else {
continue;
@ -422,8 +430,8 @@ public:
get_moves(state, m_delta_inv, mvs, epsilon_closure);
}
template<class D>
std::ostream& display(std::ostream& out, D& displayer) const {
template<class D = default_display>
std::ostream& display(std::ostream& out, D& displayer = D()) const {
out << "init: " << init() << "\n";
out << "final: ";
for (unsigned i = 0; i < m_final_states.size(); ++i) out << m_final_states[i] << " ";

325
src/smt/theory_seq.cpp
View file

@ -146,7 +146,6 @@ theory_seq::theory_seq(ast_manager& m):
m_axioms(m),
m_axioms_head(0),
m_branch_variable_head(0),
m_model_completion(false),
m_mg(0),
m_rewrite(m),
m_util(m),
@ -157,14 +156,12 @@ theory_seq::theory_seq(ast_manager& m):
m_steps_qhead(0) {
m_prefix = "seq.prefix.suffix";
m_suffix = "seq.suffix.prefix";
m_left = "seq.left";
m_right = "seq.right";
m_contains_left = "seq.contains.left";
m_contains_right = "seq.contains.right";
m_accept = "aut.accept";
m_reject = "aut.reject";
m_tail = "seq.tail";
m_head_elem = "seq.head.elem";
m_nth = "seq.nth";
m_seq_first = "seq.first";
m_seq_last = "seq.last";
m_indexof_left = "seq.indexof.left";
@ -196,7 +193,7 @@ final_check_status theory_seq::final_check_eh() {
return FC_CONTINUE;
}
if (branch_variable()) {
TRACE("seq", tout << "branch\n";);
TRACE("seq", tout << "branch_variable\n";);
return FC_CONTINUE;
}
if (!check_length_coherence()) {
@ -315,27 +312,27 @@ bool theory_seq::check_length_coherence() {
if (m_length.empty()) return true;
context& ctx = get_context();
bool coherent = true;
// each variable that canonizes to itself can have length 0.
unsigned sz = get_num_vars();
for (unsigned i = 0; i < sz; ++i) {
unsigned j = (i + m_branch_variable_head) % sz;
enode* n = get_enode(j);
expr* e = n->get_owner();
if (m_util.is_re(e)) {
continue;
}
SASSERT(m_util.is_seq(e));
// extend length of variables.
obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
for (; it != end; ++it) {
expr* e = *it;
enode_pair_dependency* dep = 0;
expr* f = m_rep.find(e, dep);
if (is_var(f) && f == e) {
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
expr_ref head(m), tail(m);
rational lo, hi;
TRACE("seq", tout << "Unsolved " << mk_pp(e, m) << "\n";);
TRACE("seq", tout << "Unsolved " << mk_pp(e, m);
if (!lower_bound(e, lo)) lo = -rational::one();
if (!upper_bound(e, hi)) hi = -rational::one();
tout << " lo: " << lo << " ";
tout << "hi: " << hi << " ";
tout << "\n";
ctx.display(tout);
);
if (lower_bound(e, lo) && lo.is_pos() && lo < rational(512)) {
TRACE("seq", tout << "lower bound: " << mk_pp(e, m) << " " << lo << "\n";);
expr_ref low(m_autil.mk_ge(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true)), m);
literal low(mk_literal(m_autil.mk_ge(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true))));
expr_ref seq(e, m);
expr_ref_vector elems(m);
unsigned _lo = lo.get_unsigned();
@ -347,18 +344,14 @@ bool theory_seq::check_length_coherence() {
elems.push_back(seq);
tail = m_util.str.mk_concat(elems.size(), elems.c_ptr());
// len(e) >= low => e = tail
add_axiom(~mk_literal(low), mk_eq(e, tail, false));
add_axiom(~low, mk_eq(e, tail, false));
assume_equality(tail, e);
if (upper_bound(e, hi) && hi == lo) {
expr_ref high(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true)), m);
add_axiom(~mk_literal(high), mk_eq(seq, emp, false));
if (upper_bound(e, hi)) {
expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m);
expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m);
add_axiom(~mk_literal(high1), mk_literal(high2));
}
}
else if (upper_bound(e, hi) && hi.is_zero()) {
expr_ref len(m_util.str.mk_length(e), m);
expr_ref zero(m_autil.mk_int(0), m);
add_axiom(~mk_eq(len, zero, false), mk_eq(e, emp, false));
}
else if (!assume_equality(e, emp)) {
mk_decompose(e, emp, head, tail);
// e = emp \/ e = unit(head.elem(e))*tail(e)
@ -366,7 +359,6 @@ bool theory_seq::check_length_coherence() {
add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false));
assume_equality(tail, emp);
}
m_branch_variable_head = j + 1;
return false;
}
}
@ -380,8 +372,8 @@ void theory_seq::mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref&
VERIFY(m_util.is_seq(m.get_sort(e), char_sort));
emp = m_util.str.mk_empty(m.get_sort(e));
if (m_util.str.is_empty(e)) {
head = m_util.str.mk_unit(mk_skolem(m_head_elem, e, 0, 0, char_sort));
tail = mk_skolem(m_tail, e);
head = m_util.str.mk_unit(mk_skolem(m_nth, e, m_autil.mk_int(0), 0, char_sort));
tail = e;
}
else if (m_util.str.is_string(e, s)) {
head = m_util.str.mk_unit(m_util.str.mk_char(s, 0));
@ -395,13 +387,18 @@ void theory_seq::mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref&
head = e1;
tail = e2;
}
else if (is_skolem(m_tail, e)) {
rational r;
app* a = to_app(e);
expr* s = a->get_arg(0);
VERIFY (m_autil.is_numeral(a->get_arg(1), r));
expr* idx = m_autil.mk_int(r.get_unsigned() + 1);
head = m_util.str.mk_unit(mk_skolem(m_nth, s, idx, 0, char_sort));
tail = mk_skolem(m_tail, s, idx);
}
else {
head = m_util.str.mk_unit(mk_skolem(m_head_elem, e, 0, 0, char_sort));
tail = mk_skolem(m_tail, e);
if (!m_util.is_skolem(e)) {
expr_ref conc(m_util.str.mk_concat(head, tail), m);
add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false));
}
head = m_util.str.mk_unit(mk_skolem(m_nth, e, m_autil.mk_int(0), 0, char_sort));
tail = mk_skolem(m_tail, e, m_autil.mk_int(0));
}
}
@ -531,6 +528,7 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps, bo
}
if (is_var(lh) && !occurs(lh, rh)) {
propagated = add_solution(lh, rh, deps) || propagated;
return true;
}
if (is_var(rh) && !occurs(rh, lh)) {
propagated = add_solution(rh, lh, deps) || propagated;
@ -547,19 +545,21 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps, bo
bool theory_seq::occurs(expr* a, expr* b) {
// true if a occurs under an interpreted function or under left/right selector.
SASSERT(is_var(a));
SASSERT(m_todo.empty());
expr* e1, *e2;
while (is_left_select(a, e1) || is_right_select(a, e1)) {
a = e1;
m_todo.push_back(b);
while (!m_todo.empty()) {
b = m_todo.back();
if (a == b) {
m_todo.reset();
return true;
}
m_todo.pop_back();
if (m_util.str.is_concat(b, e1, e2)) {
m_todo.push_back(e1);
m_todo.push_back(e2);
}
}
if (m_util.str.is_concat(b, e1, e2)) {
return occurs(a, e1) || occurs(a, e2);
}
while (is_left_select(b, e1) || is_right_select(b, e1)) {
b = e1;
}
if (a == b) {
return true;
}
return false;
}
@ -572,16 +572,9 @@ bool theory_seq::is_var(expr* a) {
!m_util.str.is_unit(a);
}
bool theory_seq::is_left_select(expr* a, expr*& b) {
return is_skolem(m_left, a) && (b = to_app(a)->get_arg(0), true);
}
bool theory_seq::is_right_select(expr* a, expr*& b) {
return is_skolem(m_right, a) && (b = to_app(a)->get_arg(0), true);
}
bool theory_seq::is_head_elem(expr* e) const {
return is_skolem(m_head_elem, e);
return is_skolem(m_nth, e);
}
bool theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) {
@ -589,6 +582,7 @@ bool theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) {
return false;
}
context& ctx = get_context();
TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n";);
m_rep.update(l, r, deps);
// TBD: skip new equalities for non-internalized terms.
if (ctx.e_internalized(l) && ctx.e_internalized(r) && ctx.get_enode(l)->get_root() != ctx.get_enode(r)->get_root()) {
@ -768,9 +762,6 @@ bool theory_seq::internalize_term(app* term) {
}
mk_var(e);
}
if (m_util.str.is_length(term, arg) && !has_length(arg)) {
add_length(arg);
}
return true;
}
@ -889,20 +880,103 @@ void theory_seq::init_model(model_generator & mg) {
mg.register_factory(m_factory);
}
class seq_value_proc : public model_value_proc {
theory_seq& th;
app* n;
svector<model_value_dependency> m_dependencies;
public:
seq_value_proc(theory_seq& th, app* n): th(th), n(n) {
}
virtual ~seq_value_proc() {}
void add_dependency(enode* n) { m_dependencies.push_back(model_value_dependency(n)); }
virtual void get_dependencies(buffer<model_value_dependency> & result) {
result.append(m_dependencies.size(), m_dependencies.c_ptr());
}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
SASSERT(values.size() == m_dependencies.size());
ast_manager& m = mg.get_manager();
if (values.empty()) {
return th.mk_value(n);
}
SASSERT(values.size() == n->get_num_args());
return th.mk_value(mg.get_manager().mk_app(n->get_decl(), values.size(), values.c_ptr()));
}
};
model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
enode_pair_dependency* deps = 0;
expr_ref e(n->get_owner(), m);
flet<bool> _model_completion(m_model_completion, true);
m_rep.reset_cache();
m_mg = &mg;
e = canonize(e, deps);
m_mg = 0;
SASSERT(is_app(e));
TRACE("seq", tout << mk_pp(n->get_owner(), m) << " -> " << e << "\n";);
m_factory->add_trail(e);
return alloc(expr_wrapper_proc, to_app(e));
context& ctx = get_context();
enode_pair_dependency* dep = 0;
expr* e = m_rep.find(n->get_owner(), dep);
expr* e1, *e2;
seq_value_proc* sv = alloc(seq_value_proc, *this, to_app(e));
if (m_util.str.is_concat(e, e1, e2)) {
sv->add_dependency(ctx.get_enode(e1));
sv->add_dependency(ctx.get_enode(e2));
}
else if (m_util.str.is_unit(e, e1)) {
sv->add_dependency(ctx.get_enode(e1));
}
return sv;
}
app* theory_seq::mk_value(app* e) {
expr* e1;
expr_ref result(e, m);
if (m_util.str.is_unit(e, e1)) {
enode_pair_dependency* deps = 0;
result = expand(e1, deps);
bv_util bv(m);
rational val;
unsigned sz;
if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) {
svector<bool> val_as_bits;
for (unsigned i = 0; i < sz; ++i) {
val_as_bits.push_back(!val.is_even());
val = div(val, rational(2));
}
result = m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr()));
}
else {
result = m_util.str.mk_unit(result);
}
}
else if (is_var(e)) {
SASSERT(m_factory);
expr_ref val(m);
val = m_factory->get_some_value(m.get_sort(e));
if (val) {
result = val;
}
else {
result = e;
}
}
else if (is_head_elem(e)) {
enode* n = get_context().get_enode(e)->get_root();
enode* n0 = n;
bool found_value = false;
do {
result = n->get_owner();
found_value = m.is_model_value(result);
}
while (n0 != n && !found_value);
if (!found_value) {
if (m_util.is_char(result)) {
result = m_util.str.mk_char('#');
}
else {
result = m_mg->get_some_value(m.get_sort(result));
}
}
}
m_rewrite(result);
m_factory->add_trail(result);
TRACE("seq", tout << mk_pp(e, m) << " -> " << result << "\n";);
return to_app(result);
}
theory_var theory_seq::mk_var(enode* n) {
@ -957,49 +1031,6 @@ expr_ref theory_seq::expand(expr* e0, enode_pair_dependency*& eqs) {
else if (m_util.str.is_contains(e, e1, e2)) {
result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps));
}
else if (m_model_completion && is_var(e)) {
SASSERT(m_factory);
expr_ref val(m);
val = m_factory->get_some_value(m.get_sort(e));
if (val) {
m_rep.update(e, val, 0);
result = val;
}
else {
result = e;
}
}
else if (m_model_completion && m_util.str.is_unit(e, e1)) {
result = expand(e1, deps);
bv_util bv(m);
rational val;
unsigned sz;
if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) {
svector<bool> val_as_bits;
for (unsigned i = 0; i < sz; ++i) {
val_as_bits.push_back(!val.is_even());
val = div(val, rational(2));
}
result = m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr()));
}
else {
result = m_util.str.mk_unit(result);
}
}
else if (m_model_completion && is_head_elem(e)) {
enode* n = get_context().get_enode(e)->get_root();
result = n->get_owner();
if (!m.is_model_value(result)) {
if (m_util.is_char(result)) {
result = m_util.str.mk_char('#');
}
else {
result = m_mg->get_some_value(m.get_sort(result));
}
}
m_rep.update(e, result, 0);
TRACE("seq", tout << mk_pp(e, m) << " |-> " << result << "\n";);
}
else {
result = e;
}
@ -1193,15 +1224,6 @@ void theory_seq::add_elim_string_axiom(expr* n) {
}
void theory_seq::add_length_coherence_axiom(expr* n) {
expr_ref len(n, m);
m_rewrite(len);
if (n != len) {
TRACE("seq", tout << "Add length coherence for " << mk_pp(n, m) << "\n";);
add_axiom(mk_eq(n, len, false));
}
}
/*
let n = len(x)
@ -1212,9 +1234,18 @@ void theory_seq::add_length_coherence_axiom(expr* n) {
void theory_seq::add_length_axiom(expr* n) {
expr* x;
VERIFY(m_util.str.is_length(n, x));
if (!m_util.str.is_unit(x) &&
!m_util.str.is_empty(x) &&
!m_util.str.is_string(x)) {
if (m_util.str.is_concat(x) ||
m_util.str.is_unit(x) ||
m_util.str.is_empty(x) ||
m_util.str.is_string(x)) {
expr_ref len(n, m);
m_rewrite(len);
if (n != len) {
TRACE("seq", tout << "Add length coherence for " << mk_pp(n, m) << "\n";);
add_axiom(mk_eq(n, len, false));
}
}
else {
expr_ref zero(m_autil.mk_int(0), m);
expr_ref emp(m_util.str.mk_empty(m.get_sort(x)), m);
literal eq1(mk_eq(zero, n, false));
@ -1223,12 +1254,6 @@ void theory_seq::add_length_axiom(expr* n) {
add_axiom(~eq1, eq2);
add_axiom(~eq2, eq1);
}
if (m_util.str.is_concat(x) ||
m_util.str.is_unit(x) ||
m_util.str.is_empty(x) ||
m_util.str.is_string(x)) {
add_length_coherence_axiom(x);
}
}
@ -1638,8 +1663,7 @@ void theory_seq::restart_eh() {
}
void theory_seq::relevant_eh(app* n) {
if (m_util.str.is_length(n) ||
m_util.str.is_index(n) ||
if (m_util.str.is_index(n) ||
m_util.str.is_replace(n) ||
m_util.str.is_extract(n) ||
m_util.str.is_at(n) ||
@ -1647,6 +1671,11 @@ void theory_seq::relevant_eh(app* n) {
is_step(n)) {
enque_axiom(n);
}
expr* arg;
if (m_util.str.is_length(n, arg) && !has_length(arg)) {
enforce_length(get_context().get_enode(arg));
}
}
@ -1729,24 +1758,28 @@ expr_ref theory_seq::mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned
void theory_seq::add_accept2step(expr* acc) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(acc) == l_true);
expr* s, *re;
expr* e, *re;
unsigned src;
eautomaton* aut = 0;
VERIFY(is_accept(acc, s, re, src, aut));
VERIFY(is_accept(acc, e, re, src, aut));
if (!aut) return;
if (m_util.str.is_empty(s)) return;
if (m_util.str.is_empty(e)) return;
eautomaton::moves mvs;
aut->get_moves_from(src, mvs);
expr_ref head(m), tail(m), emp(m), step(m);
mk_decompose(s, emp, head, tail);
mk_decompose(e, emp, head, tail);
if (!m_util.is_skolem(e)) {
expr_ref conc(m_util.str.mk_concat(head, tail), m);
add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false));
}
literal_vector lits;
lits.push_back(~ctx.get_literal(acc));
if (aut->is_final_state(src)) {
lits.push_back(mk_eq(emp, s, false));
lits.push_back(mk_eq(emp, e, false));
}
for (unsigned i = 0; i < mvs.size(); ++i) {
eautomaton::move mv = mvs[i];
step = mk_step(s, tail, re, src, mv.dst(), mv.t());
step = mk_step(e, tail, re, src, mv.dst(), mv.t());
lits.push_back(mk_literal(step));
}
TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
@ -1778,22 +1811,26 @@ void theory_seq::add_step2accept(expr* step) {
void theory_seq::add_reject2reject(expr* rej) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(rej) == l_true);
expr* s, *re;
expr* e, *re;
unsigned src;
eautomaton* aut = 0;
VERIFY(is_reject(rej, s, re, src, aut));
VERIFY(is_reject(rej, e, re, src, aut));
if (!aut) return;
if (m_util.str.is_empty(s)) return;
if (m_util.str.is_empty(e)) return;
eautomaton::moves mvs;
aut->get_moves_from(src, mvs);
expr_ref head(m), tail(m), emp(m), conc(m);
mk_decompose(s, emp, head, tail);
mk_decompose(e, emp, head, tail);
if (!m_util.is_skolem(e)) {
expr_ref conc(m_util.str.mk_concat(head, tail), m);
add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false));
}
literal rej1 = ctx.get_literal(rej);
for (unsigned i = 0; i < mvs.size(); ++i) {
eautomaton::move const& mv = mvs[i];
conc = m_util.str.mk_concat(m_util.str.mk_unit(mv.t()), tail);
literal rej2 = mk_reject(tail, re, m_autil.mk_int(mv.dst()));
add_axiom(~rej1, ~mk_eq(s, conc, false), rej2);
add_axiom(~rej1, ~mk_eq(e, conc, false), rej2);
}
}

12
src/smt/theory_seq.h
View file

@ -259,17 +259,17 @@ namespace smt {
unsigned m_axioms_head; // index of first axiom to add.
unsigned m_branch_variable_head; // index of first equation to examine.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
obj_hashtable<expr> m_length; // is length applied
bool m_model_completion; // during model construction, invent values in canonizer
obj_hashtable<expr> m_length; // is length applied
model_generator* m_mg;
th_rewriter m_rewrite;
seq_util m_util;
arith_util m_autil;
th_trail_stack m_trail_stack;
stats m_stats;
symbol m_prefix, m_suffix, m_contains_left, m_contains_right, m_left, m_right, m_accept, m_reject;
symbol m_tail, m_head_elem, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
symbol m_prefix, m_suffix, m_contains_left, m_contains_right, m_accept, m_reject;
symbol m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
symbol m_extract_prefix, m_at_left, m_at_right;
ptr_vector<expr> m_todo;
// maintain automata with regular expressions.
scoped_ptr_vector<eautomaton> m_automata;
@ -348,7 +348,6 @@ namespace smt {
void add_replace_axiom(expr* e);
void add_extract_axiom(expr* e);
void add_length_axiom(expr* n);
void add_length_coherence_axiom(expr* n);
bool has_length(expr *e) const { return m_length.contains(e); }
void add_length(expr* e);
@ -407,6 +406,9 @@ namespace smt {
theory_seq(ast_manager& m);
virtual ~theory_seq();
// model building
app* mk_value(app* a);
};
};