mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master' into lackr

Browse source
This commit is contained in:
Mikolas Janota 2016-01-26 16:51:57 +00:00
parent c63f9f4912 8e378062e2
commit 470f8bca73
7 changed files with 466 additions and 251 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -383,7 +383,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
zstring s;
rational pos, len;
if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) {
pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() + len.get_unsigned() <= s.length()) {
unsigned _pos = pos.get_unsigned();
unsigned _len = len.get_unsigned();
result = m_util.str.mk_string(s.extract(_pos, _len));
@ -538,34 +538,40 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
}
}
}
if (a1 != b1) {
return BR_FAILED;
}
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
unsigned i = 0;
bool all_values = true;
expr_ref_vector eqs(m());
for (; i < as.size() && i < bs.size(); ++i) {
all_values &= m().is_value(as[i].get()) && m().is_value(bs[i].get());
if (as[i].get() != bs[i].get()) {
if (all_values) {
result = m().mk_false();
return BR_DONE;
}
break;
expr* a = as[i].get(), *b = bs[i].get();
if (a == b) {
continue;
}
};
all_values &= m().is_value(a) && m().is_value(b);
if (all_values) {
result = m().mk_false();
return BR_DONE;
}
if (m_util.str.is_unit(a) && m_util.str.is_unit(b)) {
eqs.push_back(m().mk_eq(a, b));
continue;
}
break;
}
if (i == as.size()) {
result = m().mk_true();
return BR_DONE;
result = mk_and(eqs);
if (m().is_true(result)) {
return BR_DONE;
}
return BR_REWRITE3;
}
SASSERT(i < as.size());
if (i == bs.size()) {
expr_ref_vector es(m());
for (unsigned j = i; j < as.size(); ++j) {
es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
eqs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
}
result = mk_and(es);
result = mk_and(eqs);
return BR_REWRITE3;
}
if (i > 0) {
@ -575,8 +581,9 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
result = m_util.str.mk_prefix(a, b);
return BR_DONE;
}
UNREACHABLE();
return BR_FAILED;
else {
return BR_FAILED;
}
}
br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
@ -1221,19 +1228,19 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
SASSERT(m().get_sort(ch) == m().get_sort(a));
lhs.push_back(ch);
rhs.push_back(a);
ls.pop_back();
++head1;
if (s.length() == 1) {
rs.pop_back();
++head2;
}
else {
expr_ref s2(m_util.str.mk_string(s.extract(1, s.length()-1)), m());
rs[rs.size()-1] = s2;
rs[head2] = s2;
}
}
else {
break;
}
TRACE("seq", tout << "change front\n";);
TRACE("seq", tout << ls << " == " << rs << "\n";);
change = true;
lchange = true;

23
src/ast/seq_decl_plugin.cpp
View file

@ -143,11 +143,15 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
if (eq) {
result.m_buffer.append(dst.m_buffer);
found = true;
i += src.length() - 1;
}
else {
result.m_buffer.push_back(m_buffer[i]);
}
}
for (unsigned i = length() - src.length() + 1; i < length(); ++i) {
result.m_buffer.push_back(m_buffer[i]);
}
return result;
}
@ -554,7 +558,11 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
parameter param(symbol(""));
return mk_func_decl(OP_STRING_CONST, 1, &param, 0, 0, m_string);
}
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
else {
parameter param(rng.get());
func_decl_info info(m_family_id, k, 1, &param);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, info);
}
case OP_SEQ_UNIT:
case OP_RE_PLUS:
@ -736,6 +744,19 @@ bool seq_decl_plugin::is_value(app* e) const {
m_manager->is_value(e->get_arg(0)));
}
expr* seq_decl_plugin::get_some_value(sort* s) {
seq_util util(*m_manager);
if (util.is_seq(s)) {
return util.str.mk_empty(s);
}
sort* seq;
if (util.is_re(s, seq)) {
return util.re.mk_to_re(util.str.mk_empty(seq));
}
UNREACHABLE();
return 0;
}
app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
SASSERT(range);
parameter param(name);

3
src/ast/seq_decl_plugin.h
View file

