mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

updated seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-21 06:07:50 -08:00
parent 8e26c97782
commit 65da0f9f3a
2 changed files with 9 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/smt/theory_seq.cpp
View file

@ -318,7 +318,8 @@ bool theory_seq::check_length_coherence_tbd() {
// each variable that canonizes to itself can have length 0. // each variable that canonizes to itself can have length 0.
unsigned sz = get_num_vars(); unsigned sz = get_num_vars();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
enode* n = get_enode(i); unsigned j = (i + m_branch_variable_head) % sz;
enode* n = get_enode(j);
expr* e = n->get_owner(); expr* e = n->get_owner();
if (m_util.is_re(e)) { if (m_util.is_re(e)) {
continue; continue;
@ -332,15 +333,14 @@ bool theory_seq::check_length_coherence_tbd() {
TRACE("seq", tout << "Unsolved " << mk_pp(e, m) << "\n";); TRACE("seq", tout << "Unsolved " << mk_pp(e, m) << "\n";);
#if 0 #if 0
if (!assume_equality(e, emp)) { if (!assume_equality(e, emp)) {
// e = emp \/ e = head*tail & head = unit(v) // e = emp \/ e = unit(head.elem(e))*tail(e)
sort* char_sort = 0; sort* char_sort = 0;
VERIFY(m_util.is_seq(m.get_sort(e), char_sort)); VERIFY(m_util.is_seq(m.get_sort(e), char_sort));
expr_ref tail(mk_skolem(symbol("seq.tail"), e), m); expr_ref tail(mk_skolem(symbol("seq.tail"), e), m);
expr_ref v(mk_skolem(symbol("seq.head.elem"), e, 0, 0, char_sort), m); expr_ref v(mk_skolem(symbol("seq.head.elem"), e, 0, 0, char_sort), m);
expr_ref head(m_util.str.mk_unit(v), m); expr_ref head(m_util.str.mk_unit(v), m);
expr_ref conc(m_util.str.mk_concat(head, tail), m); expr_ref conc(m_util.str.mk_concat(head, tail), m);
literal e_eq_emp(mk_eq(e, emp, false)); add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false));
add_axiom(e_eq_emp, mk_eq(e, conc, false));
} }
#endif #endif
coherent = false; coherent = false;
@ -565,10 +565,9 @@ bool theory_seq::solve_nqs() {
bool change = false; bool change = false;
context & ctx = get_context(); context & ctx = get_context();
for (unsigned i = 0; !ctx.inconsistent() && i < m_nqs.size(); ++i) { for (unsigned i = 0; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
change = solve_ne(i) || change; TRACE("seq", tout << i << " " << m_nqs.size() << "\n";);
if (m_nqs[i].is_solved()) { if (!m_nqs[i].is_solved()) {
m_nqs.erase_and_swap(i); change = solve_ne(i) || change;
--i;
} }
} }
return change; return change;
@ -614,7 +613,7 @@ bool theory_seq::solve_ne(unsigned idx) {
// continue // continue
} }
else { else {
TRACE("seq", tout << lhs.size() << "\n"; TRACE("seq",
for (unsigned j = 0; j < lhs.size(); ++j) { for (unsigned j = 0; j < lhs.size(); ++j) {
tout << mk_pp(lhs[j].get(), m) << " "; tout << mk_pp(lhs[j].get(), m) << " ";
} }
@ -625,11 +624,9 @@ bool theory_seq::solve_ne(unsigned idx) {
expr_ref nl(lhs[j].get(), m); expr_ref nl(lhs[j].get(), m);
expr_ref nr(rhs[j].get(), m); expr_ref nr(rhs[j].get(), m);
if (m_util.is_seq(nl) || m_util.is_re(nl)) { if (m_util.is_seq(nl) || m_util.is_re(nl)) {
//std::cout << "push_ne " << nl << " != " << nr << "\n";
m_trail_stack.push(push_ne(*this, idx, nl, nr)); m_trail_stack.push(push_ne(*this, idx, nl, nr));
} }
else { else {
//std::cout << "push_lit\n";
literal lit(mk_eq(nl, nr, false)); literal lit(mk_eq(nl, nr, false));
m_trail_stack.push(push_lit(*this, idx, ~lit)); m_trail_stack.push(push_lit(*this, idx, ~lit));
ctx.mark_as_relevant(lit); ctx.mark_as_relevant(lit);

2
src/util/scoped_vector.h
View file

@ -110,7 +110,7 @@ public:
void erase_and_swap(unsigned i) { void erase_and_swap(unsigned i) {
if (i + 1 < size()) { if (i + 1 < size()) {
set(i, m_elems[m_index[i]]); set(i, m_elems[m_index[size()-1]]);
} }
pop_back(); pop_back();
} }