mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fixup compiled patterns

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-29 11:42:40 -07:00
parent 1c694fd42f
commit 3afe081f62
5 changed files with 54 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/pattern/expr_pattern_match.cpp
View file

@ -102,7 +102,7 @@ expr_pattern_match::instantiate(expr* a, unsigned num_bound, subst& s, expr_ref&
for (unsigned i = 0; i < num_bound; ++i) {
b.insert(m_bound_dom[i], m_bound_rng[i]);
}
TRACE("expr_pattern_match", tout << mk_pp(a, m_manager) << " " << num_bound << "\n";);
inst_proc proc(m_manager, s, b, m_regs);
for_each_ast(proc, a);
expr* v = nullptr;
@ -273,11 +273,7 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s)
break;
}
case CHECK_BOUND:
TRACE("expr_pattern_match",
tout
<< "check bound "
<< pc.m_num_bound << " " << pc.m_reg;
);
TRACE("expr_pattern_match", tout << "check bound " << pc.m_num_bound << " " << pc.m_reg << "\n";);
ok = m_bound_rng[pc.m_num_bound] == m_regs[pc.m_reg];
break;
case BIND:
@ -418,7 +414,6 @@ expr_pattern_match::initialize(char const * spec_string) {
for (expr * e : ctx.assertions()) {
compile(e);
}
TRACE("expr_pattern_match", display(tout); );
}
unsigned expr_pattern_match::initialize(quantifier* q) {
@ -444,7 +439,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case BIND:
out << "bind ";
out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
@ -452,7 +446,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case BIND_AC:
out << "bind_ac ";
out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
@ -460,7 +453,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case BIND_C:
out << "bind_c ";
out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";

21
src/ast/pattern/expr_pattern_match.h
View file

@ -80,13 +80,7 @@ class expr_pattern_match {
}
void operator()(var* v) {
var* b = nullptr;
if (m_bound.find(v, b)) {
m_memoize.insert(v, b);
}
else {
UNREACHABLE();
}
m_memoize.insert(v, m_bound[v]);
}
void operator()(app * n) {
@ -98,15 +92,9 @@ class expr_pattern_match {
if (m_subst.find(decl, r)) {
decl = to_app(m_regs[r])->get_decl();
}
for (unsigned i = 0; i < num_args; ++i) {
expr* arg = nullptr;
if (m_memoize.find(n->get_arg(i), arg)) {
SASSERT(arg);
args.push_back(arg);
}
else {
UNREACHABLE();
}
for (expr* arg : *n) {
arg = m_memoize[arg];
args.push_back(arg);
}
if (m_manager.is_pattern(n)) {
result = m_manager.mk_pattern(num_args, reinterpret_cast<app**>(args.c_ptr()));
@ -116,7 +104,6 @@ class expr_pattern_match {
}
m_pinned.push_back(result);
m_memoize.insert(n, result);
return;
}
};