mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 22:33:40 +00:00
Code Activity

Addressing comments from pull request: more descriptive variable names and m.mk_not

Browse source
This commit is contained in:
Federico Mora 2019-11-27 11:30:18 -08:00 • committed by Nikolaj Bjorner
parent 574051df1b
commit 30d9ea5c2c
1 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_str.cpp
View file

@ -1882,14 +1882,16 @@ namespace smt {
} }
// axiom 2: The only (str.from-int N) that starts with a "0" is "0". // axiom 2: The only (str.from-int N) that starts with a "0" is "0".
expr_ref zero(mk_string("0"), m); {
// let (the result starts with a "0") be p expr_ref zero(mk_string("0"), m);
expr_ref p(u.str.mk_prefix(zero, ex), m); // let (the result starts with a "0") be p
// let (the result is "0") be q expr_ref starts_with_zero(u.str.mk_prefix(zero, ex), m);
expr_ref q(ctx.mk_eq_atom(ex, zero), m); // let (the result is "0") be q
// encoding: the result does NOT start with a "0" (~p) xor the result is "0" (q) expr_ref is_zero(ctx.mk_eq_atom(ex, zero), m);
// ~p xor q == (~p or q) and (p or ~q) // encoding: the result does NOT start with a "0" (~p) xor the result is "0" (q)
assert_axiom(m.mk_and(m.mk_or(mk_not(m, p), q), m.mk_or(p, mk_not(m, q)))); // ~p xor q == (~p or q) and (p or ~q)
assert_axiom(m.mk_and(m.mk_or(m.mk_not(starts_with_zero), is_zero), m.mk_or(starts_with_zero, m.mk_not(is_zero))));
}
} }
expr * theory_str::mk_RegexIn(expr * str, expr * regexp) { expr * theory_str::mk_RegexIn(expr * str, expr * regexp) {