mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
Merge pull request #2 from wintersteiger/lackr
Imported latest master branch.
This commit is contained in:
MikolasJanota
commit
7f7185ce02
src
api
ast
muz/base
smt
solver
tactic/ufbv
util
|
|
@ -130,4 +130,8 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0.0);
|
||||
}
|
||||
|
||||
__uint64 Z3_API Z3_get_estimated_alloc_size(void) {
|
||||
return memory::get_allocation_size();
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -4419,6 +4419,9 @@ extern "C" {
|
|||
\brief Interface to simplifier.
|
||||
|
||||
Provides an interface to the AST simplifier used by Z3.
|
||||
It returns an AST object which is equal to the argument.
|
||||
The returned AST is simplified using algebraic simplificaiton rules,
|
||||
such as constant propagation (propagating true/false over logical connectives).
|
||||
|
||||
def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
|
|
@ -5964,6 +5967,13 @@ extern "C" {
|
|||
*/
|
||||
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx);
|
||||
|
||||
/**
|
||||
\brief Return the estimated allocated memory in bytes.
|
||||
|
||||
def_API('Z3_get_estimated_alloc_size', UINT64, ())
|
||||
*/
|
||||
__uint64 Z3_API Z3_get_estimated_alloc_size(void);
|
||||
|
||||
/*@}*/
|
||||
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
|
|
@ -743,7 +743,14 @@ void bit_blaster_tpl<Cfg>::mk_srem(unsigned sz, expr * const * a_bits, expr * co
|
|||
mk_abs(sz, a_bits, abs_a_bits);
|
||||
mk_abs(sz, b_bits, abs_b_bits);
|
||||
expr_ref_vector urem_bits(m());
|
||||
mk_urem(sz, abs_a_bits.c_ptr(), abs_b_bits.c_ptr(), urem_bits);
|
||||
numeral n_b;
|
||||
unsigned shift;
|
||||
// a urem 2^n -> a & ((2^n)-1)
|
||||
if (is_numeral(sz, abs_b_bits.c_ptr(), n_b) && n_b.is_power_of_two(shift)) {
|
||||
mk_zero_extend(shift, abs_a_bits.c_ptr(), sz - shift, urem_bits);
|
||||
} else {
|
||||
mk_urem(sz, abs_a_bits.c_ptr(), abs_b_bits.c_ptr(), urem_bits);
|
||||
}
|
||||
expr_ref_vector neg_urem_bits(m());
|
||||
mk_neg(sz, urem_bits.c_ptr(), neg_urem_bits);
|
||||
mk_multiplexer(a_msb, sz, neg_urem_bits.c_ptr(), urem_bits.c_ptr(), out_bits);
|
||||
|
|
|
|||
|
|
@ -36,6 +36,7 @@ expr_ref sym_expr::accept(expr* e) {
|
|||
break;
|
||||
}
|
||||
case t_char:
|
||||
SASSERT(m.get_sort(e) == m.get_sort(m_t));
|
||||
result = m.mk_eq(e, m_t);
|
||||
break;
|
||||
case t_range: {
|
||||
|
|
@ -792,8 +793,8 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
|
|||
else if (m_util.str.is_empty(e)) {
|
||||
continue;
|
||||
}
|
||||
else if (m_util.str.is_unit(e)) {
|
||||
seq.push_back(e);
|
||||
else if (m_util.str.is_unit(e, e1)) {
|
||||
seq.push_back(e1);
|
||||
}
|
||||
else if (m_util.str.is_concat(e, e1, e2)) {
|
||||
todo.push_back(e1);
|
||||
|
|
@ -1420,6 +1421,7 @@ expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
|
|||
|
||||
bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs) {
|
||||
zstring s;
|
||||
expr* emp = 0;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (m_util.str.is_unit(es[i])) {
|
||||
if (all) return false;
|
||||
|
|
@ -1434,7 +1436,8 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_ve
|
|||
}
|
||||
}
|
||||
else {
|
||||
lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i])));
|
||||
emp = emp?emp:m_util.str.mk_empty(m().get_sort(es[i]));
|
||||
lhs.push_back(emp);
|
||||
rhs.push_back(es[i]);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -31,6 +31,10 @@ static bool is_hex_digit(char ch, unsigned& d) {
|
|||
d = 10 + ch - 'A';
|
||||
return true;
|
||||
}
|
||||
if ('a' <= ch && ch <= 'f') {
|
||||
d = 10 + ch - 'a';
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
@ -85,6 +89,7 @@ static bool is_escape_char(char const *& s, unsigned& result) {
|
|||
s += 2;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
zstring::zstring(encoding enc): m_encoding(enc) {}
|
||||
|
|
|
|||
|
|
@ -1069,14 +1069,7 @@ namespace datalog {
|
|||
func_decl_set::iterator it = rels.begin(), end = rels.end();
|
||||
for (; it != end; ++it) {
|
||||
func_decl* f = *it;
|
||||
out << "(declare-rel " << f->get_name() << " (";
|
||||
for (unsigned i = 0; i < f->get_arity(); ++i) {
|
||||
ast_smt2_pp(out, f->get_domain(i), env);
|
||||
if (i + 1 < f->get_arity()) {
|
||||
out << " ";
|
||||
}
|
||||
}
|
||||
out << "))\n";
|
||||
display_rel_decl(out, f);
|
||||
}
|
||||
|
||||
if (use_fixedpoint_extensions && do_declare_vars) {
|
||||
|
|
@ -1120,9 +1113,29 @@ namespace datalog {
|
|||
}
|
||||
if (use_fixedpoint_extensions) {
|
||||
for (unsigned i = 0; i < queries.size(); ++i) {
|
||||
out << "(query ";
|
||||
PP(queries[i].get());
|
||||
out << ")\n";
|
||||
expr* q = queries[i].get();
|
||||
func_decl_ref fn(m);
|
||||
if (is_query(q)) {
|
||||
fn = to_app(q)->get_decl();
|
||||
}
|
||||
else {
|
||||
m_free_vars(q);
|
||||
m_free_vars.set_default_sort(m.mk_bool_sort());
|
||||
sort* const* domain = m_free_vars.c_ptr();
|
||||
expr_ref qfn(m);
|
||||
expr_ref_vector args(m);
|
||||
fn = m.mk_fresh_func_decl(symbol("q"), symbol(""), m_free_vars.size(), domain, m.mk_bool_sort());
|
||||
display_rel_decl(out, fn);
|
||||
for (unsigned j = 0; j < m_free_vars.size(); ++j) {
|
||||
args.push_back(m.mk_var(j, m_free_vars[j]));
|
||||
}
|
||||
qfn = m.mk_implies(q, m.mk_app(fn, args.size(), args.c_ptr()));
|
||||
|
||||
out << "(assert ";
|
||||
PP(qfn);
|
||||
out << ")\n";
|
||||
}
|
||||
out << "(query " << fn->get_name() << ")\n";
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
|
@ -1139,6 +1152,35 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
void context::display_rel_decl(std::ostream& out, func_decl* f) {
|
||||
smt2_pp_environment_dbg env(m);
|
||||
out << "(declare-rel " << f->get_name() << " (";
|
||||
for (unsigned i = 0; i < f->get_arity(); ++i) {
|
||||
ast_smt2_pp(out, f->get_domain(i), env);
|
||||
if (i + 1 < f->get_arity()) {
|
||||
out << " ";
|
||||
}
|
||||
}
|
||||
out << "))\n";
|
||||
}
|
||||
|
||||
bool context::is_query(expr* q) {
|
||||
if (!is_app(q) || !is_predicate(to_app(q)->get_decl())) {
|
||||
return false;
|
||||
}
|
||||
app* a = to_app(q);
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
if (!is_var(a->get_arg(i))) {
|
||||
return false;
|
||||
}
|
||||
var* v = to_var(a->get_arg(i));
|
||||
if (v->get_idx() != i) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
void context::declare_vars(expr_ref_vector& rules, mk_fresh_name& fresh_names, std::ostream& out) {
|
||||
//
|
||||
|
|
|
|||
|
|
@ -581,6 +581,9 @@ namespace datalog {
|
|||
//undefined and private copy constructor and operator=
|
||||
context(const context&);
|
||||
context& operator=(const context&);
|
||||
|
||||
bool is_query(expr* e);
|
||||
void display_rel_decl(std::ostream& out, func_decl* f);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -847,6 +847,9 @@ namespace smt {
|
|||
setup_AUFLIA(false);
|
||||
setup_datatypes();
|
||||
setup_bv();
|
||||
setup_dl();
|
||||
setup_seq();
|
||||
setup_card();
|
||||
setup_fpa();
|
||||
return;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -64,6 +64,34 @@ bool theory_seq::solution_map::is_root(expr* e) const {
|
|||
return !m_map.contains(e);
|
||||
}
|
||||
|
||||
// e1 -> ... -> e2
|
||||
// e2 -> e3
|
||||
// e1 -> .... -> e3
|
||||
|
||||
// e1 -> ... x, e2 -> ... x
|
||||
void theory_seq::solution_map::find_rec(expr* e, svector<std::pair<expr*, dependency*> >& finds) {
|
||||
dependency* d = 0;
|
||||
std::pair<expr*, dependency*> value(e, d);
|
||||
do {
|
||||
e = value.first;
|
||||
d = m_dm.mk_join(d, value.second);
|
||||
finds.push_back(value);
|
||||
}
|
||||
while (m_map.find(e, value));
|
||||
}
|
||||
|
||||
bool theory_seq::solution_map::find1(expr* e, expr*& r, dependency*& d) {
|
||||
std::pair<expr*, dependency*> value;
|
||||
if (m_map.find(e, value)) {
|
||||
d = m_dm.mk_join(d, value.second);
|
||||
r = value.first;
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
expr* theory_seq::solution_map::find(expr* e, dependency*& d) {
|
||||
std::pair<expr*, dependency*> value;
|
||||
d = 0;
|
||||
|
|
@ -183,9 +211,9 @@ theory_seq::theory_seq(ast_manager& m):
|
|||
m_indexof_left = "seq.indexof.left";
|
||||
m_indexof_right = "seq.indexof.right";
|
||||
m_aut_step = "aut.step";
|
||||
m_extract_prefix = "seq.extract.prefix";
|
||||
m_at_left = "seq.at.left";
|
||||
m_at_right = "seq.at.right";
|
||||
m_pre = "seq.pre"; // (seq.pre s l): prefix of string s of length l
|
||||
m_post = "seq.post"; // (seq.post s l): suffix of string s of length l
|
||||
m_eq = "seq.eq";
|
||||
}
|
||||
|
||||
theory_seq::~theory_seq() {
|
||||
|
|
@ -215,21 +243,21 @@ final_check_status theory_seq::final_check_eh() {
|
|||
TRACE("seq", tout << ">>check_length_coherence\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (propagate_automata()) {
|
||||
++m_stats.m_propagate_automata;
|
||||
TRACE("seq", tout << ">>propagate_automata\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (!check_extensionality()) {
|
||||
++m_stats.m_extensionality;
|
||||
TRACE("seq", tout << ">>extensionality\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (propagate_automata()) {
|
||||
++m_stats.m_propagate_automata;
|
||||
TRACE("seq", tout << ">>propagate_automata\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (is_solved()) {
|
||||
TRACE("seq", tout << ">>is_solved\n";);
|
||||
return FC_DONE;
|
||||
}
|
||||
|
||||
TRACE("seq", tout << ">>give_up\n";);
|
||||
return FC_GIVEUP;
|
||||
}
|
||||
|
||||
|
|
@ -451,7 +479,7 @@ bool theory_seq::check_length_coherence(expr* e) {
|
|||
propagate_is_conc(e, conc);
|
||||
assume_equality(tail, emp);
|
||||
}
|
||||
if (!get_context().at_base_level()) {
|
||||
else if (!get_context().at_base_level()) {
|
||||
m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
|
||||
}
|
||||
return true;
|
||||
|
|
@ -501,11 +529,17 @@ bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const {
|
|||
}
|
||||
|
||||
bool theory_seq::is_eq(expr* e, expr*& a, expr*& b) const {
|
||||
return is_skolem(symbol("seq.eq"), e) &&
|
||||
return is_skolem(m_eq, e) &&
|
||||
(a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true);
|
||||
}
|
||||
|
||||
|
||||
bool theory_seq::is_pre(expr* e, expr*& s, expr*& i) {
|
||||
return is_skolem(m_pre, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true);
|
||||
}
|
||||
|
||||
|
||||
|
||||
expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
|
||||
sort* char_sort = 0;
|
||||
VERIFY(m_util.is_seq(m.get_sort(s), char_sort));
|
||||
|
|
@ -573,29 +607,41 @@ bool theory_seq::check_extensionality() {
|
|||
unsigned sz = get_num_vars();
|
||||
unsigned_vector seqs;
|
||||
for (unsigned v = 0; v < sz; ++v) {
|
||||
enode* n = get_enode(v);
|
||||
expr* o1 = n->get_owner();
|
||||
if (n != n->get_root()) {
|
||||
enode* n1 = get_enode(v);
|
||||
expr* o1 = n1->get_owner();
|
||||
if (n1 != n1->get_root()) {
|
||||
continue;
|
||||
}
|
||||
if (!seqs.empty() && ctx.is_relevant(n) && m_util.is_seq(o1) && ctx.is_shared(n)) {
|
||||
if (!seqs.empty() && ctx.is_relevant(n1) && m_util.is_seq(o1) && ctx.is_shared(n1)) {
|
||||
dependency* dep = 0;
|
||||
expr_ref e1 = canonize(o1, dep);
|
||||
for (unsigned i = 0; i < seqs.size(); ++i) {
|
||||
enode* n2 = get_enode(seqs[i]);
|
||||
expr* o2 = n2->get_owner();
|
||||
if (m_exclude.contains(o1, o2)) {
|
||||
if (m.get_sort(o1) != m.get_sort(o2)) {
|
||||
continue;
|
||||
}
|
||||
if (ctx.is_diseq(n1, n2) || m_exclude.contains(o1, o2)) {
|
||||
continue;
|
||||
}
|
||||
expr_ref e2 = canonize(n2->get_owner(), dep);
|
||||
m_lhs.reset(); m_rhs.reset();
|
||||
bool change = false;
|
||||
if (!m_seq_rewrite.reduce_eq(o1, o2, m_lhs, m_rhs, change)) {
|
||||
if (!m_seq_rewrite.reduce_eq(e1, e2, m_lhs, m_rhs, change)) {
|
||||
m_exclude.update(o1, o2);
|
||||
continue;
|
||||
}
|
||||
TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";);
|
||||
ctx.assume_eq(n, n2);
|
||||
bool excluded = false;
|
||||
for (unsigned j = 0; !excluded && j < m_lhs.size(); ++j) {
|
||||
if (m_exclude.contains(m_lhs[j].get(), m_rhs[j].get())) {
|
||||
excluded = true;
|
||||
}
|
||||
}
|
||||
if (excluded) {
|
||||
continue;
|
||||
}
|
||||
TRACE("seq", tout << m_lhs << " = " << m_rhs << "\n";);
|
||||
ctx.assume_eq(n1, n2);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
|
@ -670,7 +716,7 @@ void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) {
|
|||
enode_pair_vector eqs;
|
||||
literal_vector lits(_lits);
|
||||
linearize(dep, eqs, lits);
|
||||
TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); if (!lits.empty()) tout << "\n"; display_deps(tout, dep); ;);
|
||||
TRACE("seq", display_deps(tout, lits, eqs););
|
||||
m_new_propagation = true;
|
||||
ctx.set_conflict(
|
||||
ctx.mk_justification(
|
||||
|
|
@ -720,6 +766,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
|
|||
context& ctx = get_context();
|
||||
expr_ref_vector lhs(m), rhs(m);
|
||||
bool changed = false;
|
||||
TRACE("seq", tout << ls << " = " << rs << "\n";);
|
||||
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, changed)) {
|
||||
// equality is inconsistent.
|
||||
TRACE("seq", tout << ls << " != " << rs << "\n";);
|
||||
|
|
@ -739,9 +786,10 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
|
|||
expr_ref li(lhs[i].get(), m);
|
||||
expr_ref ri(rhs[i].get(), m);
|
||||
if (solve_unit_eq(li, ri, deps)) {
|
||||
// skip
|
||||
// no-op
|
||||
}
|
||||
else if (m_util.is_seq(li) || m_util.is_re(li)) {
|
||||
reduce_length(li, ri);
|
||||
m_eqs.push_back(mk_eqdep(li, ri, deps));
|
||||
}
|
||||
else {
|
||||
|
|
@ -769,6 +817,23 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const&
|
|||
return false;
|
||||
}
|
||||
|
||||
bool theory_seq::reduce_length(expr* l, expr* r) {
|
||||
expr* l2, *r2;
|
||||
expr_ref len1(m), len2(m);
|
||||
literal_vector lits;
|
||||
m_util.str.is_concat(l, l, l2);
|
||||
m_util.str.is_concat(r, r, r2);
|
||||
if (get_length(l, len1, lits) &&
|
||||
get_length(r, len2, lits) && len1 == len2) {
|
||||
TRACE("seq", tout << "Propagate equal lengths\n";);
|
||||
//propagate_eq(lits, l, r, true);
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
|
||||
if (l == r) {
|
||||
return true;
|
||||
|
|
@ -996,6 +1061,58 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
|
|||
return false;
|
||||
}
|
||||
|
||||
bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
|
||||
context& ctx = get_context();
|
||||
expr* s, *i, *l;
|
||||
if (m_util.str.is_extract(e, s, i, l)) {
|
||||
// 0 <= i <= len(s), 0 <= l, i + l <= len(s)
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
expr_ref ls(m_util.str.mk_length(s), m);
|
||||
expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
|
||||
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
|
||||
literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
|
||||
literal li_ge_ls = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
|
||||
literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
|
||||
if (ctx.get_assignment(i_ge_0) == l_true &&
|
||||
ctx.get_assignment(i_lt_len_s) == l_true &&
|
||||
ctx.get_assignment(li_ge_ls) == l_true &&
|
||||
ctx.get_assignment(l_ge_zero) == l_true) {
|
||||
len = l;
|
||||
lits.push_back(i_ge_0); lits.push_back(i_lt_len_s); lits.push_back(li_ge_ls); lits.push_back(l_ge_zero);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
else if (m_util.str.is_at(e, s, i)) {
|
||||
// has length 1 if 0 <= i < len(s)
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
|
||||
literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
|
||||
if (ctx.get_assignment(i_ge_0) == l_true &&
|
||||
ctx.get_assignment(i_lt_len_s) == l_true) {
|
||||
len = m_autil.mk_int(1);
|
||||
lits.push_back(i_ge_0); lits.push_back(i_lt_len_s);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
else if (is_pre(e, s, i)) {
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
|
||||
literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
|
||||
if (ctx.get_assignment(i_ge_0) == l_true &&
|
||||
ctx.get_assignment(i_lt_len_s) == l_true) {
|
||||
len = i;
|
||||
lits.push_back(i_ge_0); lits.push_back(i_lt_len_s);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
else if (m_util.str.is_unit(e)) {
|
||||
len = m_autil.mk_int(1);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
bool theory_seq::solve_nqs(unsigned i) {
|
||||
context & ctx = get_context();
|
||||
for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
|
||||
|
|
@ -1046,7 +1163,7 @@ bool theory_seq::solve_ne(unsigned idx) {
|
|||
change = canonize(n.rs(i), rs, deps) || change;
|
||||
|
||||
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, change)) {
|
||||
TRACE("seq", display_disequation(tout << "reduces to false", n););
|
||||
TRACE("seq", display_disequation(tout << "reduces to false: ", n););
|
||||
return true;
|
||||
}
|
||||
else if (!change) {
|
||||
|
|
@ -1144,16 +1261,181 @@ bool theory_seq::solve_ne(unsigned idx) {
|
|||
if (updated) {
|
||||
if (num_undef_lits == 0 && new_ls.empty()) {
|
||||
TRACE("seq", tout << "conflict\n";);
|
||||
|
||||
dependency* deps1 = 0;
|
||||
if (explain_eq(n.l(), n.r(), deps1)) {
|
||||
new_lits.reset();
|
||||
new_lits.push_back(~mk_eq(n.l(), n.r(), false));
|
||||
new_deps = deps1;
|
||||
TRACE("seq", tout << "conflict explained\n";);
|
||||
}
|
||||
set_conflict(new_deps, new_lits);
|
||||
SASSERT(m_new_propagation);
|
||||
}
|
||||
else {
|
||||
m_nqs.push_back(ne(new_ls, new_rs, new_lits, new_deps));
|
||||
m_nqs.push_back(ne(n.l(), n.r(), new_ls, new_rs, new_lits, new_deps));
|
||||
}
|
||||
}
|
||||
return updated;
|
||||
}
|
||||
|
||||
theory_seq::cell* theory_seq::mk_cell(cell* p, expr* e, dependency* d) {
|
||||
cell* c = alloc(cell, p, e, d);
|
||||
m_all_cells.push_back(c);
|
||||
return c;
|
||||
}
|
||||
|
||||
void theory_seq::unfold(cell* c, ptr_vector<cell>& cons) {
|
||||
dependency* dep = 0;
|
||||
expr* a, *e1, *e2;
|
||||
if (m_rep.find1(c->m_expr, a, dep)) {
|
||||
cell* c1 = mk_cell(c, a, m_dm.mk_join(dep, c->m_dep));
|
||||
unfold(c1, cons);
|
||||
}
|
||||
else if (m_util.str.is_concat(c->m_expr, e1, e2)) {
|
||||
cell* c1 = mk_cell(c, e1, c->m_dep);
|
||||
cell* c2 = mk_cell(0, e2, 0);
|
||||
unfold(c1, cons);
|
||||
unfold(c2, cons);
|
||||
}
|
||||
else {
|
||||
cons.push_back(c);
|
||||
}
|
||||
c->m_last = cons.size()-1;
|
||||
}
|
||||
//
|
||||
// a -> a1.a2, a2 -> a3.a4 -> ...
|
||||
// b -> b1.b2, b2 -> b3.a4
|
||||
//
|
||||
// e1
|
||||
//
|
||||
|
||||
void theory_seq::display_explain(std::ostream& out, unsigned indent, expr* e) {
|
||||
expr* e1, *e2, *a;
|
||||
dependency* dep = 0;
|
||||
smt2_pp_environment_dbg env(m);
|
||||
params_ref p;
|
||||
for (unsigned i = 0; i < indent; ++i) out << " ";
|
||||
ast_smt2_pp(out, e, env, p, indent);
|
||||
out << "\n";
|
||||
|
||||
if (m_rep.find1(e, a, dep)) {
|
||||
display_explain(out, indent + 1, a);
|
||||
}
|
||||
else if (m_util.str.is_concat(e, e1, e2)) {
|
||||
display_explain(out, indent + 1, e1);
|
||||
display_explain(out, indent + 1, e2);
|
||||
}
|
||||
}
|
||||
|
||||
bool theory_seq::explain_eq(expr* e1, expr* e2, dependency*& dep) {
|
||||
|
||||
if (e1 == e2) {
|
||||
return true;
|
||||
}
|
||||
expr* a1, *a2;
|
||||
ptr_vector<cell> v1, v2;
|
||||
unsigned cells_sz = m_all_cells.size();
|
||||
cell* c1 = mk_cell(0, e1, 0);
|
||||
cell* c2 = mk_cell(0, e2, 0);
|
||||
unfold(c1, v1);
|
||||
unfold(c2, v2);
|
||||
unsigned i = 0, j = 0;
|
||||
|
||||
TRACE("seq",
|
||||
tout << "1:\n";
|
||||
display_explain(tout, 0, e1);
|
||||
tout << "2:\n";
|
||||
display_explain(tout, 0, e2););
|
||||
|
||||
bool result = true;
|
||||
while (i < v1.size() || j < v2.size()) {
|
||||
if (i == v1.size()) {
|
||||
while (j < v2.size() && m_util.str.is_empty(v2[j]->m_expr)) {
|
||||
dep = m_dm.mk_join(dep, v2[j]->m_dep);
|
||||
++j;
|
||||
}
|
||||
result = j == v2.size();
|
||||
break;
|
||||
}
|
||||
if (j == v2.size()) {
|
||||
while (i < v1.size() && m_util.str.is_empty(v1[i]->m_expr)) {
|
||||
dep = m_dm.mk_join(dep, v1[i]->m_dep);
|
||||
++i;
|
||||
}
|
||||
result = i == v1.size();
|
||||
break;
|
||||
}
|
||||
cell* c1 = v1[i];
|
||||
cell* c2 = v2[j];
|
||||
e1 = c1->m_expr;
|
||||
e2 = c2->m_expr;
|
||||
if (e1 == e2) {
|
||||
if (c1->m_parent && c2->m_parent &&
|
||||
c1->m_parent->m_expr == c2->m_parent->m_expr) {
|
||||
TRACE("seq", tout << "parent: " << mk_pp(e1, m) << " " << mk_pp(c1->m_parent->m_expr, m) << "\n";);
|
||||
c1 = c1->m_parent;
|
||||
c2 = c2->m_parent;
|
||||
v1[c1->m_last] = c1;
|
||||
i = c1->m_last;
|
||||
v2[c2->m_last] = c2;
|
||||
j = c2->m_last;
|
||||
}
|
||||
else {
|
||||
dep = m_dm.mk_join(dep, c1->m_dep);
|
||||
dep = m_dm.mk_join(dep, c2->m_dep);
|
||||
++i;
|
||||
++j;
|
||||
}
|
||||
}
|
||||
else if (m_util.str.is_empty(e1)) {
|
||||
dep = m_dm.mk_join(dep, c1->m_dep);
|
||||
++i;
|
||||
}
|
||||
else if (m_util.str.is_empty(e2)) {
|
||||
dep = m_dm.mk_join(dep, c2->m_dep);
|
||||
++j;
|
||||
}
|
||||
else if (m_util.str.is_unit(e1, a1) &&
|
||||
m_util.str.is_unit(e2, a2)) {
|
||||
if (explain_eq(a1, a2, dep)) {
|
||||
++i;
|
||||
++j;
|
||||
}
|
||||
else {
|
||||
result = false;
|
||||
break;
|
||||
}
|
||||
}
|
||||
else {
|
||||
TRACE("seq", tout << "Could not solve " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
|
||||
result = false;
|
||||
break;
|
||||
}
|
||||
}
|
||||
m_all_cells.resize(cells_sz);
|
||||
return result;
|
||||
|
||||
}
|
||||
|
||||
bool theory_seq::explain_empty(expr_ref_vector& es, dependency*& dep) {
|
||||
while (!es.empty()) {
|
||||
expr* e = es.back();
|
||||
if (m_util.str.is_empty(e)) {
|
||||
es.pop_back();
|
||||
continue;
|
||||
}
|
||||
expr* a;
|
||||
if (m_rep.find1(e, a, dep)) {
|
||||
es.pop_back();
|
||||
m_util.str.get_concat(a, es);
|
||||
continue;
|
||||
}
|
||||
TRACE("seq", tout << "Could not set to empty: " << es << "\n";);
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool theory_seq::simplify_and_solve_eqs() {
|
||||
context & ctx = get_context();
|
||||
|
|
@ -1294,18 +1576,44 @@ void theory_seq::display_disequation(std::ostream& out, ne const& e) const {
|
|||
}
|
||||
}
|
||||
|
||||
void theory_seq::display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const {
|
||||
context& ctx = get_context();
|
||||
smt2_pp_environment_dbg env(m);
|
||||
params_ref p;
|
||||
for (unsigned i = 0; i < eqs.size(); ++i) {
|
||||
out << " (= ";
|
||||
ast_smt2_pp(out, eqs[i].first->get_owner(), env, p, 5);
|
||||
out << "\n ";
|
||||
ast_smt2_pp(out, eqs[i].second->get_owner(), env, p, 5);
|
||||
out << ")\n";
|
||||
}
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
literal l = lits[i];
|
||||
if (l == true_literal) {
|
||||
out << " true";
|
||||
}
|
||||
else if (l == false_literal) {
|
||||
out << " false";
|
||||
}
|
||||
else {
|
||||
expr* e = ctx.bool_var2expr(l.var());
|
||||
if (l.sign()) {
|
||||
ast_smt2_pp(out << " (not ", e, env, p, 7);
|
||||
out << ")";
|
||||
}
|
||||
else {
|
||||
ast_smt2_pp(out << " ", e, env, p, 2);
|
||||
}
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
void theory_seq::display_deps(std::ostream& out, dependency* dep) const {
|
||||
literal_vector lits;
|
||||
enode_pair_vector eqs;
|
||||
linearize(dep, eqs, lits);
|
||||
for (unsigned i = 0; i < eqs.size(); ++i) {
|
||||
out << " " << mk_pp(eqs[i].first->get_owner(), m) << " = " << mk_pp(eqs[i].second->get_owner(), m) << "\n";
|
||||
}
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
literal lit = lits[i];
|
||||
get_context().display_literals_verbose(out << " ", 1, &lit);
|
||||
out << "\n";
|
||||
}
|
||||
display_deps(out, lits, eqs);
|
||||
}
|
||||
|
||||
void theory_seq::collect_statistics(::statistics & st) const {
|
||||
|
|
@ -1534,6 +1842,9 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
|
|||
else if (m_util.str.is_contains(e, e1, e2)) {
|
||||
result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps));
|
||||
}
|
||||
else if (m_util.str.is_unit(e, e1)) {
|
||||
result = m_util.str.mk_unit(expand(e1, deps));
|
||||
}
|
||||
else {
|
||||
result = e;
|
||||
}
|
||||
|
|
@ -1954,12 +2265,30 @@ bool theory_seq::get_length(expr* e, rational& val) {
|
|||
void theory_seq::add_extract_axiom(expr* e) {
|
||||
expr* s, *i, *l;
|
||||
VERIFY(m_util.str.is_extract(e, s, i, l));
|
||||
expr_ref x(mk_skolem(m_extract_prefix, s, e), m);
|
||||
if (is_tail(s, i, l)) {
|
||||
add_tail_axiom(e, s);
|
||||
return;
|
||||
}
|
||||
if (is_drop_last(s, i, l)) {
|
||||
add_drop_last_axiom(e, s);
|
||||
return;
|
||||
}
|
||||
if (is_extract_prefix0(s, i, l)) {
|
||||
add_extract_prefix_axiom(e, s, l);
|
||||
return;
|
||||
}
|
||||
if (is_extract_suffix(s, i, l)) {
|
||||
add_extract_suffix_axiom(e, s, i);
|
||||
return;
|
||||
}
|
||||
expr_ref x(mk_skolem(m_pre, s, i), m);
|
||||
expr_ref ls(m_util.str.mk_length(s), m);
|
||||
expr_ref lx(m_util.str.mk_length(x), m);
|
||||
expr_ref le(m_util.str.mk_length(e), m);
|
||||
expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
|
||||
expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i), l), m);
|
||||
expr_ref y(mk_skolem(m_post, s, ls_minus_i_l), m);
|
||||
expr_ref xe = mk_concat(x, e);
|
||||
expr_ref xey = mk_concat(x, e, y);
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
|
||||
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
|
||||
|
|
@ -1967,13 +2296,91 @@ void theory_seq::add_extract_axiom(expr* e) {
|
|||
literal li_ge_ls = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
|
||||
literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
|
||||
|
||||
add_axiom(~i_ge_0, ~i_le_ls, mk_literal(m_util.str.mk_prefix(xe, s)));
|
||||
// add_axiom(~i_ge_0, ~i_le_ls, mk_literal(m_util.str.mk_prefix(xe, s)));
|
||||
add_axiom(~i_ge_0, ~i_le_ls, mk_seq_eq(xey, s));
|
||||
add_axiom(~i_ge_0, ~i_le_ls, mk_eq(lx, i, false));
|
||||
add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_zero, ~li_ge_ls, mk_eq(le, l, false));
|
||||
add_axiom(~i_ge_0, ~i_le_ls, li_ge_ls, mk_eq(le, mk_sub(ls, i), false));
|
||||
add_axiom(~i_ge_0, ~i_le_ls, l_ge_zero, mk_eq(le, zero, false));
|
||||
}
|
||||
|
||||
void theory_seq::add_tail_axiom(expr* e, expr* s) {
|
||||
expr_ref head(m), tail(m);
|
||||
mk_decompose(s, head, tail);
|
||||
add_axiom(mk_eq_empty(s), mk_seq_eq(s, mk_concat(head, e)));
|
||||
}
|
||||
|
||||
void theory_seq::add_drop_last_axiom(expr* e, expr* s) {
|
||||
add_axiom(mk_eq_empty(s), mk_seq_eq(s, mk_concat(e, m_util.str.mk_unit(mk_last(s)))));
|
||||
}
|
||||
|
||||
bool theory_seq::is_drop_last(expr* s, expr* i, expr* l) {
|
||||
rational i1;
|
||||
if (!m_autil.is_numeral(i, i1) || !i1.is_zero()) {
|
||||
return false;
|
||||
}
|
||||
expr_ref l2(m), l1(l, m);
|
||||
l2 = m_autil.mk_sub(m_util.str.mk_length(s), m_autil.mk_int(1));
|
||||
m_rewrite(l1);
|
||||
m_rewrite(l2);
|
||||
return l1 == l2;
|
||||
}
|
||||
|
||||
bool theory_seq::is_tail(expr* s, expr* i, expr* l) {
|
||||
rational i1;
|
||||
if (!m_autil.is_numeral(i, i1) || !i1.is_one()) {
|
||||
return false;
|
||||
}
|
||||
expr_ref l2(m), l1(l, m);
|
||||
l2 = m_autil.mk_sub(m_util.str.mk_length(s), m_autil.mk_int(1));
|
||||
m_rewrite(l1);
|
||||
m_rewrite(l2);
|
||||
return l1 == l2;
|
||||
}
|
||||
|
||||
bool theory_seq::is_extract_prefix0(expr* s, expr* i, expr* l) {
|
||||
rational i1;
|
||||
return m_autil.is_numeral(i, i1) && i1.is_zero();
|
||||
}
|
||||
|
||||
bool theory_seq::is_extract_suffix(expr* s, expr* i, expr* l) {
|
||||
expr_ref len(m_autil.mk_add(l, i), m);
|
||||
m_rewrite(len);
|
||||
return m_util.str.is_length(len, l) && l == s;
|
||||
}
|
||||
|
||||
/*
|
||||
0 <= l <= len(s) => s = ey & l = len(e)
|
||||
*/
|
||||
void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
|
||||
expr_ref le(m_util.str.mk_length(e), m);
|
||||
expr_ref ls(m_util.str.mk_length(s), m);
|
||||
expr_ref ls_minus_l(mk_sub(ls, l), m);
|
||||
expr_ref y(mk_skolem(m_post, s, ls_minus_l), m);
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
expr_ref ey = mk_concat(e, y);
|
||||
literal l_ge_0 = mk_literal(m_autil.mk_ge(l, zero));
|
||||
literal l_le_s = mk_literal(m_autil.mk_le(mk_sub(l, ls), zero));
|
||||
add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey));
|
||||
add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false));
|
||||
}
|
||||
|
||||
/*
|
||||
0 <= i <= len(s) => s = xe & i = len(x)
|
||||
*/
|
||||
void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
|
||||
expr_ref x(mk_skolem(m_pre, s, i), m);
|
||||
expr_ref lx(m_util.str.mk_length(x), m);
|
||||
expr_ref ls(m_util.str.mk_length(s), m);
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
expr_ref xe = mk_concat(x, e);
|
||||
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
|
||||
literal i_le_s = mk_literal(m_autil.mk_le(mk_sub(i, ls), zero));
|
||||
add_axiom(~i_ge_0, ~i_le_s, mk_seq_eq(s, xe));
|
||||
add_axiom(~i_ge_0, ~i_le_s, mk_eq(i, lx, false));
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
let e = at(s, i)
|
||||
|
||||
|
|
@ -1983,14 +2390,14 @@ void theory_seq::add_extract_axiom(expr* e) {
|
|||
void theory_seq::add_at_axiom(expr* e) {
|
||||
expr* s, *i;
|
||||
VERIFY(m_util.str.is_at(e, s, i));
|
||||
expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m);
|
||||
x = mk_skolem(m_at_left, s, i);
|
||||
y = mk_skolem(m_at_right, s, i);
|
||||
xey = mk_concat(x, e, y);
|
||||
zero = m_autil.mk_int(0);
|
||||
one = m_autil.mk_int(1);
|
||||
len_e = m_util.str.mk_length(e);
|
||||
len_x = m_util.str.mk_length(x);
|
||||
expr_ref len_e(m_util.str.mk_length(e), m);
|
||||
expr_ref len_s(m_util.str.mk_length(s), m);
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
expr_ref one(m_autil.mk_int(1), m);
|
||||
expr_ref x = mk_skolem(m_pre, s, i);
|
||||
expr_ref y = mk_skolem(m_post, s, mk_sub(mk_sub(len_s, i), one));
|
||||
expr_ref xey = mk_concat(x, e, y);
|
||||
expr_ref len_x(m_util.str.mk_length(x), m);
|
||||
|
||||
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
|
||||
literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
|
||||
|
|
@ -2057,7 +2464,7 @@ literal theory_seq::mk_literal(expr* _e) {
|
|||
|
||||
literal theory_seq::mk_seq_eq(expr* a, expr* b) {
|
||||
SASSERT(m_util.is_seq(a));
|
||||
return mk_literal(mk_skolem(symbol("seq.eq"), a, b, 0, m.mk_bool_sort()));
|
||||
return mk_literal(mk_skolem(m_eq, a, b, 0, m.mk_bool_sort()));
|
||||
}
|
||||
|
||||
literal theory_seq::mk_eq_empty(expr* _e) {
|
||||
|
|
@ -2116,8 +2523,13 @@ bool theory_seq::is_skolem(symbol const& s, expr* e) const {
|
|||
return m_util.is_skolem(e) && to_app(e)->get_decl()->get_parameter(0).get_symbol() == s;
|
||||
}
|
||||
|
||||
|
||||
void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs) {
|
||||
literal_vector lits;
|
||||
lits.push_back(lit);
|
||||
propagate_eq(lits, e1, e2, add_to_eqs);
|
||||
}
|
||||
|
||||
void theory_seq::propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs) {
|
||||
context& ctx = get_context();
|
||||
|
||||
enode* n1 = ensure_enode(e1);
|
||||
|
|
@ -2128,18 +2540,21 @@ void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs)
|
|||
ctx.mark_as_relevant(n1);
|
||||
ctx.mark_as_relevant(n2);
|
||||
if (add_to_eqs) {
|
||||
SASSERT(l_true == ctx.get_assignment(lit));
|
||||
dependency* deps = m_dm.mk_leaf(assumption(lit));
|
||||
dependency* deps = 0;
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
literal lit = lits[i];
|
||||
SASSERT(l_true == ctx.get_assignment(lit));
|
||||
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit)));
|
||||
}
|
||||
new_eq_eh(deps, n1, n2);
|
||||
|
||||
}
|
||||
TRACE("seq",
|
||||
ctx.display_literals_verbose(tout, 1, &lit);
|
||||
ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr());
|
||||
tout << " => " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
|
||||
justification* js =
|
||||
ctx.mk_justification(
|
||||
ext_theory_eq_propagation_justification(
|
||||
get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2));
|
||||
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, 0, n1, n2));
|
||||
|
||||
m_new_propagation = true;
|
||||
ctx.assign_eq(n1, n2, eq_justification(js));
|
||||
|
|
|
|||
|
|
@ -81,6 +81,8 @@ namespace smt {
|
|||
bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); }
|
||||
expr* find(expr* e, dependency*& d);
|
||||
expr* find(expr* e);
|
||||
bool find1(expr* a, expr*& b, dependency*& dep);
|
||||
void find_rec(expr* e, svector<std::pair<expr*, dependency*> >& finds);
|
||||
bool is_root(expr* e) const;
|
||||
void cache(expr* e, expr* r, dependency* d);
|
||||
void reset_cache() { m_cache.reset(); }
|
||||
|
|
@ -142,31 +144,35 @@ namespace smt {
|
|||
return eq(m_eq_id++, ls, rs, dep);
|
||||
}
|
||||
|
||||
class ne {
|
||||
vector<expr_ref_vector> m_lhs;
|
||||
vector<expr_ref_vector> m_rhs;
|
||||
class ne {
|
||||
expr_ref m_l, m_r;
|
||||
vector<expr_ref_vector> m_lhs, m_rhs;
|
||||
literal_vector m_lits;
|
||||
dependency* m_dep;
|
||||
public:
|
||||
ne(expr_ref const& l, expr_ref const& r, dependency* dep):
|
||||
m_dep(dep) {
|
||||
expr_ref_vector ls(l.get_manager()); ls.push_back(l);
|
||||
expr_ref_vector rs(r.get_manager()); rs.push_back(r);
|
||||
m_l(l), m_r(r), m_dep(dep) {
|
||||
expr_ref_vector ls(l.get_manager()); ls.push_back(l);
|
||||
expr_ref_vector rs(r.get_manager()); rs.push_back(r);
|
||||
m_lhs.push_back(ls);
|
||||
m_rhs.push_back(rs);
|
||||
}
|
||||
|
||||
ne(vector<expr_ref_vector> const& l, vector<expr_ref_vector> const& r, literal_vector const& lits, dependency* dep):
|
||||
ne(expr_ref const& _l, expr_ref const& _r, vector<expr_ref_vector> const& l, vector<expr_ref_vector> const& r, literal_vector const& lits, dependency* dep):
|
||||
m_l(_l), m_r(_r),
|
||||
m_lhs(l),
|
||||
m_rhs(r),
|
||||
m_lits(lits),
|
||||
m_dep(dep) {}
|
||||
|
||||
ne(ne const& other):
|
||||
m_l(other.m_l), m_r(other.m_r),
|
||||
m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
|
||||
|
||||
ne& operator=(ne const& other) {
|
||||
if (this != &other) {
|
||||
m_l = other.m_l;
|
||||
m_r = other.m_r;
|
||||
m_lhs.reset(); m_lhs.append(other.m_lhs);
|
||||
m_rhs.reset(); m_rhs.append(other.m_rhs);
|
||||
m_lits.reset(); m_lits.append(other.m_lits);
|
||||
|
|
@ -181,6 +187,8 @@ namespace smt {
|
|||
literal_vector const& lits() const { return m_lits; }
|
||||
literal lits(unsigned i) const { return m_lits[i]; }
|
||||
dependency* dep() const { return m_dep; }
|
||||
expr_ref const& l() const { return m_l; }
|
||||
expr_ref const& r() const { return m_r; }
|
||||
};
|
||||
|
||||
class apply {
|
||||
|
|
@ -268,7 +276,7 @@ namespace smt {
|
|||
stats m_stats;
|
||||
symbol m_prefix, m_suffix, m_contains_left, m_contains_right, m_accept, m_reject;
|
||||
symbol m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
|
||||
symbol m_extract_prefix, m_at_left, m_at_right;
|
||||
symbol m_pre, m_post, m_eq;
|
||||
ptr_vector<expr> m_todo;
|
||||
expr_ref_vector m_ls, m_rs, m_lhs, m_rhs;
|
||||
|
||||
|
|
@ -326,6 +334,9 @@ namespace smt {
|
|||
bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
|
||||
bool propagate_max_length(expr* l, expr* r, dependency* dep);
|
||||
|
||||
bool get_length(expr* s, expr_ref& len, literal_vector& lits);
|
||||
bool reduce_length(expr* l, expr* r);
|
||||
|
||||
expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
|
||||
expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); }
|
||||
expr_ref mk_concat(expr_ref_vector const& es, sort* s) { if (es.empty()) return mk_empty(s); return mk_concat(es.size(), es.c_ptr()); }
|
||||
|
|
@ -334,12 +345,27 @@ namespace smt {
|
|||
bool solve_nqs(unsigned i);
|
||||
bool solve_ne(unsigned i);
|
||||
|
||||
struct cell {
|
||||
cell* m_parent;
|
||||
expr* m_expr;
|
||||
dependency* m_dep;
|
||||
unsigned m_last;
|
||||
cell(cell* p, expr* e, dependency* d): m_parent(p), m_expr(e), m_dep(d), m_last(0) {}
|
||||
};
|
||||
scoped_ptr_vector<cell> m_all_cells;
|
||||
cell* mk_cell(cell* p, expr* e, dependency* d);
|
||||
void unfold(cell* c, ptr_vector<cell>& cons);
|
||||
void display_explain(std::ostream& out, unsigned indent, expr* e);
|
||||
bool explain_eq(expr* e1, expr* e2, dependency*& dep);
|
||||
bool explain_empty(expr_ref_vector& es, dependency*& dep);
|
||||
|
||||
// asserting consequences
|
||||
void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
|
||||
void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
|
||||
void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
|
||||
void propagate_eq(dependency* dep, enode* n1, enode* n2);
|
||||
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs);
|
||||
void propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs);
|
||||
void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
|
||||
|
||||
u_map<unsigned> m_branch_start;
|
||||
|
|
@ -357,6 +383,7 @@ namespace smt {
|
|||
bool is_nth(expr* a) const;
|
||||
bool is_tail(expr* a, expr*& s, unsigned& idx) const;
|
||||
bool is_eq(expr* e, expr*& a, expr*& b) const;
|
||||
bool is_pre(expr* e, expr*& s, expr*& i);
|
||||
expr_ref mk_nth(expr* s, expr* idx);
|
||||
expr_ref mk_last(expr* e);
|
||||
expr_ref mk_first(expr* e);
|
||||
|
|
@ -376,6 +403,15 @@ namespace smt {
|
|||
void add_replace_axiom(expr* e);
|
||||
void add_extract_axiom(expr* e);
|
||||
void add_length_axiom(expr* n);
|
||||
void add_tail_axiom(expr* e, expr* s);
|
||||
void add_drop_last_axiom(expr* e, expr* s);
|
||||
void add_extract_prefix_axiom(expr* e, expr* s, expr* l);
|
||||
void add_extract_suffix_axiom(expr* e, expr* s, expr* i);
|
||||
bool is_tail(expr* s, expr* i, expr* l);
|
||||
bool is_drop_last(expr* s, expr* i, expr* l);
|
||||
bool is_extract_prefix0(expr* s, expr* i, expr* l);
|
||||
bool is_extract_suffix(expr* s, expr* i, expr* l);
|
||||
|
||||
|
||||
bool has_length(expr *e) const { return m_length.contains(e); }
|
||||
void add_length(expr* e);
|
||||
|
|
@ -445,6 +481,7 @@ namespace smt {
|
|||
void display_disequations(std::ostream& out) const;
|
||||
void display_disequation(std::ostream& out, ne const& e) const;
|
||||
void display_deps(std::ostream& out, dependency* deps) const;
|
||||
void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
|
||||
public:
|
||||
theory_seq(ast_manager& m);
|
||||
virtual ~theory_seq();
|
||||
|
|
|
|||
|
|
@ -190,14 +190,14 @@ public:
|
|||
}
|
||||
|
||||
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
|
||||
m_check_sat_executed = true;
|
||||
|
||||
m_check_sat_executed = true;
|
||||
m_use_solver1_results = false;
|
||||
|
||||
if (get_num_assumptions() != 0 ||
|
||||
num_assumptions > 0 || // assumptions were provided
|
||||
m_ignore_solver1) {
|
||||
// must use incremental solver
|
||||
switch_inc_mode();
|
||||
m_use_solver1_results = false;
|
||||
return m_solver2->check_sat(num_assumptions, assumptions);
|
||||
}
|
||||
|
||||
|
|
@ -206,7 +206,6 @@ public:
|
|||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);
|
||||
lbool r = m_solver2->check_sat(0, 0);
|
||||
if (r != l_undef || !use_solver1_when_undef()) {
|
||||
m_use_solver1_results = false;
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
|
@ -219,7 +218,6 @@ public:
|
|||
r = m_solver2->check_sat(0, 0);
|
||||
}
|
||||
if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) {
|
||||
m_use_solver1_results = false;
|
||||
return r;
|
||||
}
|
||||
if (eh.m_canceled) {
|
||||
|
|
@ -227,7 +225,6 @@ public:
|
|||
}
|
||||
}
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);
|
||||
|
||||
}
|
||||
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";);
|
||||
|
|
|
|||
|
|
@ -75,7 +75,7 @@ class ufbv_rewriter_tactic : public tactic {
|
|||
void updt_params(params_ref const & p) {
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
|
||||
|
|
@ -88,7 +88,7 @@ public:
|
|||
virtual tactic * translate(ast_manager & m) {
|
||||
return alloc(ufbv_rewriter_tactic, m, m_params);
|
||||
}
|
||||
|
||||
|
||||
virtual ~ufbv_rewriter_tactic() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
|
@ -103,19 +103,19 @@ public:
|
|||
insert_produce_models(r);
|
||||
insert_produce_proofs(r);
|
||||
}
|
||||
|
||||
virtual void operator()(goal_ref const & in,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
|
||||
virtual void operator()(goal_ref const & in,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
(*m_imp)(in, result, mc, pc, core);
|
||||
}
|
||||
|
||||
|
||||
virtual void cleanup() {
|
||||
ast_manager & m = m_imp->m();
|
||||
imp * d = alloc(imp, m, m_params);
|
||||
std::swap(d, m_imp);
|
||||
std::swap(d, m_imp);
|
||||
dealloc(d);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -25,4 +25,8 @@ class tactic;
|
|||
|
||||
tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
|
||||
/*
|
||||
ADD_TACTIC("ufbv-rewriter", "Applies UFBV-specific rewriting rules, mainly demodulation.", "mk_quasi_macros_tactic(m, p)")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -46,11 +46,6 @@ public:
|
|||
out_of_memory_error();
|
||||
};
|
||||
|
||||
class exceeded_memory_allocations : public z3_error {
|
||||
public:
|
||||
exceeded_memory_allocations();
|
||||
};
|
||||
|
||||
class memory {
|
||||
public:
|
||||
static bool is_out_of_memory();
|
||||
|
|
|
|||
Loading…
Reference in a new issue