mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

logging which theory added constraints

Browse source
This commit is contained in:
nilsbecker 2018-10-05 13:58:22 +02:00
parent fd9fd52271
commit a0f6447a33
1 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/smt_internalizer.cpp
View file

@ -1018,8 +1018,17 @@ namespace smt {
void context::apply_sort_cnstr(app * term, enode * e) { void context::apply_sort_cnstr(app * term, enode * e) {
sort * s = term->get_decl()->get_range(); sort * s = term->get_decl()->get_range();
theory * th = m_theories.get_plugin(s->get_family_id()); theory * th = m_theories.get_plugin(s->get_family_id());
if (th) if (th) {
if (m_manager.has_trace_stream()) {
m_manager.trace_stream() << "[theory-constraints] " << m_manager.get_family_name(s->get_family_id()) << "\n";
}
th->apply_sort_cnstr(e, s); th->apply_sort_cnstr(e, s);
if (m_manager.has_trace_stream()) {
m_manager.trace_stream() << "[end-theory-constraints]\n";
}
}
} }
/** /**