From 465d28e160700580c31078f0c5548c3622d5b1ec Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 5 Jan 2016 14:57:41 +0000 Subject: [PATCH 1/3] seq_decl: fix build with stricter compilers get rid of 32 rellocations as a nice side-effect --- src/ast/seq_decl_plugin.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 44901b506..9c8a085e8 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -80,8 +80,9 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const { return result; } -static char* esc_table[32] = { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N", - "^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"}; +static const char esc_table[32][3] = + { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N", + "^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"}; std::string zstring::encode() const { SASSERT(m_encoding == ascii); From af758dea4ae0b7c438de749977ade9d3f19407de Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Jan 2016 08:23:44 -0800 Subject: [PATCH 2/3] tuning for seq Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 2 ++ src/smt/theory_arith_aux.h | 3 ++ src/smt/theory_arith_core.h | 14 +++++++++ src/smt/theory_seq.cpp | 57 ++++++++++++++++++++++++++++--------- src/smt/theory_seq.h | 4 +-- 5 files changed, 64 insertions(+), 16 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 2f5590e25..7b56f19e5 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -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 m_rows; svector 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()); } diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 2473b32ab..4291590c6 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -2153,6 +2153,9 @@ namespace smt { */ template bool theory_arith::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(); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index d6fe16089..4561e1ced 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -37,6 +37,15 @@ namespace smt { } } + template + void theory_arith::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(m_found_underspecified_op)); + m_found_underspecified_op = true; + } + } + template bool theory_arith::process_atoms() const { if (!adaptive()) @@ -308,6 +317,7 @@ namespace smt { template theory_var theory_arith::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 theory_var theory_arith::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 theory_var theory_arith::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 theory_var theory_arith::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), diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index e3ede010c..0592f88d9 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -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)) { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index cd8d67cd1..12975b94d 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -304,7 +304,6 @@ namespace smt { expr_ref_vector m_axioms; // list of axioms to add. obj_hashtable 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 m_length; // is length applied scoped_ptr_vector 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 From 752a973e53bd21da97b34fb715c7bda7a097a483 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Jan 2016 08:32:48 -0800 Subject: [PATCH 3/3] missing files? Signed-off-by: Nikolaj Bjorner --- src/api/java/ReExpr.java | 33 +++++++++++++++++++++++++++++++++ src/api/java/ReSort.java | 29 +++++++++++++++++++++++++++++ src/api/java/SeqExpr.java | 33 +++++++++++++++++++++++++++++++++ src/api/java/SeqSort.java | 29 +++++++++++++++++++++++++++++ 4 files changed, 124 insertions(+) create mode 100644 src/api/java/ReExpr.java create mode 100644 src/api/java/ReSort.java create mode 100644 src/api/java/SeqExpr.java create mode 100644 src/api/java/SeqSort.java diff --git a/src/api/java/ReExpr.java b/src/api/java/ReExpr.java new file mode 100644 index 000000000..60dc2bf96 --- /dev/null +++ b/src/api/java/ReExpr.java @@ -0,0 +1,33 @@ +/** +Copyright (c) 2012-2016 Microsoft Corporation + +Module Name: + + ReExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + +package com.microsoft.z3; + +/** + * Re expressions + **/ +public class ReExpr extends Expr +{ + /** + * Constructor for ReExpr + * @throws Z3Exception on error + **/ + ReExpr(Context ctx, long obj) + { + super(ctx, obj); + } +} diff --git a/src/api/java/ReSort.java b/src/api/java/ReSort.java new file mode 100644 index 000000000..74e7c5c5f --- /dev/null +++ b/src/api/java/ReSort.java @@ -0,0 +1,29 @@ +/** +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + ReSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + +package com.microsoft.z3; + +/** + * A Regular expression sort + **/ +public class ReSort extends Sort +{ + ReSort(Context ctx, long obj) + { + super(ctx, obj); + } +} diff --git a/src/api/java/SeqExpr.java b/src/api/java/SeqExpr.java new file mode 100644 index 000000000..47976dd5e --- /dev/null +++ b/src/api/java/SeqExpr.java @@ -0,0 +1,33 @@ +/** +Copyright (c) 2012-2016 Microsoft Corporation + +Module Name: + + SeqExpr.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + +package com.microsoft.z3; + +/** + * Seq expressions + **/ +public class SeqExpr extends Expr +{ + /** + * Constructor for SeqExpr + * @throws Z3Exception on error + **/ + SeqExpr(Context ctx, long obj) + { + super(ctx, obj); + } +} diff --git a/src/api/java/SeqSort.java b/src/api/java/SeqSort.java new file mode 100644 index 000000000..5c7a549c9 --- /dev/null +++ b/src/api/java/SeqSort.java @@ -0,0 +1,29 @@ +/** +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + SeqSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + +package com.microsoft.z3; + +/** + * A Sequence sort + **/ +public class SeqSort extends Sort +{ + SeqSort(Context ctx, long obj) + { + super(ctx, obj); + } +}