@ -177,10 +177,13 @@ public:
virtual bool is_unique_value(app * e) const { return is_value(e); }
virtual expr * get_some_value(sort * s);
bool is_char(ast* a) const { return a == m_char; }
app* mk_string(symbol const& s);
app* mk_string(zstring const& s);
};
class seq_util {

1
src/cmd_context/cmd_context.cpp
View file

@ -1638,6 +1638,7 @@ void cmd_context::validate_model() {
catch (contains_array_op_proc::found) {
continue;
}
TRACE("model_validate", model_smt2_pp(tout, *this, *(md.get()), 0););
throw cmd_exception("an invalid model was generated");
}
}

600
src/smt/theory_seq.cpp
View file

File diff suppressed because it is too large Load diff

24
src/smt/theory_seq.h
View file

@ -45,6 +45,8 @@ namespace smt {
typedef std::pair<expr*, dependency*> expr_dep;
typedef obj_map<expr, expr_dep> eqdep_map_t;
class seq_value_proc;
// cache to track evaluations under equalities
class eval_cache {
eqdep_map_t m_map;
@ -138,8 +140,7 @@ namespace smt {
m_util.str.get_concat(l, ls);
m_util.str.get_concat(r, rs);
return eq(m_eq_id++, ls, rs, dep);
}
}
class ne {
vector<expr_ref_vector> m_lhs;
@ -355,6 +356,7 @@ namespace smt {
bool add_solution(expr* l, expr* r, dependency* dep);
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;
expr_ref mk_nth(expr* s, expr* idx);
expr_ref mk_last(expr* e);
expr_ref mk_first(expr* e);
@ -369,7 +371,7 @@ namespace smt {
// terms whose meaning are encoded using axioms.
void enque_axiom(expr* e);
void deque_axiom(expr* e);
void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal);
void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);
void add_indexof_axiom(expr* e);
void add_replace_axiom(expr* e);
void add_extract_axiom(expr* e);
@ -385,7 +387,7 @@ namespace smt {
void add_in_re_axiom(expr* n);
literal mk_literal(expr* n);
literal mk_eq_empty(expr* n);
literal mk_equals(expr* a, expr* b);
literal mk_seq_eq(expr* a, expr* b);
void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
expr_ref mk_sub(expr* a, expr* b);
enode* ensure_enode(expr* a);
@ -421,12 +423,14 @@ namespace smt {
bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
bool is_step(expr* e) const;
void propagate_step(literal lit, expr* n);
bool add_reject2reject(expr* rej);
bool add_accept2step(expr* acc);
bool add_step2accept(expr* step);
bool add_prefix2prefix(expr* e);
bool add_suffix2suffix(expr* e);
bool add_contains2contains(expr* e);
bool add_reject2reject(expr* rej, bool& change);
bool add_accept2step(expr* acc, bool& change);
bool add_step2accept(expr* step, bool& change);
bool add_prefix2prefix(expr* e, bool& change);
bool add_suffix2suffix(expr* e, bool& change);
bool add_contains2contains(expr* e, bool& change);
void propagate_not_prefix(expr* e);
void propagate_not_suffix(expr* e);
void ensure_nth(literal lit, expr* s, expr* idx);
bool canonizes(bool sign, expr* e);
void propagate_non_empty(literal lit, expr* s);

13
src/tactic/smtlogics/quant_tactics.h
View file

@ -32,4 +32,17 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p);
tactic * mk_lia_tactic(ast_manager & m, params_ref const & p);
tactic * mk_lira_tactic(ast_manager & m, params_ref const & p);
/*
ADD_TACTIC("ufnia", "builtin strategy for solving UFNIA problems.", "mk_ufnia_tactic(m, p)")
ADD_TACTIC("uflra", "builtin strategy for solving UFLRA problems.", "mk_uflra_tactic(m, p)")
ADD_TACTIC("auflia", "builtin strategy for solving AUFLIA problems.", "mk_auflia_tactic(m, p)")
ADD_TACTIC("auflira", "builtin strategy for solving AUFLIRA problems.", "mk_auflira_tactic(m, p)")
ADD_TACTIC("aufnira", "builtin strategy for solving AUFNIRA problems.", "mk_aufnira_tactic(m, p)")
ADD_TACTIC("lra", "builtin strategy for solving LRA problems.", "mk_lra_tactic(m, p)")
ADD_TACTIC("lia", "builtin strategy for solving LIA problems.", "mk_lia_tactic(m, p)")
ADD_TACTIC("lira", "builtin strategy for solving LIRA problems.", "mk_lira_tactic(m, p)")
*/
#endif