mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3 into polysat

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-11 09:21:58 -07:00
commit 524ebed44f
14 changed files with 361 additions and 102 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -285,6 +285,7 @@ void OP(unsigned num_args, expr * const * args, expr_ref & result) { \
MK_BIN_AC_REDUCE(reduce_add, reduce_bin_add, mk_adder);
MK_BIN_AC_REDUCE(reduce_mul, reduce_bin_mul, mk_multiplier);
MK_BIN_AC_REDUCE(reduce_and, reduce_bin_and, mk_and);
MK_BIN_AC_REDUCE(reduce_or, reduce_bin_or, mk_or);
MK_BIN_AC_REDUCE(reduce_xor, reduce_bin_xor, mk_xor);
@ -357,8 +358,11 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
result = mk_mkbv(m_out);
}
void throw_unsupported() {
throw rewriter_exception("operator is not supported, you must simplify the goal before applying bit-blasting");
void throw_unsupported(func_decl * f) {
std::string msg = "operator ";
msg += f->get_name().str();
msg += " is not supported, you must simplify the goal before applying bit-blasting";
throw rewriter_exception(std::move(msg));
}
void blast_bv_term(expr * t, expr_ref & result, proof_ref & result_pr) {
@ -424,7 +428,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
case OP_BUREM:
case OP_BSMOD:
if (m_blast_mul)
throw_unsupported(); // must simplify to DIV_I AND DIV0
throw_unsupported(f); // must simplify to DIV_I AND DIV0
return BR_FAILED; // keep them
case OP_BSDIV0:
@ -472,6 +476,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
SASSERT(num == 2);
reduce_sle(args[0], args[1], result);
return BR_DONE;
case OP_BAND:
reduce_and(num, args, result);
return BR_DONE;
case OP_BOR:
reduce_or(num, args, result);
return BR_DONE;
@ -545,7 +552,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
default:
TRACE("bit_blaster", tout << "non-supported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
throw_unsupported();
throw_unsupported(f);
}
}

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

@ -1043,12 +1043,19 @@ namespace seq {
}
/**
suffix(s, t):
- the sequence s is a suffix of t.
suffix(s, t) => s = seq.suffix_inv(s, t) + t
Positive case is handled by the solver when the atom is asserted
suffix(s, t) => t = seq.suffix_inv(s, t) + s
Negative case is handled by axioms when the negation of the atom is asserted
~suffix(s, t) => len(s) > len(t) or s = y(s, t) + unit(c(s, t)) + x(s, t)
~suffix(s, t) => len(s) > len(t) or t = z(s, t) + unit(d(s, t)) + x(s, t)
~suffix(s, t) => len(s) > len(t) or c(s,t) != d(s,t)
Symmetric axioms are provided for prefix
*/
void axioms::suffix_axiom(expr* e) {
@ -1101,7 +1108,7 @@ namespace seq {
expr_ref c = m_sk.mk("seq.prefix.c", s, t, char_sort);
expr_ref d = m_sk.mk("seq.prefix.d", s, t, char_sort);
add_clause(lit, s_gt_t, mk_seq_eq(s, mk_concat(x, seq.str.mk_unit(c), y)));
add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)), mk_seq_eq(t, x));
add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)));
add_clause(lit, s_gt_t, ~mk_eq(c, d));
#endif
}

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

