mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

Cleanup and revert/incorporate changes -- merge remote-tracking branch 'upstream/master'

Browse source
This commit is contained in:
calebstanford-msr 2020-06-08 11:18:23 -04:00
commit 36102a65ea
11 changed files with 545 additions and 553 deletions
Download patch file Download diff file Expand all files Collapse all files

1
CMakeLists.txt
View file

@ -315,6 +315,7 @@ endif()
################################################################################
# Threading support
################################################################################
set(THREADS_PREFER_PTHREAD_FLAG TRUE)
find_package(Threads)
list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})

2
src/api/api_log.cpp
View file

@ -54,7 +54,7 @@ extern "C" {
res = false;
}
else {
*g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n";
*g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << "\"\n";
g_z3_log->flush();
g_z3_log_enabled = true;
}

795
src/ast/rewriter/seq_rewriter.cpp
View file

@ -416,6 +416,9 @@ br_status seq_rewriter::mk_bool_app(func_decl* f, unsigned n, expr* const* args,
return mk_bool_app_helper(true, n, args, result);
case OP_OR:
return mk_bool_app_helper(false, n, args, result);
case OP_EQ:
SASSERT(n == 2);
// return mk_eq_helper(args[0], args[1], result);
default:
return BR_FAILED;
}
@ -492,7 +495,27 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const*
}
}
result = is_and ? m().mk_and(new_args.size(), new_args.c_ptr()) : m().mk_or(new_args.size(), new_args.c_ptr());
result = is_and ? m().mk_and(new_args) : m().mk_or(new_args);
return BR_REWRITE_FULL;
}
br_status seq_rewriter::mk_eq_helper(expr* a, expr* b, expr_ref& result) {
expr* sa = nullptr, *ra = nullptr, *sb = nullptr, *rb = nullptr;
if (str().is_in_re(b))
std::swap(a, b);
if (!str().is_in_re(a, sa, ra))
return BR_FAILED;
bool is_not = m().is_not(b, b);
if (!str().is_in_re(b, sb, rb))
return BR_FAILED;
if (sa != sb)
return BR_FAILED;
// sa in ra = sb in rb;
// sa in (ra n rb) u (C(ra) n C(rb))
if (is_not)
rb = re().mk_complement(rb);
expr* r = re().mk_union(re().mk_inter(ra, rb), re().mk_inter(re().mk_complement(ra), re().mk_complement(rb)));
result = re().mk_in_re(sa, r);
return BR_REWRITE_FULL;
}
@ -703,9 +726,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case _OP_STRING_STRIDOF:
UNREACHABLE();
}
// if (st == BR_FAILED) {
// st = lift_ites_throttled(f, num_args, args, result);
// }
if (st == BR_FAILED) {
st = lift_ites_throttled(f, num_args, args, result);
}
CTRACE("seq_verbose", st != BR_FAILED, tout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n";);
SASSERT(st == BR_FAILED || m().get_sort(result) == f->get_range());
return st;
@ -2137,7 +2160,7 @@ expr_ref seq_rewriter::is_nullable_rec(expr* r) {
if (!result) {
std::cout << "(m) ";
result = is_nullable(r);
m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result);
m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result);
} else {
std::cout << "(h) ";
}
@ -2288,119 +2311,226 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
Symbolic derivative: seq -> regex -> regex
seq should be single char
*/
br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
sort *seq_sort = nullptr, *ele_sort = nullptr;
result = mk_derivative(ele, r);
// TBD: we may even declare BR_DONE here and potentially miss some simplifications
return re().is_derivative(result) ? BR_DONE : BR_REWRITE_FULL;
}
/*
Recursive implementation of the symbolic derivative such that
the result is in an optimized BDD form.
Definition of BDD form:
if-then-elses are pushed outwards
and sorted by condition ID (cond->get_id()), from largest on
the outside to smallest on the inside.
Duplicate nested conditions are eliminated.
*/
expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
expr_ref result(m_op_cache.find(OP_RE_DERIVATIVE, ele, r, nullptr), m());
if (!result) {
result = mk_derivative_rec(ele, r);
m_op_cache.insert(OP_RE_DERIVATIVE, ele, r, nullptr, result);
}
return result;
}
expr_ref seq_rewriter::mk_der_union(expr* r1, expr* r2) {
return mk_der_op(OP_RE_UNION, r1, r2);
}
expr_ref seq_rewriter::mk_der_inter(expr* r1, expr* r2) {
return mk_der_op(OP_RE_INTERSECT, r1, r2);
}
expr_ref seq_rewriter::mk_der_concat(expr* r1, expr* r2) {
return mk_der_op(OP_RE_CONCAT, r1, r2);
}
/*
Form a derivative by combining two if-then-else expressions in BDD form.
Preconditions:
- k is a binary op code on REs (re.union, re.inter, etc.)
- a and b are in BDD form
Postcondition:
- result is in BDD form
*/
expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) {
expr* ca = nullptr, *a1 = nullptr, *a2 = nullptr;
expr* cb = nullptr, *b1 = nullptr, *b2 = nullptr;
expr_ref result(m());
auto mk_ite = [&](expr* c, expr* a, expr* b) {
return (a == b) ? a : m().mk_ite(c, a, b);
};
if (m().is_ite(a, ca, a1, a2)) {
if (m().is_ite(b, cb, b1, b2)) {
if (ca == cb) {
expr_ref r1 = mk_der_op(k, a1, b1);
expr_ref r2 = mk_der_op(k, a2, b2);
result = mk_ite(ca, r1, r2);
return result;
}
else if (ca->get_id() < cb->get_id()) {
expr_ref r1 = mk_der_op(k, a, b1);
expr_ref r2 = mk_der_op(k, a, b2);
result = mk_ite(cb, r1, r2);
return result;
}
}
expr_ref r1 = mk_der_op(k, a1, b);
expr_ref r2 = mk_der_op(k, a2, b);
result = mk_ite(ca, r1, r2);
return result;
}
if (m().is_ite(b, cb, b1, b2)) {
expr_ref r1 = mk_der_op(k, a, b1);
expr_ref r2 = mk_der_op(k, a, b2);
result = mk_ite(cb, r1, r2);
return result;
}
switch (k) {
case OP_RE_INTERSECT:
if (BR_FAILED == mk_re_inter(a, b, result))
result = re().mk_inter(a, b);
break;
case OP_RE_UNION:
if (BR_FAILED == mk_re_union(a, b, result))
result = re().mk_union(a, b);
break;
case OP_RE_CONCAT:
if (BR_FAILED == mk_re_concat(a, b, result))
result = re().mk_concat(a, b);
break;
default:
UNREACHABLE();
break;
}
return result;
}
expr_ref seq_rewriter::mk_der_op(decl_kind k, expr* a, expr* b) {
expr_ref _a(a, m()), _b(b, m());
expr_ref result(m_op_cache.find(k, a, b, nullptr), m());
if (!result) {
result = mk_der_op_rec(k, a, b);
m_op_cache.insert(k, a, b, nullptr, result);
}
return result;
}
expr_ref seq_rewriter::mk_der_compl(expr* r) {
expr_ref result(m_op_cache.find(OP_RE_COMPLEMENT, r, nullptr, nullptr), m());
if (!result) {
expr* c = nullptr, * r1 = nullptr, * r2 = nullptr;
if (m().is_ite(r, c, r1, r2)) {
result = m().mk_ite(c, mk_der_compl(r1), mk_der_compl(r2));
}
else if (BR_FAILED == mk_re_complement(r, result))
result = re().mk_complement(r);
}
m_op_cache.insert(OP_RE_COMPLEMENT, r, nullptr, nullptr, result);
return result;
}
expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
expr_ref result(m());
sort* seq_sort = nullptr, *ele_sort = nullptr;
VERIFY(m_util.is_re(r, seq_sort));
VERIFY(m_util.is_seq(seq_sort, ele_sort));
SASSERT(ele_sort == m().get_sort(ele));
expr *r1 = nullptr, *r2 = nullptr, *p = nullptr;
expr* r1 = nullptr, *r2 = nullptr, *p = nullptr;
auto mk_empty = [&]() { return expr_ref(re().mk_empty(m().get_sort(r)), m()); };
unsigned lo = 0, hi = 0;
if (re().is_concat(r, r1, r2)) {
expr_ref is_n = is_nullable(r1);
expr_ref dr1(re().mk_derivative(ele, r1), m());
expr_ref dr2(re().mk_derivative(ele, r2), m());
result = re().mk_concat(dr1, r2);
expr_ref dr1 = mk_derivative(ele, r1);
result = mk_der_concat(dr1, r2);
if (m().is_false(is_n)) {
return BR_REWRITE2;
}
else if (m().is_true(is_n)) {
result = re().mk_union(result, dr2);
return BR_REWRITE3;
}
else {
result = m().mk_ite(is_n, re().mk_union(result, dr2), result);
return BR_REWRITE3;
return result;
}
expr_ref dr2 = mk_derivative(ele, r2);
is_n = re_predicate(is_n, seq_sort);
return mk_der_union(result, mk_der_concat(is_n, dr2));
}
else if (re().is_star(r, r1)) {
result = re().mk_concat(re().mk_derivative(ele, r1), r);
return BR_REWRITE2;
return mk_der_concat(mk_derivative(ele, r1), r);
}
else if (re().is_plus(r, r1)) {
result = re().mk_derivative(ele, re().mk_star(r1));
return BR_REWRITE1;
expr_ref star(re().mk_star(r1), m());
return mk_derivative(ele, star);
}
else if (re().is_union(r, r1, r2)) {
result = re().mk_union(
re().mk_derivative(ele, r1),
re().mk_derivative(ele, r2)
);
return BR_REWRITE2;
return mk_der_union(mk_derivative(ele, r1), mk_derivative(ele, r2));
}
else if (re().is_intersection(r, r1, r2)) {
result = re().mk_inter(
re().mk_derivative(ele, r1),
re().mk_derivative(ele, r2)
);
return BR_REWRITE2;
return mk_der_inter(mk_derivative(ele, r1), mk_derivative(ele, r2));
}
else if (re().is_diff(r, r1, r2)) {
result = re().mk_diff(
re().mk_derivative(ele, r1),
re().mk_derivative(ele, r2)
);
return BR_REWRITE2;
return mk_der_inter(mk_derivative(ele, r1), mk_der_compl(mk_derivative(ele, r2)));
}
else if (m().is_ite(r, p, r1, r2)) {
result = m().mk_ite(
p,
re().mk_derivative(ele, r1),
re().mk_derivative(ele, r2)
);
return BR_REWRITE2;
// there is no BDD normalization here
result = m().mk_ite(p, mk_derivative(ele, r1), mk_derivative(ele, r2));
return result;
}
else if (re().is_opt(r, r1)) {
result = re().mk_derivative(ele, r1);
return BR_REWRITE1;
return mk_derivative(ele, r1);
}
else if (re().is_complement(r, r1)) {
result = re().mk_complement(re().mk_derivative(ele, r1));
return BR_REWRITE2;
return mk_der_compl(mk_derivative(ele, r1));
}
else if (re().is_loop(r, r1, lo)) {
if (lo > 0) {
lo--;
}
result = re().mk_concat(
re().mk_derivative(ele, r1),
re().mk_loop(r1, lo)
);
return BR_REWRITE2;
return mk_der_concat(mk_derivative(ele, r1), re().mk_loop(r1, lo));
}
else if (re().is_loop(r, r1, lo, hi)) {
if (hi == 0) {
result = re().mk_empty(m().get_sort(r));
return BR_DONE;
return mk_empty();
}
hi--;
if (lo > 0) {
lo--;
}
result = re().mk_concat(
re().mk_derivative(ele, r1),
re().mk_loop(r1, lo, hi)
);
return BR_REWRITE2;
return mk_der_concat(mk_derivative(ele, r1), re().mk_loop(r1, lo, hi));
}
else if (re().is_full_seq(r) ||
re().is_empty(r)) {
result = r;
return BR_DONE;
return expr_ref(r, m());
}
else if (re().is_to_re(r, r1)) {
// r1 is a string here (not a regexp)
expr_ref hd(m()), tl(m());
if (get_head_tail(r1, hd, tl)) {
// head must be equal; if so, derivative is tail
result = re_and(m().mk_eq(ele, hd),re().mk_to_re(tl));
return BR_REWRITE2;
return re_and(m().mk_eq(ele, hd), re().mk_to_re(tl));
}
else if (str().is_empty(r1)) {
result = re().mk_empty(m().get_sort(r));
return BR_DONE;
return mk_empty();
}
else {
return BR_FAILED;
return expr_ref(re().mk_derivative(ele, r), m());
}
}
else if (re().is_reverse(r, r1) && re().is_to_re(r1, r2)) {
// Reverses are rewritten so that the only derivative case is
// derivative of a reverse of a string. (All other cases stuck)
// This is analagous to the previous is_to_re case.
expr_ref hd(m()), tl(m());
if (get_head_tail_reversed(r2, hd, tl)) {
return re_and(m().mk_eq(ele, tl), re().mk_reverse(re().mk_to_re(hd)));
}
else if (str().is_empty(r2)) {
return mk_empty();
}
else {
return expr_ref(re().mk_derivative(ele, r), m());
}
}
else if (re().is_range(r, r1, r2)) {
@ -2410,220 +2540,39 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
if (s1.length() == 1 && s2.length() == 1) {
r1 = m_util.mk_char(s1[0]);
r2 = m_util.mk_char(s2[0]);
result = m().mk_and(m_util.mk_le(r1, ele), m_util.mk_le(ele, r2));
result = re_predicate(result, seq_sort);
return BR_REWRITE3;
return mk_der_inter(re_predicate(m_util.mk_le(r1, ele), seq_sort),
re_predicate(m_util.mk_le(ele, r2), seq_sort));
}
else {
result = re().mk_empty(m().get_sort(r));
return BR_DONE;
return mk_empty();
}
}
expr* e1 = nullptr, *e2 = nullptr;
if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) {
result = m().mk_and(m_util.mk_le(e1, ele), m_util.mk_le(ele, e2));
result = re_predicate(result, seq_sort);
return BR_REWRITE2;
return mk_der_inter(re_predicate(m_util.mk_le(e1, ele), seq_sort),
re_predicate(m_util.mk_le(ele, e2), seq_sort));
}
}
else if (re().is_full_char(r)) {
result = re().mk_to_re(str().mk_empty(seq_sort));
return BR_DONE;
return expr_ref(re().mk_to_re(str().mk_empty(seq_sort)), m());
}
else if (re().is_of_pred(r, p)) {
array_util array(m());
expr* args[2] = { p, ele };
result = array.mk_select(2, args);
result = re_predicate(result, seq_sort);
return BR_REWRITE2;
return re_predicate(result, seq_sort);
}
// stuck cases: re().is_derivative, variable, ...
// and re().is_reverse
return BR_FAILED;
// and re().is_reverse if the reverse is not applied to a string
return expr_ref(re().mk_derivative(ele, r), m());
}
/*
Combine two if-then-else expressions in BDD form.
Lift all ite expressions to the top level, safely
throttled to not blowup the size of the expression.
Definition of BDD form:
if-then-elses are pushed outwards
and sorted by condition ID (cond->get_id()), from largest on
the outside to smallest on the inside.
Duplicate nested conditions are eliminated.
Preconditions:
- EITHER k is a binary op code on REs (re.union, re.inter, etc.)
and cond is nullptr,
OR k is if-then-else (OP.ITE) and cond is the condition.
- a and b are in BDD form.
Postcondition: result is in BDD form.
if-then-elses are pushed outwards
and sorted by condition ID (cond->get_id()), from largest on
the outside to smallest on the inside.
Uses op cache (memoization) to avoid duplicating work for the same
pair of pointers.
*/
expr_ref seq_rewriter::combine_ites(decl_kind k, expr* a, expr* b, expr* cond) {
std::cout << "c";
expr_ref result(m_op_cache.find(k, a, b, cond), m());
if (result) {
std::cout << "(h) ";
return result;
}
std::cout << "(m) ";
std::cout << std::endl << "combine_ites: "
<< k << ", "
<< expr_ref(a, m()) << ", "
<< expr_ref(b, m()) << ", "
<< expr_ref(cond, m()) << std::endl;
SASSERT((k == OP_ITE) == (cond != nullptr));
expr *acond = nullptr, *a1 = nullptr, *a2 = nullptr,
*bcond = nullptr, *b1 = nullptr, *b2 = nullptr;
expr_ref result1(m()), result2(m());
if (k == OP_ITE) {
if (m().is_ite(a, acond, a1, a2) &&
cond->get_id() < acond->get_id()) {
std::cout << " case 1a" << std::endl;
// Push ITE inwards on first arg
result1 = combine_ites(k, a1, b, cond);
result2 = combine_ites(k, a2, b, cond);
result = combine_ites(k, result1, result2, acond);
}
else if (m().is_ite(a, acond, a1, a2) &&
cond == acond) {
std::cout << " case 1b" << std::endl;
// Collapse ITE on first arg
result = combine_ites(k, a1, b, cond);
}
else if (m().is_ite(b, bcond, b1, b2) &&
cond->get_id() < bcond->get_id()) {
// Push ITE inwards on second arg
std::cout << " case 1c" << std::endl;
result1 = combine_ites(k, a, b1, cond);
result2 = combine_ites(k, a, b2, cond);
result = combine_ites(k, result1, result2, bcond);
}
else if (m().is_ite(b, bcond, b1, b2) &&
cond == bcond) {
std::cout << " case 1d" << std::endl;
// Collapse ITE on second arg
result = combine_ites(k, a, b2, cond);
}
else {
// Apply ITE -- no simplification required
std::cout << " case 1e" << std::endl;
result = m().mk_ite(cond, a, b);
}
}
else if (m().is_ite(a, acond, a1, a2)) {
std::cout << " case 2" << std::endl;
// Push binary op inwards on first arg
result1 = combine_ites(k, a1, b, nullptr);
result2 = combine_ites(k, a2, b, nullptr);
result = combine_ites(OP_ITE, result1, result2, acond);
}
else if (m().is_ite(b, bcond, b1, b2)) {
std::cout << " case 3" << std::endl;
// Push binary op inwards on second arg
result1 = combine_ites(k, a, b1, nullptr);
result2 = combine_ites(k, a, b2, nullptr);
result = combine_ites(OP_ITE, result1, result2, bcond);
}
else {
std::cout << " case 4" << std::endl;
// Apply binary op (a and b are free of ITE)
result = m().mk_app(get_fid(), k, a, b);
}
// Save result before returning
m_op_cache.insert(k, a, b, cond, result);
std::cout << "combine result: " << result << std::endl;
return result;
}
/*
Lift if-then-else expressions to the top level, enforcing a BDD form.
Postcondition: result is in BDD form.
- Alternatively, if lift_over_union and/or lift_over_inter is false,
then result is a disjunction and/or conjunciton of expressions in
BDD form. (Even in this case, ITE is still lifted at lower levels,
just not at the top level.)
- Note that the result may not be fully simplified (particularly the
nested expressions inside if-then-else). Simplification should be
called afterwards.
Cost: Causes potential blowup in the size of an expression (when
expanded out), but keeps the representation compact (subexpressions
are shared).
Used by: the regex solver in seq_regex.cpp when dealing with
derivatives of a regex by a symbolic character. Enables efficient
representation in unfolding string in regex constraints.
*/
expr_ref seq_rewriter::lift_ites(expr* r, bool lift_over_union, bool lift_over_inter) {
std::cout << "l ";
decl_kind k = to_app(r)->get_decl_kind();
family_id fid = get_fid();
expr *r1 = nullptr, *r2 = nullptr, *cond = nullptr, *ele = nullptr;
unsigned lo = 0, hi = 0;
expr_ref result(m()), result1(m()), result2(m());
if ((re().is_union(r, r1, r2) && !lift_over_union) ||
(re().is_intersection(r, r1, r2) && !lift_over_inter)) {
// Preserve unions and/or intersections
result1 = lift_ites(r1, lift_over_union, lift_over_inter);
result2 = lift_ites(r2, lift_over_union, lift_over_inter);
result = m().mk_app(fid, k, r1, r2);
}
else if (m().is_ite(r, cond, r1, r2) ||
re().is_concat(r, r1, r2) ||
re().is_union(r, r1, r2) ||
re().is_intersection(r, r1, r2) ||
re().is_diff(r, r1, r2)) {
// Use combine_ites on the subresults
// Stop preserving unions and intersections
result1 = lift_ites(r1, true, true);
result2 = lift_ites(r2, true, true);
result = combine_ites(k, r1, r2, cond);
}
else if (re().is_star(r, r1) ||
re().is_plus(r, r1) ||
re().is_opt(r, r1) ||
re().is_complement(r, r1) ||
re().is_reverse(r, r1)) {
// Stop preserving unions and intersections
result1 = lift_ites(r1, true, true);
result = m().mk_app(fid, k, r1);
}
else if (re().is_derivative(r, ele, r1)) {
result1 = lift_ites(r1, true, true);
result = m().mk_app(fid, k, ele, r1);
}
else if (re().is_loop(r, r1, lo)) {
result1 = lift_ites(r1, true, true);
result = re().mk_loop(result1, lo);
}
else if (re().is_loop(r, r1, lo, hi)) {
result1 = lift_ites(r1, true, true);
result = re().mk_loop(result1, lo, hi);
}
else {
// is_full_seq, is_empty, is_to_re, is_range, is_full_char, is_of_pred
result = r;
}
std::cout << std::endl << "lift of: " << expr_ref(r, m()) << std::endl;
std::cout << " = " << result << std::endl;
return result;
}
/*
Lift all ite expressions to the top level, but
a different "safe" version which is throttled to not
blowup the size of the expression.
Note: this function does not ensure the same BDD form that lift_ites
ensures.
Note: this function does not ensure the same BDD form that is
used in the normal form for derivatives in mk_re_derivative.
*/
br_status seq_rewriter::lift_ites_throttled(func_decl* f, unsigned n, expr* const* args, expr_ref& result) {
expr* c = nullptr, *t = nullptr, *e = nullptr;
@ -2644,51 +2593,6 @@ br_status seq_rewriter::lift_ites_throttled(func_decl* f, unsigned n, expr* cons
return BR_FAILED;
}
// /*
// Rewrite rules for ITEs of regexes.
// ite(not c, r1, r2) -> ite(c, r2, r1)
// ite(c, ite(c, r1, r2), r3)) -> ite(c, r1, r3)
// ite(c, r1, ite(c, r2, r3)) -> ite(c, r1, r3)
// ite(c1, ite(c2, r1, r2), r3) where id of c1 < id of c2 ->
// ite(c2, ite(c1, r1, r3), ite(c1, r2, r3))
// ite(c1, r1, ite(c2, r2, r3)) where id of c1 < id of c2 ->
// ite(c2, ite(c1, r1, r2), ite(c1, r1, r3))
// */
// br_status seq_rewriter::rewrite_re_ite(expr* cond, expr* r1, expr* r2, expr_ref& result) {
// VERIFY(m_util.is_re(r1));
// VERIFY(m_util.is_re(r2));
// expr *c = nullptr, *ra = nullptr, *rb = nullptr;
// if (m().is_not(cond, c)) {
// result = m().mk_ite(c, r2, r1);
// return BR_REWRITE1;
// }
// if (m().is_ite(r1, c, ra, rb)) {
// if (m().are_equal(c, cond)) {
// result = m().mk_ite(cond, ra, r2);
// return BR_REWRITE1;
// }
// if (cond->get_id() < c->get_id()) {
// expr *result1 = m().mk_ite(cond, ra, r2);
// expr *result2 = m().mk_ite(cond, rb, r2);
// result = m().mk_ite(c, result1, result2);
// return BR_REWRITE2;
// }
// }
// if (m().is_ite(r2, c, ra, rb)) {
// if (m().are_equal(c, cond)) {
// result = m().mk_ite(cond, r1, rb);
// return BR_REWRITE1;
// }
// if (cond->get_id() < c->get_id()) {
// expr *result1 = m().mk_ite(cond, r1, ra);
// expr* result2 = m().mk_ite(cond, r1, rb);
// result = m().mk_ite(c, result1, result2);
// return BR_REWRITE2;
// }
// }
// return BR_DONE;
// }
/*
* pattern match against all ++ "abc" ++ all ++ "def" ++ all regexes.
*/
@ -2885,7 +2789,6 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
return BR_REWRITE_FULL;
}
#if 0
if (get_re_head_tail(b, hd, tl)) {
SASSERT(re().min_length(hd) == re().max_length(hd));
expr_ref len_hd(m_autil.mk_int(re().min_length(hd)), m());
@ -2906,7 +2809,6 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl));
return BR_REWRITE_FULL;
}
#endif
if (false && rewrite_contains_pattern(a, b, result))
return BR_REWRITE_FULL;
@ -2998,6 +2900,50 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
}
return BR_FAILED;
}
bool seq_rewriter::are_complements(expr* r1, expr* r2) const {
expr* r = nullptr;
if (re().is_complement(r1, r) && r == r2)
return true;
if (re().is_complement(r2, r) && r == r1)
return true;
return false;
}
/*
* basic subset checker.
*/
bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
// return false;
expr* ra1 = nullptr, *ra2 = nullptr, *ra3 = nullptr;
expr* rb1 = nullptr, *rb2 = nullptr, *rb3 = nullptr;
if (re().is_complement(r1, ra1) &&
re().is_complement(r2, rb1)) {
return is_subset(rb1, ra1);
}
auto is_concat = [&](expr* r, expr*& a, expr*& b, expr*& c) {
return re().is_concat(r, a, b) && re().is_concat(b, b, c);
};
while (true) {
if (r1 == r2)
return true;
if (re().is_full_seq(r2))
return true;
if (is_concat(r1, ra1, ra2, ra3) &&
is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) {
r1 = ra3;
r2 = rb3;
continue;
}
if (re().is_concat(r1, ra1, ra2) &&
re().is_concat(r2, rb1, rb2) && re().is_full_seq(rb1)) {
r1 = ra2;
continue;
}
return false;
}
}
/*
(a + a) = a
(a + eps) = a
@ -3032,18 +2978,66 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
result = b;
return BR_DONE;
}
auto mk_full = [&]() { return re().mk_full_seq(m().get_sort(a)); };
if (are_complements(a, b)) {
result = mk_full();
return BR_DONE;
}
expr* a1 = nullptr, *a2 = nullptr;
expr* b1 = nullptr, *b2 = nullptr;
// ensure union is right-associative
// and swap-sort entries
if (re().is_union(a, a1, a2)) {
result = re().mk_union(a1, re().mk_union(a2, b));
return BR_REWRITE2;
}
auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); };
if (re().is_union(b, b1, b2)) {
if (is_subset(a, b1)) {
result = b;
return BR_DONE;
}
if (is_subset(b1, a)) {
result = re().mk_union(a, b2);
return BR_REWRITE1;
}
if (are_complements(a, b1)) {
result = mk_full();
return BR_DONE;
}
if (get_id(a) > get_id(b1)) {
result = re().mk_union(b1, re().mk_union(a, b2));
return BR_REWRITE2;
}
}
else {
if (get_id(a) > get_id(b)) {
result = re().mk_union(b, a);
return BR_DONE;
}
if (is_subset(a, b)) {
result = b;
return BR_DONE;
}
if (is_subset(b, a)) {
result = a;
return BR_DONE;
}
}
return BR_FAILED;
}
/*
comp(intersect e1 e2) -> union comp(e1) comp(e2)
comp(union e1 e2) -> intersect comp(e1) comp(e2)
comp(none) = all
comp(all) = none
comp(none) -> all
comp(all) -> none
comp(comp(e1)) -> e1
comp(ite p e1 e2) -> ite p comp(e1) comp(e2)
*/
br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
expr* e1, *e2;
expr *cond = nullptr, *e1 = nullptr, *e2 = nullptr;
if (re().is_intersection(a, e1, e2)) {
result = re().mk_union(re().mk_complement(e1), re().mk_complement(e2));
return BR_REWRITE2;
@ -3060,10 +3054,13 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
result = re().mk_empty(m().get_sort(a));
return BR_DONE;
}
expr *a1 = nullptr, *a2 = nullptr, *cond = nullptr;
if (m().is_ite(a, cond, a1, a2)) {
result = m().mk_ite(cond, re().mk_complement(a1),
re().mk_complement(a2));
if (re().is_complement(a, e1)) {
result = e1;
return BR_DONE;
}
if (m().is_ite(a, cond, e1, e2)) {
result = m().mk_ite(cond, re().mk_complement(e1),
re().mk_complement(e2));
return BR_REWRITE2;
}
return BR_FAILED;
@ -3101,12 +3098,53 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) {
result = a;
return BR_DONE;
}
expr* ac = nullptr, *bc = nullptr;
if ((re().is_complement(a, ac) && ac == b) ||
(re().is_complement(b, bc) && bc == a)) {
result = re().mk_empty(m().get_sort(a));
auto mk_empty = [&]() { return re().mk_empty(m().get_sort(a)); };
if (are_complements(a, b)) {
result = mk_empty();
return BR_DONE;
}
expr* a1 = nullptr, *a2 = nullptr;
expr* b1 = nullptr, *b2 = nullptr;
// ensure intersection is right-associative
// and swap-sort entries
if (re().is_intersection(a, a1, a2)) {
result = re().mk_inter(a1, re().mk_inter(a2, b));
return BR_REWRITE2;
}
auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); };
if (re().is_intersection(b, b1, b2)) {
if (is_subset(b1, a)) {
result = b;
return BR_DONE;
}
if (is_subset(a, b1)) {
result = re().mk_inter(a, b2);
return BR_REWRITE1;
}
if (are_complements(a, b1)) {
result = mk_empty();
return BR_DONE;
}
if (get_id(a) > get_id(b1)) {
result = re().mk_inter(b1, re().mk_inter(a, b2));
return BR_REWRITE2;
}
}
else {
if (get_id(a) > get_id(b)) {
result = re().mk_inter(b, a);
return BR_DONE;
}
if (is_subset(a, b)) {
result = a;
return BR_DONE;
}
if (is_subset(b, a)) {
result = b;
return BR_DONE;
}
}
if (re().is_to_re(b))
std::swap(a, b);
expr* s = nullptr;
@ -3388,7 +3426,6 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
else
intersect(0, ch-1, ranges);
}
// TBD: case for negation of range (not (and (<= lo e) (<= e hi)))
else {
all_ranges = false;
break;
@ -3429,124 +3466,6 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
}
}
void seq_rewriter::get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result) {
expr_ref cond(m()), th(m()), el(m());
if (has_cofactor(r, cond, th, el)) {
conds.push_back(cond);
get_cofactors(th, conds, result);
conds.pop_back();
conds.push_back(mk_not(m(), cond));
get_cofactors(el, conds, result);
conds.pop_back();
}
else {
cond = mk_and(conds);
result.push_back(cond, r);
}
}
bool seq_rewriter::has_cofactor(expr* r, expr_ref& cond, expr_ref& th, expr_ref& el) {
if (m().is_ite(r)) {
cond = to_app(r)->get_arg(0);
th = to_app(r)->get_arg(1);
el = to_app(r)->get_arg(2);
return true;
}
expr_ref_vector trail(m()), args_th(m()), args_el(m());
expr* c = nullptr, *tt = nullptr, *ee = nullptr;
cond = nullptr;
obj_map<expr,expr*> cache_th, cache_el;
expr_mark no_cofactor, visited;
ptr_vector<expr> todo;
todo.push_back(r);
while (!todo.empty()) {
expr* e = todo.back();
if (visited.is_marked(e) || !is_app(e)) {
todo.pop_back();
continue;
}
app* a = to_app(e);
if (m().is_ite(e, c, tt, ee)) {
if (!cond) {
cond = c;
cache_th.insert(a, tt);
cache_el.insert(a, ee);
}
else if (cond == c) {
cache_th.insert(a, tt);
cache_el.insert(a, ee);
}
else {
no_cofactor.mark(a);
}
visited.mark(e, true);
todo.pop_back();
continue;
}
if (a->get_family_id() != u().get_family_id()) {
visited.mark(e, true);
no_cofactor.mark(e, true);
todo.pop_back();
continue;
}
switch (a->get_decl_kind()) {
case OP_RE_CONCAT:
case OP_RE_UNION:
case OP_RE_INTERSECT:
case OP_RE_COMPLEMENT:
break;
case OP_RE_STAR:
case OP_RE_LOOP:
default:
visited.mark(e, true);
no_cofactor.mark(e, true);
continue;
}
args_th.reset();
args_el.reset();
bool has_cof = false;
for (expr* arg : *a) {
if (no_cofactor.is_marked(arg)) {
args_th.push_back(arg);
args_el.push_back(arg);
}
else if (cache_th.contains(arg)) {
args_th.push_back(cache_th[arg]);
args_el.push_back(cache_el[arg]);
has_cof = true;
}
else {
todo.push_back(arg);
}
}
if (args_th.size() == a->get_num_args()) {
if (has_cof) {
th = mk_app(a->get_decl(), args_th);
el = mk_app(a->get_decl(), args_el);
trail.push_back(th);
trail.push_back(el);
cache_th.insert(a, th);
cache_el.insert(a, el);
}
else {
no_cofactor.mark(a, true);
}
visited.mark(e, true);
todo.pop_back();
}
}
SASSERT(cond == !no_cofactor.is_marked(r));
if (cond) {
th = cache_th[r];
el = cache_el[r];
return true;
}
else {
return false;
}
}
br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) {
expr* r1, *r2, *r3, *r4;
zstring s1, s2;

32
src/ast/rewriter/seq_rewriter.h
View file

@ -182,6 +182,18 @@ class seq_rewriter {
expr_ref mk_seq_concat(expr* a, expr* b);
expr_ref mk_der_op(decl_kind k, expr* a, expr* b);
expr_ref mk_der_op_rec(decl_kind k, expr* a, expr* b);
expr_ref mk_der_concat(expr* a, expr* b);
expr_ref mk_der_union(expr* a, expr* b);
expr_ref mk_der_inter(expr* a, expr* b);
expr_ref mk_der_compl(expr* a);
expr_ref mk_derivative(expr* ele, expr* r);
expr_ref mk_derivative_rec(expr* ele, expr* r);
bool are_complements(expr* r1, expr* r2) const;
bool is_subset(expr* r1, expr* r2) const;
br_status mk_seq_unit(expr* e, expr_ref& result);
br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
br_status mk_seq_length(expr* a, expr_ref& result);
@ -230,6 +242,7 @@ class seq_rewriter {
bool rewrite_contains_pattern(expr* a, expr* b, expr_ref& result);
br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result);
br_status mk_eq_helper(expr* a, expr* b, expr_ref& result);
bool cannot_contain_prefix(expr* a, expr* b);
bool cannot_contain_suffix(expr* a, expr* b);
@ -265,15 +278,15 @@ class seq_rewriter {
class seq_util::str& str() { return u().str; }
class seq_util::str const& str() const { return u().str; }
void get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result);
expr_ref is_nullable_rec(expr* r);
void intersect(unsigned lo, unsigned hi, svector<std::pair<unsigned, unsigned>>& ranges);
expr_ref combine_ites(decl_kind k, expr* a, expr* b, expr* cond);
br_status lift_ites_throttled(func_decl* f, unsigned n, expr* const* args, expr_ref& result);
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m), m_re2aut(m), m_op_cache(m), m_es(m), m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
m_util(m), m_autil(m), m_re2aut(m), m_op_cache(m), m_es(m),
m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
}
ast_manager & m() const { return m_util.get_manager(); }
family_id get_fid() const { return m_util.get_family_id(); }
@ -314,23 +327,12 @@ public:
void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs);
// Memoized checking for acceptance of the empty string
// Check for acceptance of the empty string
expr_ref is_nullable(expr* r);
expr_ref is_nullable_rec(expr* r);
// utilities for cofactors of if-then-else expressions
bool has_cofactor(expr* r, expr_ref& cond, expr_ref& th, expr_ref& el);
void get_cofactors(expr* r, expr_ref_pair_vector& result) {
expr_ref_vector conds(m());
get_cofactors(r, conds, result);
}
// heuristic elimination of element from condition that comes form a derivative.
// special case optimization for conjunctions of equalities, disequalities and ranges.
void elim_condition(expr* elem, expr_ref& cond);
// if-then-else rewriting support (for REs)
expr_ref lift_ites(expr* r, bool lift_over_union = true, bool lift_over_inter = true);
};
#endif

