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

Added more comments

Browse source
This commit is contained in:
Federico Mora 2019-11-26 20:40:51 -08:00 • committed by Nikolaj Bjorner
parent 6ffb475007
commit 900e707619
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str.cpp
View file

@ -1884,8 +1884,9 @@ namespace smt {
// axiom 2: (str.from-int N) should not result in a string with leading zeros. // axiom 2: (str.from-int N) should not result in a string with leading zeros.
expr_ref zero(mk_string("0"), m); expr_ref zero(mk_string("0"), m);
expr_ref pref(u.str.mk_prefix(zero, ex), m); expr_ref pref(u.str.mk_prefix(zero, ex), m);
// The result does not start with a "0" xor the result is "0" // The result does not start with a "0" (~p) xor the result is "0" (q)
assert_axiom(m.mk_or(m.mk_and(mk_not(m, pref), ctx.mk_eq_atom(ex, zero)), m.mk_and(pref, mk_not(m, ctx.mk_eq_atom(ex, zero))))); // ~p xor q == (p or q) and (~p or ~q)
assert_axiom(m.mk_and(m.mk_or(pref, ctx.mk_eq_atom(ex, zero)), m.mk_or(mk_not(m, pref), mk_not(m, ctx.mk_eq_atom(ex, zero)))));
} }
expr * theory_str::mk_RegexIn(expr * str, expr * regexp) { expr * theory_str::mk_RegexIn(expr * str, expr * regexp) {