@ -14,6 +14,7 @@ Author:
Nikolaj Bjorner (nbjorner) 2015-12-5
Murphy Berzish 2017-02-21
Caleb Stanford 2020-07-07
Margus Veanes 2021
--*/
@ -872,6 +873,65 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
return BR_FAILED;
}
/*
* In general constructs nth(t,0) but if t = substring(s,j,..) then simplifies to nth(s,j)
* This method assumes that |t| > 0.
*/
expr_ref seq_rewriter::mk_seq_first(expr* t) {
expr_ref result(m());
expr* s, * j, * k;
if (str().is_extract(t, s, j, k))
result = str().mk_nth_i(s, j);
else
result = str().mk_nth_i(t, m_autil.mk_int(0));
return result;
}
/*
* In general constructs substring(t,1,|t|-1) but if t = substring(s,j,k) then simplifies to substring(s,j+1,k-1)
* This method assumes that |t| > 0.
*/
expr_ref seq_rewriter::mk_seq_rest(expr* t) {
expr_ref result(m());
expr* s, * j, * k;
expr_ref one(m_autil.mk_int(1), m());
if (str().is_extract(t, s, j, k))
result = str().mk_substr(s, m_autil.mk_add(j, one), m_autil.mk_sub(k, one));
else
result = str().mk_substr(t, one, m_autil.mk_sub(str().mk_length(t), one));
return result;
}
/*
* In general constructs nth(t,|t|-1) but if t = substring(s,j,k) then simplifies to nth(s,j+k-1)
* This method assumes that |t| > 0.
*/
expr_ref seq_rewriter::mk_seq_last(expr* t) {
expr_ref result(m());
expr* s, * j, * k;
expr_ref one(m_autil.mk_int(1), m());
if (str().is_extract(t, s, j, k))
result = str().mk_nth_i(s, m_autil.mk_sub(m_autil.mk_add(j, k), one));
else
result = str().mk_nth_i(t, m_autil.mk_sub(str().mk_length(t), one));
return result;
}
/*
* In general constructs substring(t,0,|t|-1) but if t = substring(s,j,k) then simplifies to substring(s,j,k-1)
* This method assumes that |t| > 0 holds.
*/
expr_ref seq_rewriter::mk_seq_butlast(expr* t) {
expr_ref result(m());
expr* s, * j, * k;
expr_ref one(m_autil.mk_int(1), m());
if (str().is_extract(t, s, j, k))
result = str().mk_substr(s, j, m_autil.mk_sub(k, one));
else
result = str().mk_substr(t, m_autil.mk_int(0), m_autil.mk_sub(str().mk_length(t), one));
return result;
}
/*
Lift all ite expressions to the top level, safely
throttled to not blowup the size of the expression.
@ -1890,16 +1950,16 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
}
if (a == b) {
result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(a->get_sort()), c);
return BR_REWRITE1;
return BR_REWRITE2;
}
zstring s1, s2;
expr_ref_vector strs(m());
if (str().is_string(a, s1) && str().is_string(b, s2)) {
SASSERT(s2.length() > 0);
if (s1.length() < s2.length()) {
result = a;
return BR_DONE;
}
expr_ref_vector strs(m());
for (unsigned i = 0; i < s1.length(); ++i) {
if (s1.length() >= s2.length() + i &&
s2 == s1.extract(i, s2.length())) {
@ -1912,11 +1972,63 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
result = str().mk_concat(strs, a->get_sort());
return BR_REWRITE_FULL;
}
// TBD: add case when a, b are concatenation of units that are values.
// in this case we can use a similar loop as for strings.
expr_ref_vector a_vals(m());
expr_ref_vector b_vals(m());
if (try_get_unit_values(a, a_vals) && try_get_unit_values(b, b_vals)) {
replace_all_subvectors(a_vals, b_vals, c, strs);
result = str().mk_concat(strs, a->get_sort());
return BR_REWRITE_FULL;
}
//TODO: the case when a is a unit or concatenation of units while b is a string
//or the other way around -- if that situation is possible at all -- is similar to the above
return BR_FAILED;
}
/*
* Returns false if s is not a single unit value or concatenation of unit values.
* Else extracts the units from s into vals and returns true.
*/
bool seq_rewriter::try_get_unit_values(expr* s, expr_ref_vector& vals) {
expr* h, * t, * v;
t = s;
//collect all unit values from s, if not all elements are unit-values then fail
while (str().is_concat(t, h, t))
if (str().is_unit(h, v) && m().is_value(v))
vals.push_back(h);
else
return false;
//add the last element
if (str().is_unit(t, v) && m().is_value(v))
vals.push_back(t);
else
return false;
return true;
}
/*
* Replace all subvectors of b in a by c
*/
void seq_rewriter::replace_all_subvectors(expr_ref_vector const& a, expr_ref_vector const& b, expr* c, expr_ref_vector& result) {
unsigned int i = 0;
unsigned int k = b.size();
while (i + k <= a.size()) {
//if a[i..i+k-1] equals b then replace it by c and inceremnt i by k
unsigned j = 0;
while (j < k && b[j] == a[i + j])
++j;
if (j < k) //the equality failed
result.push_back(a[i++]);
else { //the equality succeeded
result.push_back(c);
i += k;
}
}
//add the trailing elements from a
while (i < a.size())
result.push_back(a[i++]);
}
br_status seq_rewriter::mk_seq_replace_re_all(expr* a, expr* b, expr* c, expr_ref& result) {
return BR_FAILED;
}
@ -2521,12 +2633,18 @@ bool seq_rewriter::get_re_head_tail_reversed(expr* r, expr_ref& head, expr_ref&
if (re().is_concat(r, r1, r2)) {
unsigned len = re().min_length(r2);
if (len != UINT_MAX && re().max_length(r2) == len) {
head = r1;
tail = r2;
if (get_re_head_tail_reversed(r1, head, tail))
// left associative binding of concat
tail = mk_re_append(tail, r2);
else {
// right associative binding of concat
head = r1;
tail = r2;
}
return true;
}
if (get_re_head_tail_reversed(r2, head, tail)) {
head = re().mk_concat(r1, head);
head = mk_re_append(r1, head);
return true;
}
}
@ -3059,7 +3177,8 @@ expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) {
return result;
}
// Order with higher IDs on the outside
if (get_id(ca) < get_id(cb)) {
bool is_symmetric = k == OP_RE_UNION || k == OP_RE_INTERSECT;
if (is_symmetric && get_id(ca) < get_id(cb)) {
std::swap(a, b);
std::swap(ca, cb);
std::swap(notca, notcb);
@ -3348,7 +3467,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
//while mk_empty() = [], because deriv(epsilon) = [] = nothing
return mk_empty();
}
else if (str().is_itos(r1, r2)) {
else if (str().is_itos(r1)) {
//
// here r1 = (str.from_int r2) and r2 is non-ground
// or else the expression would have been simplified earlier
@ -3356,27 +3475,46 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
// '0' <= elem <= '9'
// if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else []
//
hd = str().mk_nth_i(r1, m_autil.mk_int(0));
m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), m().mk_eq(hd, ele), result);
tl = re().mk_to_re(str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1))));
hd = mk_seq_first(r1);
m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')),
m().mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele)), result);
tl = re().mk_to_re(mk_seq_rest(r1));
return re_and(result, tl);
}
else {
// recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence
// construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else []))
hd = mk_seq_first(r1);
m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result);
tl = re().mk_to_re(mk_seq_rest(r1));
return re_and(result, tl);
}
}
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)) {
// Use mk_der_cond to normalize
STRACE("seq_verbose", tout << "deriv reverse to_re" << std::endl;);
result = m().mk_eq(ele, tl);
result = mk_der_cond(result, ele, seq_sort);
result = mk_der_concat(result, re().mk_reverse(re().mk_to_re(hd)));
return result;
}
else if (str().is_empty(r2)) {
return mk_empty();
else if (re().is_reverse(r, r1)) {
if (re().is_to_re(r1, r2)) {
// First try to exctract hd and tl such that r = hd ++ tl and |tl|=1
expr_ref hd(m()), tl(m());
if (get_head_tail_reversed(r2, hd, tl)) {
// Use mk_der_cond to normalize
STRACE("seq_verbose", tout << "deriv reverse to_re" << std::endl;);
result = m().mk_eq(ele, tl);
result = mk_der_cond(result, ele, seq_sort);
result = mk_der_concat(result, re().mk_reverse(re().mk_to_re(hd)));
return result;
}
else if (str().is_empty(r2)) {
return mk_empty();
}
else {
// construct the term (if (r2 != () and (ele = (last r2)) then reverse(to_re (butlast r2)) else []))
// hd = first of reverse(r2) i.e. last of r2
// tl = rest of reverse(r2) i.e. butlast of r2
//hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), m_autil.mk_int(1)));
hd = mk_seq_last(r2);
m_br.mk_and(m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result);
tl = re().mk_to_re(mk_seq_butlast(r2));
return re_and(result, re().mk_reverse(tl));
}
}
}
else if (re().is_range(r, r1, r2)) {
@ -3423,10 +3561,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
STRACE("seq_verbose", tout << "deriv of_pred" << std::endl;);
return mk_der_cond(result, ele, seq_sort);
}
// stuck cases: re.derivative, variable,
// str.to_re if the head of the string can't be obtained,
// and re.reverse if not applied to a string or if the tail char
// of the string can't be obtained
// stuck cases: re.derivative, re variable,
return expr_ref(re().mk_derivative(ele, r), m());
}
@ -3662,12 +3797,14 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
}
if (get_re_head_tail_reversed(b, hd, tl)) {
SASSERT(re().min_length(tl) == re().max_length(tl));
expr_ref len_tl(m_autil.mk_int(re().min_length(tl)), m());
expr_ref len_tl(m_autil.mk_int(re().min_length(tl)), m());
expr_ref len_a(str().mk_length(a), m());
expr_ref len_hd(m_autil.mk_sub(len_a, len_tl), m());
expr* s = nullptr;
result = m().mk_and(m_autil.mk_ge(len_a, len_tl),
re().mk_in_re(str().mk_substr(a, m_autil.mk_int(0), len_hd), hd),
re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl));
re().mk_in_re(str().mk_substr(a, m_autil.mk_int(0), len_hd), hd),
(re().is_to_re(tl, s) ? m().mk_eq(s, str().mk_substr(a, len_hd, len_tl)) :
re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)));
return BR_REWRITE_FULL;
}
@ -4974,6 +5111,12 @@ bool seq_rewriter::reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs,
str().is_itos(ls.get(0), n) &&
is_string(rs.size(), rs.data(), s)) {
std::string s1 = s.encode();
for (auto c : s1) {
if (!('0' <= c && c <= '9'))
return false;
}
if (s1.size() > 1 && s1[0] == '0')
return false;
try {
rational r(s1.c_str());
if (s1 == r.to_string()) {
@ -5015,6 +5158,10 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
result = m().mk_or(fmls);
return true;
}
if (str().is_itos(r, s)) {
result = m_autil.mk_lt(s, m_autil.mk_int(0));
return true;
}
return false;
}

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

@ -180,6 +180,16 @@ class seq_rewriter {
expr_ref mk_seq_concat(expr* a, expr* b);
// Construct the expressions for taking the first element, the last element, the rest, and the butlast element
expr_ref mk_seq_first(expr* s);
expr_ref mk_seq_rest(expr* s);
expr_ref mk_seq_last(expr* s);
expr_ref mk_seq_butlast(expr* s);
bool try_get_unit_values(expr* s, expr_ref_vector& result);
//replace b in a by c into result
void replace_all_subvectors(expr_ref_vector const& as, expr_ref_vector const& bs, expr* c, expr_ref_vector& result);
// Calculate derivative, memoized and enforcing a normal form
expr_ref is_nullable_rec(expr* r);
expr_ref mk_derivative_rec(expr* ele, expr* r);
@ -344,6 +354,16 @@ public:
return result;
}
/*
* makes concat and simplifies
*/
expr_ref mk_re_append(expr* r1, expr* r2) {
expr_ref result(m());
if (mk_re_concat(r1, r2, result) == BR_FAILED)
result = re().mk_concat(r1, r2);
return result;
}
/**
* check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences
*/

19
src/ast/seq_decl_plugin.cpp
View file

@ -911,7 +911,7 @@ unsigned seq_util::str::max_length(expr* s) const {
return UINT_MAX;
};
while (is_concat(s, s1, s2)) {
result = u.max_plus(get_length(s), result);
result = u.max_plus(get_length(s1), result);
s = s2;
}
result = u.max_plus(get_length(s), result);
@ -1058,6 +1058,7 @@ app* seq_util::rex::mk_epsilon(sort* seq_sort) {
*/
std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) const {
SASSERT(re.u.is_seq(s));
zstring z;
if (re.u.str.is_empty(s))
out << "()";
else if (re.u.str.is_unit(s))
@ -1068,6 +1069,10 @@ std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s)
for (expr* e : es)
compact_helper_seq(out, e);
}
else if (re.u.str.is_string(s, z)) {
for (unsigned i = 0; i < z.length(); i++)
out << (char)z[i];
}
//using braces to indicate 'full' output
//for example an uninterpreted constant X will be printed as {X}
//while a unit sequence "X" will be printed as X
@ -1100,7 +1105,7 @@ bool seq_util::rex::pp::can_skip_parenth(expr* r) const {
std::ostream& seq_util::rex::pp::seq_unit(std::ostream& out, expr* s) const {
expr* e;
unsigned n = 0;
if (re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) {
if ((re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) || re.u.is_const_char(s, n)) {
char c = (char)n;
if (c == '\n')
out << "\\n";
@ -1148,7 +1153,11 @@ std::ostream& seq_util::rex::pp::seq_unit(std::ostream& out, expr* s) const {
std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
expr* r1 = nullptr, * r2 = nullptr, * s = nullptr, * s2 = nullptr;
unsigned lo = 0, hi = 0;
if (re.is_full_char(e))
if (re.u.is_char(e))
return seq_unit(out, e);
else if (re.u.is_seq(e))
return compact_helper_seq(out, e);
else if (re.is_full_char(e))
return out << ".";
else if (re.is_full_seq(e))
return out << ".*";
@ -1163,9 +1172,9 @@ std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
else if (re.is_concat(e, r1, r2))
return out << pp(re, r1) << pp(re, r2);
else if (re.is_union(e, r1, r2))
return out << pp(re, r1) << "|" << pp(re, r2);
return out << "(" << pp(re, r1) << "|" << pp(re, r2) << ")";
else if (re.is_intersection(e, r1, r2))
return out << "(" << pp(re, r1) << (html_encode ? ")&amp;(": ")&(" ) << pp(re, r2) << ")";
return out << "(" << pp(re, r1) << "&amp;" /*(html_encode ? ")&amp;(" : ")&(")*/ << pp(re, r2) << ")";
else if (re.is_complement(e, r1)) {
if (can_skip_parenth(r1))
return out << "~" << pp(re, r1);

12
src/sat/sat_simplifier.cpp
View file

@ -2022,10 +2022,14 @@ namespace sat {
}
remove_bin_clauses(pos_l);
remove_bin_clauses(neg_l);
remove_clauses(pos_occs, pos_l);
remove_clauses(neg_occs, neg_l);
pos_occs.reset();
neg_occs.reset();
{
clause_use_list& pos_occs = m_use_list.get(pos_l);
clause_use_list& neg_occs = m_use_list.get(neg_l);
remove_clauses(pos_occs, pos_l);
remove_clauses(neg_occs, neg_l);
pos_occs.reset();
neg_occs.reset();
}
return true;
}

1
src/sat/smt/arith_axioms.cpp
View file

@ -418,6 +418,7 @@ namespace arith {
expr* p = nullptr, * q = nullptr;
VERIFY(a.is_idiv(n, p, q));
theory_var v1 = internalize_def(p);
ensure_column(v1);
lp::impq r1 = get_ivalue(v1);
rational r2;

4
src/sat/smt/array_model.cpp
View file

@ -73,7 +73,7 @@ namespace array {
obj_map<expr, unsigned> num_occ;
for (euf::enode* p : euf::enode_parents(n->get_root())) {
if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n->get_root()) {
expr* v = values.get(p->get_root_id());
expr* v = values.get(p->get_root_id(), nullptr);
if (!v)
continue;
unsigned no = 0;
@ -92,7 +92,7 @@ namespace array {
for (euf::enode* p : euf::enode_parents(n)) {
if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n) {
expr* value = values.get(p->get_root_id());
expr* value = values.get(p->get_root_id(), nullptr);
if (!value || value == fi->get_else())
continue;
args.reset();

4
src/sat/smt/q_ematch.cpp
View file

@ -490,6 +490,10 @@ namespace q {
TRACE("q", tout << "add " << mk_pp(_q, m) << "\n";);
clause* c = clausify(_q);
quantifier* q = c->q();
if (m_q2clauses.contains(q)) {
dealloc(c);
return;
}
ensure_ground_enodes(*c);
m_clauses.push_back(c);
m_q2clauses.insert(q, c->index());

15
src/sat/smt/q_mam.cpp
View file

@ -414,7 +414,7 @@ namespace q {
enode_vector m_candidates;
#ifdef Z3DEBUG
egraph * m_egraph;
ptr_vector<app> m_patterns;
svector<std::pair<quantifier*, app*>> m_patterns;
#endif
#ifdef _PROFILE_MAM
stopwatch m_watch;
@ -568,7 +568,7 @@ namespace q {
m_egraph = ctx;
}
ptr_vector<app> & get_patterns() {
svector<std::pair<quantifier*, app*>> & get_patterns() {
return m_patterns;
}
#endif
@ -578,8 +578,8 @@ namespace q {
if (m_egraph) {
ast_manager & m = m_egraph->get_manager();
out << "patterns:\n";
for (app* a : m_patterns)
out << mk_pp(a, m) << "\n";
for (auto [q, a] : m_patterns)
out << mk_pp(q, m) << " " << mk_pp(a, m) << "\n";
}
#endif
out << "function: " << m_root_lbl->get_name();
@ -2862,12 +2862,11 @@ namespace q {
// The E-matching engine that was built when all + and * applications were binary.
// We ignore the pattern if it does not have the expected number of arguments.
// This is not the ideal solution, but it avoids possible crashes.
if (tree->expected_num_args() == p->get_num_args()) {
if (tree->expected_num_args() == p->get_num_args())
m_compiler.insert(tree, qa, mp, first_idx, false);
}
}
DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(mp);
ctx.push(push_back_trail<app*, false>(m_trees[lbl_id]->get_patterns())););
DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
ctx.push(push_back_trail<std::pair<quantifier*,app*>, false>(m_trees[lbl_id]->get_patterns())););
TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
}

12
src/tactic/core/pb_preprocess_tactic.cpp
View file

@ -44,6 +44,7 @@ class pb_preprocess_tactic : public tactic {
struct rec { unsigned_vector pos, neg; rec() { } };
typedef obj_map<app, rec> var_map;
ast_manager& m;
expr_ref_vector m_trail;
pb_util pb;
var_map m_vars;
unsigned_vector m_ge;
@ -99,7 +100,7 @@ class pb_preprocess_tactic : public tactic {
public:
pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()):
m(m), pb(m), m_r(m) {}
m(m), m_trail(m), pb(m), m_r(m) {}
~pb_preprocess_tactic() override {}
@ -157,7 +158,7 @@ public:
m_progress = false;
// first eliminate variables
var_map::iterator it = next_resolvent(m_vars.begin());
while (it != m_vars.end()) {
while (it != m_vars.end()) {
app * e = it->m_key;
rec const& r = it->m_value;
TRACE("pb", tout << mk_pp(e, m) << " " << r.pos.size() << " " << r.neg.size() << "\n";);
@ -235,6 +236,7 @@ private:
m_ge.reset();
m_other.reset();
m_vars.reset();
m_trail.reset();
}
expr* negate(expr* e) {
@ -410,6 +412,7 @@ private:
void insert(unsigned i, app* e, bool pos) {
SASSERT(is_uninterp_const(e));
if (!m_vars.contains(e)) {
m_trail.push_back(e);
m_vars.insert(e, rec());
}
if (pos) {
@ -504,10 +507,7 @@ private:
bool found = false;
for (unsigned j = 0; j < args2.size(); ++j) {
if (is_complement(args1.get(i), args2.get(j))) {
if (i == 0) {
min_coeff = coeffs2[j];
}
else if (min_coeff > coeffs2[j]) {
if (i == 0 || min_coeff > coeffs2[j]) {
min_coeff = coeffs2[j];
min_index = j;
}

85
src/tactic/core/reduce_invertible_tactic.cpp
View file

@ -93,10 +93,11 @@ public:
g->update(idx, f_new, new_pr, g->dep(idx));
}
if (mc) g->add(mc.get());
g->inc_depth();
TRACE("invertible_tactic", g->display(tout););
g->inc_depth();
}
result.push_back(g.get());
CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout););
CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout););
}
void cleanup() override {}
@ -223,28 +224,46 @@ private:
rational r;
app* a = to_app(v);
expr* fst_arg = a->get_arg(0);
bool fst_is_var = is_var(fst_arg);
for (unsigned i = 0, n = a->get_num_args(); i != n; ++i) {
auto arg = a->get_arg(i);
if (!m_parents[arg->get_id()].get() || is_var(arg) != fst_is_var)
for (expr* arg : *a)
if (!m_parents[arg->get_id()].get())
return false;
if (fst_is_var && to_var(arg)->get_idx() >= max_var)
return false;
if (m_bv.is_numeral(arg, r) && r != mdl)
return false;
if (i > 0 && !is_var(arg) && (!is_app(arg) || to_app(arg)->get_num_args() > 0))
if (is_var(fst_arg)) {
for (expr* arg : *a) {
if (!is_var(arg))
return false;
if (to_var(arg)->get_idx() >= max_var)
return false;
}
}
else {
bool first = true;
for (expr* arg : *a) {
if (!is_app(arg))
return false;
if (is_uninterp_const(arg))
continue;
if (m_bv.is_numeral(arg, r) && r == mdl) {
if (first || mdl.is_zero()) {
first = false;
continue;
}
else
return false;
}
return false;
}
}
if (mc) {
ensure_mc(mc);
expr_ref num(m_bv.mk_numeral(mdl, fst_arg->get_sort()), m);
for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) {
(*mc)->add(a->get_arg(i), num);
expr* arg = a->get_arg(i);
if (m_bv.is_numeral(arg))
continue;
(*mc)->add(arg, num);
}
}
new_v = fst_arg;
@ -327,7 +346,6 @@ private:
//
unsigned sz = m_bv.get_bv_size(p);
expr_ref bit1(m_bv.mk_numeral(1, 1), m);
new_v = m_bv.mk_numeral(0, sz);
unsigned sh = 0;
@ -335,9 +353,10 @@ private:
r /= rational(2);
++sh;
}
if (r.is_pos() && sh > 0) {
if (r.is_pos() && sh > 0)
new_v = m_bv.mk_concat(m_bv.mk_extract(sz-sh-1, 0, v), m_bv.mk_numeral(0, sh));
}
else
new_v = v;
if (mc && !r.is_zero()) {
ensure_mc(mc);
expr_ref def(m);
@ -414,6 +433,38 @@ private:
return true;
}
}
//
// v <= u
// => u + 1 == 0 or delta
// v := delta ? u : u + 1
//
if (m_bv.is_bv_ule(p, e1, e2) && e1 == v && mc) {
ensure_mc(mc);
unsigned sz = m_bv.get_bv_size(e2);
expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m);
expr_ref succ_e2(m_bv.mk_bv_add(e2, m_bv.mk_numeral(1, sz)), m);
new_v = m.mk_or(delta, m.mk_eq(succ_e2, m_bv.mk_numeral(0, sz)));
(*mc)->hide(delta);
(*mc)->add(v, m.mk_ite(delta, e2, succ_e2));
return true;
}
//
// u <= v
// => u == 0 or delta
// v := delta ? u : u - 1
//
if (m_bv.is_bv_ule(p, e1, e2) && e2 == v && mc) {
ensure_mc(mc);
unsigned sz = m_bv.get_bv_size(e1);
expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m);
expr_ref pred_e1(m_bv.mk_bv_sub(e1, m_bv.mk_numeral(1, sz)), m);
new_v = m.mk_or(delta, m.mk_eq(e1, m_bv.mk_numeral(0, sz)));
(*mc)->hide(delta);
(*mc)->add(v, m.mk_ite(delta, e1, pred_e1));
return true;
}
return false;
}

48
src/tactic/portfolio/solver_subsumption_tactic.cpp
View file

@ -41,31 +41,41 @@ class solver_subsumption_tactic : public tactic {
/**
* Check subsumption (a \/ b \/ c)
* if (a \/ b) is already implied
* Use a naive algorithm (not binary disection here)
*
* If
* F |= (a \/ ~b \/ c)
* Then replace (a \/ b \/ c) by (a \/ c)
*
* If
* F |= (a \/ b \/ c)
* Then replace (a \/ b \/ c) by true
*
*/
bool simplify(expr_ref& f) {
expr_ref_vector fmls(m), ors(m), nors(m), prefix(m);
expr_ref nf(m.mk_not(f), m);
fmls.push_back(nf);
lbool is_sat = m_solver->check_sat(fmls);
if (is_sat == l_false) {
f = m.mk_true();
return true;
}
if (!m.is_or(f))
return false;
expr_ref_vector ors(m);
ors.append(to_app(f)->get_num_args(), to_app(f)->get_args());
expr_ref_vector prefix(m);
for (expr* arg : ors)
nors.push_back(mk_not(m, arg));
for (unsigned i = 0; i < ors.size(); ++i) {
expr_ref_vector fmls(m);
fmls.append(prefix);
for (unsigned k = i + 1; k < ors.size(); ++k)
fmls.push_back(m.mk_not(ors.get(k)));
lbool is_sat = m_solver->check_sat(fmls);
if (is_sat == l_false)
continue;
fmls.reset();
fmls.push_back(ors.get(i));
is_sat = m_solver->check_sat(fmls);
if (is_sat == l_false)
continue;
prefix.push_back(ors.get(i));
expr* arg = ors.get(i);
expr_ref save(nors.get(i), m);
nors[i] = arg;
is_sat = m_solver->check_sat(nors);
nors[i] = save;
if (is_sat == l_false)
nors[i] = m.mk_true();
else
prefix.push_back(arg);
}
if (ors.size() != prefix.size()) {
ors.reset();
@ -131,7 +141,7 @@ public:
}
void collect_param_descrs(param_descrs& r) override {
r.insert("max_conflicts", CPK_UINT, "(default: 10) maximal number of conflicts allowed per solver call.");
r.insert("max_conflicts", CPK_UINT, "(default: 2) maximal number of conflicts allowed per solver call.");
}
void operator()(goal_ref const& g, goal_ref_buffer& result) override {

2
src/util/state_graph.cpp
View file

@ -13,7 +13,7 @@ Abstract:
Author:
Caleb Stanford (calebstanford-msr / cdstanford) 2020-7
Margus Veanes 2020-8
--*/
#include "state_graph.h"