2
src/ast/rewriter/th_rewriter.cpp
View file

@ -203,7 +203,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
if (st != BR_FAILED)
return st;
}
if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) {
if ((k == OP_AND || k == OP_OR /*|| k == OP_EQ*/) && m_seq_rw.u().has_re()) {
st = m_seq_rw.mk_bool_app(f, num, args, result);
if (st != BR_FAILED)
return st;

11
src/opt/opt_context.cpp
View file

@ -367,6 +367,7 @@ namespace opt {
void context::fix_model(model_ref& mdl) {
if (mdl && !m_model_fixed.contains(mdl.get())) {
TRACE("opt", m_fm->display(tout << "fix-model\n");
tout << *mdl << "\n";
if (m_model_converter) m_model_converter->display(tout););
(*m_fm)(mdl);
apply(m_model_converter, mdl);
@ -482,6 +483,7 @@ namespace opt {
lbool context::execute_box() {
if (m_box_index < m_box_models.size()) {
m_model = m_box_models[m_box_index];
CTRACE("opt", m_model, tout << *m_model << "\n";);
++m_box_index;
return l_true;
}
@ -505,12 +507,15 @@ namespace opt {
m_box_models.push_back(m_model.get());
}
else {
m_box_models.push_back(m_optsmt.get_model(j));
model* mdl = m_optsmt.get_model(j);
if (!mdl) mdl = m_model.get();
m_box_models.push_back(mdl);
++j;
}
}
if (r == l_true && !m_box_models.empty()) {
m_model = m_box_models[0];
CTRACE("opt", m_model, tout << *m_model << "\n";);
}
return r;
}
@ -787,6 +792,7 @@ namespace opt {
void context::normalize(expr_ref_vector const& asms) {
expr_ref_vector fmls(m);
m_model_converter = nullptr;
to_fmls(fmls);
simplify_fmls(fmls, asms);
from_fmls(fmls);
@ -1248,7 +1254,7 @@ namespace opt {
case O_MAXSMT: {
maxsmt& ms = *m_maxsmts.find(obj.m_id);
for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
ms.add(obj.m_terms[j].get(), obj.m_weights[j]);
ms.add(obj.m_terms.get(j), obj.m_weights[j]);
}
break;
}
@ -1468,6 +1474,7 @@ namespace opt {
void context::clear_state() {
m_pareto = nullptr;
m_box_index = UINT_MAX;
m_box_models.reset();
m_model.reset();
m_model_fixed.reset();
m_core.reset();

5
src/opt/optsmt.cpp
View file

@ -469,6 +469,7 @@ namespace opt {
return l_true;
}
void optsmt::setup(opt_solver& solver) {
m_s = &solver;
solver.reset_objectives();
@ -577,7 +578,9 @@ namespace opt {
m_upper.reset();
m_objs.reset();
m_vars.reset();
m_model.reset();
m_model.reset();
m_best_model = nullptr;
m_models.reset();
m_lower_fmls.reset();
m_s = nullptr;
}

6
src/sat/ba_solver.cpp
View file

@ -330,7 +330,7 @@ namespace sat {
m_stats.m_num_conflicts++;
TRACE("ba", display(tout, c, true); );
if (!validate_conflict(c)) {
display(std::cout, c, true);
IF_VERBOSE(0, display(verbose_stream(), c, true));
UNREACHABLE();
}
SASSERT(validate_conflict(c));
@ -2941,6 +2941,8 @@ namespace sat {
void ba_solver::pre_simplify() {
VERIFY(s().at_base_lvl());
if (s().inconsistent())
return;
m_constraint_removed = false;
xor_finder xf(s());
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) pre_simplify(xf, *m_constraints[i]);
@ -2983,6 +2985,8 @@ namespace sat {
void ba_solver::simplify() {
if (!s().at_base_lvl()) s().pop_to_base_level();
if (s().inconsistent())
return;
unsigned trail_sz, count = 0;
do {
trail_sz = s().init_trail_size();

208
src/smt/seq_regex.cpp
View file

@ -118,11 +118,9 @@ namespace smt {
if (coallesce_in_re(lit))
return;
#if 1
// Enable/disable to test effect
if (is_string_equality(lit))
return;
#endif
//
// TBD s in R => R != {}
// non-emptiness enforcement could instead of here,
@ -151,32 +149,6 @@ namespace smt {
m_to_propagate.push_back(lit);
}
// s in R[if(p,R1,R2)] & p => s in R[R1]
// s in R[if(p,R1,R2)] & ~p => s in R[R2]
bool seq_regex::unfold_cofactors(expr_ref& r, literal_vector& conds) {
expr_ref cond(m), tt(m), el(m);
while (seq_rw().has_cofactor(r, cond, tt, el)) {
rewrite(cond);
literal lcond = th.mk_literal(cond);
switch (ctx.get_assignment(lcond)) {
case l_true:
conds.push_back(~lcond);
r = tt;
break;
case l_false:
conds.push_back(lcond);
r = el;
break;
case l_undef:
ctx.mark_as_relevant(lcond);
return false;
}
rewrite(r);
}
return true;
}
/**
* Propagate the atom (accept s i r)
*
@ -184,6 +156,8 @@ namespace smt {
*
* (accept s i r[if(c,r1,r2)]) & c => (accept s i r[r1])
* (accept s i r[if(c,r1,r2)]) & ~c => (accept s i r[r2])
* (accept s i r) & nullable(r) => len(s) >= i
* (accept s i r) & ~nullable(r) => len(s) >= i + 1
* (accept s i r) & len(s) <= i => nullable(r)
* (accept s i r) & len(s) > i => (accept s (+ i 1) D(nth(s,i), r))
*/
@ -195,53 +169,121 @@ namespace smt {
expr* e = ctx.bool_var2expr(lit.var());
unsigned idx = 0;
VERIFY(sk().is_accept(e, s, i, idx, r));
expr_ref is_nullable(m), d(r, m);
TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
std::cout << "P ";
// << mk_pp(e, m) << std::endl;
if (re().is_empty(r)) {
th.add_axiom(~lit);
return true;
}
if (block_unfolding(lit, idx))
return true;
propagate_nullable(lit, e, s, idx, r);
return propagate_derivative(lit, e, s, i, idx, r);
}
/**
Implement the two axioms as propagations:
(accept s i r) => len(s) >= i
(accept s i r) & ~nullable(r) => len(s) >= i + 1
*/
void seq_regex::propagate_nullable(literal lit, expr* e, expr* s, unsigned idx, expr* r) {
expr_ref is_nullable = seq_rw().is_nullable(r);
rewrite(is_nullable);
literal len_s_ge_i = th.m_ax.mk_ge(th.mk_len(s), idx);
if (m.is_true(is_nullable)) {
th.propagate_lit(nullptr, 1,&lit, len_s_ge_i);
}
else if (m.is_false(is_nullable)) {
th.propagate_lit(nullptr, 1, &lit, th.m_ax.mk_ge(th.mk_len(s), idx + 1));
}
else {
literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx);
switch (ctx.get_assignment(len_s_le_i)) {
case l_undef:
th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable));
break;
case l_true: {
literal lits[2] = { lit, len_s_le_i };
th.propagate_lit(nullptr, 2, lits, th.mk_literal(is_nullable));
break;
}
case l_false:
break;
}
th.propagate_lit(nullptr, 1, &lit, len_s_ge_i);
}
}
bool seq_regex::propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r) {
// (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds
expr_ref d(m);
expr_ref head = th.mk_nth(s, i);
d = derivative_wrapper(m.mk_var(0, m.get_sort(head)), r);
// timer tm;
// std::cout << d->get_id() << " " << tm.get_seconds() << "\n";
// if (tm.get_seconds() > 1)
// std::cout << d << "\n";
// std::cout.flush();
literal_vector conds;
conds.push_back(~lit);
if (!unfold_cofactors(d, conds))
return false;
if (re().is_empty(d)) {
th.add_axiom(conds);
return true;
conds.push_back(th.m_ax.mk_le(th.mk_len(s), idx));
expr* cond = nullptr, *tt = nullptr, *el = nullptr;
var_subst subst(m);
expr_ref_vector sub(m);
sub.push_back(head);
// s in R[if(p,R1,R2)] & p => s in R[R1]
// s in R[if(p,R1,R2)] & ~p => s in R[R2]
while (m.is_ite(d, cond, tt, el)) {
literal lcond = th.mk_literal(subst(cond, sub));
switch (ctx.get_assignment(lcond)) {
case l_true:
conds.push_back(~lcond);
d = tt;
break;
case l_false:
conds.push_back(lcond);
d = el;
break;
case l_undef:
#if 1
ctx.mark_as_relevant(lcond);
return false;
#else
if (re().is_empty(tt)) {
literal_vector ensure_false(conds);
ensure_false.push_back(~lcond);
th.add_axiom(ensure_false);
conds.push_back(lcond);
d = el;
}
else if (re().is_empty(el)) {
literal_vector ensure_true(conds);
ensure_true.push_back(lcond);
th.add_axiom(ensure_true);
conds.push_back(~lcond);
d = tt;
}
else {
ctx.mark_as_relevant(lcond);
return false;
}
break;
#endif
}
}
// s in R & len(s) <= i => nullable(R)
literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx);
switch (ctx.get_assignment(len_s_le_i)) {
case l_undef:
ctx.mark_as_relevant(len_s_le_i);
return false;
case l_true:
is_nullable = seq_rw().is_nullable(d);
rewrite(is_nullable);
conds.push_back(~len_s_le_i);
conds.push_back(th.mk_literal(is_nullable));
th.add_axiom(conds);
return true;
case l_false:
break;
}
// (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds
expr_ref head = th.mk_nth(s, i);
d = derivative_wrapper(head, r);
literal acc_next = th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d));
conds.push_back(len_s_le_i);
conds.push_back(acc_next);
th.add_axiom(conds);
// at this point there should be no free variables as the ites are at top-level.
if (!re().is_empty(d))
conds.push_back(th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d)));
th.add_axiom(conds);
TRACE("seq", tout << "unfold " << head << "\n" << mk_pp(r, m) << "\n";);
return true;
}
@ -264,7 +306,6 @@ namespace smt {
* within the same Regex.
*/
bool seq_regex::coallesce_in_re(literal lit) {
// initially disable this
return false;
expr* s = nullptr, *r = nullptr;
expr* e = ctx.bool_var2expr(lit.var());
@ -273,10 +314,10 @@ namespace smt {
literal_vector lits;
for (unsigned i = 0; i < m_s_in_re.size(); ++i) {
auto const& entry = m_s_in_re[i];
enode* n1 = th.ensure_enode(entry.m_s);
enode* n2 = th.ensure_enode(s);
if (!entry.m_active)
continue;
enode* n1 = th.ensure_enode(entry.m_s);
enode* n2 = th.ensure_enode(s);
if (n1->get_root() != n2->get_root())
continue;
if (entry.m_re == regex)
@ -284,7 +325,7 @@ namespace smt {
th.m_trail_stack.push(vector_value_trail<theory_seq, s_in_re, true>(m_s_in_re, i));
m_s_in_re[i].m_active = false;
IF_VERBOSE(11, verbose_stream() << "intersect " << regex << " " <<
IF_VERBOSE(11, verbose_stream() << "Intersect " << regex << " " <<
mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n";);
regex = re().mk_inter(entry.m_re, regex);
rewrite(regex);
@ -315,17 +356,14 @@ namespace smt {
}
/*
Memoized(TODO) wrapper around the regex symbolic derivative.
Also ensures that the derivative is written in a normalized form
Wrapper around the regex symbolic derivative from the rewriter.
Ensures that the derivative is written in a normalized BDD form
with optimizations for if-then-else expressions involving the head.
*/
expr_ref seq_regex::derivative_wrapper(expr* hd, expr* r) {
std::cout << "D ";
expr_ref result = expr_ref(re().mk_derivative(hd, r), m);
rewrite(result);
// don't lift over unions
result = seq_rw().lift_ites(result); // false, true);
rewrite(result);
std::cout << std::endl << "Derivative result: " << result << std::endl;
return result;
}
@ -378,7 +416,7 @@ namespace smt {
if (null_lit != false_literal)
lits.push_back(null_lit);
expr_ref_pair_vector cofactors(m);
seq_rw().get_cofactors(d, cofactors);
get_cofactors(d, cofactors);
for (auto const& p : cofactors) {
if (is_member(p.second, u))
continue;
@ -395,6 +433,21 @@ namespace smt {
th.add_axiom(lits);
}
void seq_regex::get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result) {
expr* cond = nullptr, *th = nullptr, *el = nullptr;
if (m.is_ite(r, cond, th, el)) {
conds.push_back(cond);
get_cofactors(th, conds, result);
conds.pop_back();
conds.push_back(mk_not(m, cond));
get_cofactors(el, conds, result);
conds.pop_back();
}
else {
cond = mk_and(conds);
result.push_back(cond, r);
}
}
/*
is_empty(r, u) => ~is_nullable(r)
@ -418,10 +471,7 @@ namespace smt {
d = derivative_wrapper(hd, r);
literal_vector lits;
expr_ref_pair_vector cofactors(m);
seq_rw().get_cofactors(d, cofactors);
// is_empty(r, u) => forall hd . cond => is_empty(r1, u union r)
get_cofactors(d, cofactors);
for (auto const& p : cofactors) {
if (is_member(p.second, u))
continue;

13
src/smt/seq_regex.h
View file

@ -59,18 +59,27 @@ namespace smt {
bool block_unfolding(literal lit, unsigned i);
void propagate_nullable(literal lit, expr* e, expr* s, unsigned idx, expr* r);
bool propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r);
expr_ref mk_first(expr* r);
expr_ref unroll_non_empty(expr* r, expr_mark& seen, unsigned depth);
bool unfold_cofactors(expr_ref& r, literal_vector& conds);
bool is_member(expr* r, expr* u);
expr_ref symmetric_diff(expr* r1, expr* r2);
expr_ref derivative_wrapper(expr* hd, expr* r);
void get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result);
void get_cofactors(expr* r, expr_ref_pair_vector& result) {
expr_ref_vector conds(m);
get_cofactors(r, conds, result);
}
public:
seq_regex(theory_seq& th);

23
src/smt/theory_fpa.cpp
View file

@ -436,7 +436,8 @@ namespace smt {
ctx.internalize(term->get_args(), term->get_num_args(), false);
enode * e = ctx.mk_enode(term, false, false, true);
enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) :
ctx.mk_enode(term, false, false, true);
if (!is_attached_to_var(e)) {
attach_new_th_var(e);
@ -503,16 +504,14 @@ namespace smt {
fpa_util & fu = m_fpa_util;
expr_ref xe(m), ye(m);
xe = e_x->get_owner();
ye = e_y->get_owner();
expr * xe = e_x->get_owner();
expr * ye = e_y->get_owner();
if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye))
return;
expr_ref xc(m), yc(m);
xc = convert(xe);
yc = convert(ye);
expr_ref xc = convert(xe);
expr_ref yc = convert(ye);
TRACE("t_fpa_detail", tout << "xc = " << mk_ismt2_pp(xc, m) << std::endl <<
"yc = " << mk_ismt2_pp(yc, m) << std::endl;);
@ -546,16 +545,14 @@ namespace smt {
fpa_util & fu = m_fpa_util;
expr_ref xe(m), ye(m);
xe = e_x->get_owner();
ye = e_y->get_owner();
expr * xe = e_x->get_owner();
expr * ye = e_y->get_owner();
if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye))
return;
expr_ref xc(m), yc(m);
xc = convert(xe);
yc = convert(ye);
expr_ref xc = convert(xe);
expr_ref yc = convert(ye);
expr_ref c(m);