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

tuning for seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-05 08:23:44 -08:00
parent f6be76aec5
commit af758dea4a
5 changed files with 64 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_arith.h
View file

@ -429,6 +429,7 @@ namespace smt {
arith_util m_util;
arith_eq_solver m_arith_eq_solver;
bool m_found_unsupported_op;
bool m_found_underspecified_op;
arith_eq_adapter m_arith_eq_adapter;
vector<row> m_rows;
svector<unsigned> m_dead_rows;
@ -510,6 +511,7 @@ namespace smt {
virtual theory_var mk_var(enode * n);
void found_unsupported_op(app * n);
void found_underspecified_op(app * n);
bool has_var(expr * v) const { return get_context().e_internalized(v) && get_context().get_enode(v)->get_th_var(get_id()) != null_theory_var; }
theory_var expr2var(expr * v) const { SASSERT(get_context().e_internalized(v)); return get_context().get_enode(v)->get_th_var(get_id()); }

3
src/smt/theory_arith_aux.h
View file

@ -2153,6 +2153,9 @@ namespace smt {
*/
template<typename Ext>
bool theory_arith<Ext>::is_shared(theory_var v) const {
if (!m_found_underspecified_op) {
return false;
}
enode * n = get_enode(v);
enode * r = n->get_root();
enode_vector::const_iterator it = r->begin_parents();

14
src/smt/theory_arith_core.h
View file

@ -37,6 +37,15 @@ namespace smt {
}
}
template<typename Ext>
void theory_arith<Ext>::found_underspecified_op(app * n) {
if (!m_found_underspecified_op) {
TRACE("arith", tout << "found non underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
m_found_underspecified_op = true;
}
}
template<typename Ext>
bool theory_arith<Ext>::process_atoms() const {
if (!adaptive())
@ -308,6 +317,7 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_div(app * n) {
found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!ctx.relevancy())
@ -317,6 +327,7 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_idiv(app * n) {
found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
app * mod = m_util.mk_mod(n->get_arg(0), n->get_arg(1));
@ -329,6 +340,7 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_mod(app * n) {
TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!ctx.relevancy())
@ -338,6 +350,7 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_rem(app * n) {
found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!ctx.relevancy()) {
@ -1514,6 +1527,7 @@ namespace smt {
m_util(m),
m_arith_eq_solver(m),
m_found_unsupported_op(false),
m_found_underspecified_op(false),
m_arith_eq_adapter(*this, params, m_util),
m_asserted_qhead(0),
m_to_patch(1024),

57
src/smt/theory_seq.cpp
View file

@ -159,7 +159,6 @@ theory_seq::theory_seq(ast_manager& m):
m_exclude(m),
m_axioms(m),
m_axioms_head(0),
m_branch_variable_head(0),
m_mg(0),
m_rewrite(m),
m_util(m),
@ -234,8 +233,9 @@ bool theory_seq::branch_variable() {
context& ctx = get_context();
unsigned sz = m_eqs.size();
expr_ref_vector ls(m), rs(m);
int start = ctx.get_random_value();
for (unsigned i = 0; i < sz; ++i) {
unsigned k = (i + m_branch_variable_head) % sz;
unsigned k = (i + start) % sz;
eq e = m_eqs[k];
TRACE("seq", tout << e.m_lhs << " = " << e.m_rhs << "\n";);
ls.reset(); rs.reset();
@ -243,21 +243,17 @@ bool theory_seq::branch_variable() {
m_util.str.get_concat(e.m_rhs, rs);
#if 1
if (!ls.empty() && find_branch_candidate(e.m_dep, ls[0].get(), rs)) {
m_branch_variable_head = k;
if (find_branch_candidate(e.m_dep, ls, rs)) {
return true;
}
if (!rs.empty() && find_branch_candidate(e.m_dep, rs[0].get(), ls)) {
m_branch_variable_head = k;
if (find_branch_candidate(e.m_dep, rs, ls)) {
return true;
}
#else
if (ls.size() > 1 && find_branch_candidate(e.m_dep, ls.back(), rs)) {
m_branch_variable_head = k;
if (find_branch_candidate(e.m_dep, ls.back(), rs)) {
return true;
}
if (rs.size() > 1 && find_branch_candidate(e.m_dep, rs.back(), ls)) {
m_branch_variable_head = k;
if (find_branch_candidate(e.m_dep, rs.back(), ls)) {
return true;
}
#endif
@ -273,10 +269,12 @@ bool theory_seq::branch_variable() {
return ctx.inconsistent();
}
bool theory_seq::find_branch_candidate(dependency* dep, expr* l, expr_ref_vector const& rs) {
bool theory_seq::find_branch_candidate(dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs) {
TRACE("seq", tout << mk_pp(l, m) << " "
<< (is_var(l)?"var":"not var") << "\n";);
if (ls.empty()) {
return false;
}
expr* l = ls[0];
if (!is_var(l)) {
return false;
@ -286,7 +284,8 @@ bool theory_seq::find_branch_candidate(dependency* dep, expr* l, expr_ref_vector
expr_ref_vector cases(m);
expr_ref v0(m), v(m);
v0 = m_util.str.mk_empty(m.get_sort(l));
if (l_false != assume_equality(l, v0)) {
if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr()) && l_false != assume_equality(l, v0)) {
TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
return true;
}
for (unsigned j = 0; j < rs.size(); ++j) {
@ -295,8 +294,12 @@ bool theory_seq::find_branch_candidate(dependency* dep, expr* l, expr_ref_vector
}
SASSERT(!m_util.str.is_string(rs[j]));
all_units &= m_util.str.is_unit(rs[j]);
if (!can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - j - 1, rs.c_ptr() + j + 1)) {
continue;
}
v0 = m_util.str.mk_concat(j + 1, rs.c_ptr());
if (l_false != assume_equality(l, v0)) {
TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
return true;
}
}
@ -308,11 +311,37 @@ bool theory_seq::find_branch_candidate(dependency* dep, expr* l, expr_ref_vector
lits.push_back(~mk_eq(l, v0, false));
}
set_conflict(dep, lits);
TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
return true;
}
return false;
}
bool theory_seq::can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const {
unsigned i = 0;
for (; i < szl && i < szr; ++i) {
if (m.are_distinct(ls[i], rs[i])) {
return false;
}
if (!m.are_equal(ls[i], rs[i])) {
break;
}
}
if (i == szr) {
std::swap(ls, rs);
std::swap(szl, szr);
}
if (i == szl && i < szr) {
for (; i < szr; ++i) {
if (m_util.str.is_unit(rs[i])) {
return false;
}
}
}
return true;
}
lbool theory_seq::assume_equality(expr* l, expr* r) {
context& ctx = get_context();
if (m_exclude.contains(l, r)) {

4
src/smt/theory_seq.h
View file

@ -304,7 +304,6 @@ namespace smt {
expr_ref_vector m_axioms; // list of axioms to add.
obj_hashtable<expr> m_axiom_set;
unsigned m_axioms_head; // index of first axiom to add.
unsigned m_branch_variable_head; // index of first equation to examine.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
obj_hashtable<expr> m_length; // is length applied
scoped_ptr_vector<apply> m_replay; // set of actions to replay
@ -387,7 +386,8 @@ namespace smt {
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false);
void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
bool find_branch_candidate(dependency* dep, expr* l, expr_ref_vector const& rs);
bool find_branch_candidate(dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs);
bool can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const;
lbool assume_equality(expr* l, expr* r);
// variable solving utilities