mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-01 17:59:31 -08:00
parent 42219204ed
commit 9d3c8a6a2f
3 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/seq_axioms.cpp
View file

@ -1085,10 +1085,10 @@ namespace seq {
sort* domain[4] = { srt, srt, srt, srt };
auto d = plugin.ensure_def(symbol("ra"), 4, domain, m.mk_bool_sort(), true);
func_decl* ra = d.get_def()->get_decl();
var_ref vs(m.mk_var(0, srt), m);
var_ref vp(m.mk_var(1, srt), m);
var_ref vt(m.mk_var(2, srt), m);
var_ref vr(m.mk_var(3, srt), m);
var_ref vs(m.mk_var(3, srt), m);
var_ref vp(m.mk_var(2, srt), m);
var_ref vt(m.mk_var(1, srt), m);
var_ref vr(m.mk_var(0, srt), m);
var* vars[4] = { vs, vp, vt, vr };
expr_ref test1(seq.str.mk_is_empty(vs), m);
expr_ref branch1(seq.str.mk_is_empty(vr), m);

1
src/smt/seq_axioms.h
View file

@ -73,6 +73,7 @@ namespace smt {
void add_indexof_axiom(expr* n) { m_ax.indexof_axiom(n); }
void add_last_indexof_axiom(expr* n) { m_ax.last_indexof_axiom(n); }
void add_replace_axiom(expr* n) { m_ax.replace_axiom(n); }
void add_replace_all_axiom(expr* n) { m_ax.replace_all_axiom(n); }
void add_at_axiom(expr* n) { m_ax.at_axiom(n); }
void add_nth_axiom(expr* n) { m_ax.nth_axiom(n); }
void add_itos_axiom(expr* n) { m_ax.itos_axiom(n); }

4
src/smt/theory_seq.cpp
View file

@ -2646,6 +2646,9 @@ void theory_seq::deque_axiom(expr* n) {
else if (m_util.str.is_replace(n)) {
m_ax.add_replace_axiom(n);
}
else if (m_util.str.is_replace_all(n)) {
m_ax.add_replace_all_axiom(n);
}
else if (m_util.str.is_extract(n)) {
m_ax.add_extract_axiom(n);
}
@ -3190,6 +3193,7 @@ void theory_seq::relevant_eh(app* n) {
m_util.str.is_to_code(n) ||
m_util.str.is_unit(n) ||
m_util.str.is_length(n) ||
/* m_util.str.is_replace_all(n) || uncomment to enable axiomatization */
m_util.str.is_le(n)) {
enque_axiom(n);
}