mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

add length axioms

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-13 14:22:58 +02:00
parent a49a5b3a0b
commit 0752b1385c
4 changed files with 43 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -786,15 +786,37 @@ namespace seq {
unsigned sz = bv.get_bv_size(b);
expr_ref_vector es(m);
expr_ref bb(b, m), ten(bv.mk_numeral(10, sz), m);
for (unsigned i = 0; i < k; ++i) {
pow = 1;
for (unsigned i = 0; i <= k; ++i) {
if (pow > 1)
bb = bv.mk_bv_udiv(b, bv.mk_numeral(pow, bv_sort));
es.push_back(seq.str.mk_unit(m_sk.mk_ubv2ch(bv.mk_bv_urem(bb, ten))));
bb = bv.mk_bv_udiv(bb, ten);
pow *= 10;
}
es.reverse();
eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort()));
add_clause(~ge10k, ge10k1, eq);
}
/*
* len(ubv2s(b)) = k => 10^k-1 <= b < 10^{k} k > 1
* len(ubv2s(b)) = 1 => b < 10^{1} k = 1
*/
void axioms::ubv2s_len_axiom(expr* b, unsigned k) {
expr_ref ge10k(m), ge10k1(m), eq(m);
bv_util bv(m);
sort* bv_sort = b->get_sort();
rational pow(1);
for (unsigned i = 1; i < k; ++i)
pow *= 10;
ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b);
ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b);
eq = m.mk_eq(seq.str.mk_length(seq.str.mk_ubv2s(b)), a.mk_int(k));
add_clause(~eq, ~ge10k1);
if (k > 1)
add_clause(~eq, ge10k);
}
void axioms::ubv2ch_axiom(sort* bv_sort) {
bv_util bv(m);
expr_ref eq(m);