diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-04-18 09:22:37 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-18 07:22:37 -0500 |
commit | 55497dfdff15f4bb3d839f64a7baa46c3aa84266 (patch) | |
tree | a8c9ac1ab3590beead09da968f3916ac295c72fc /src/theory/uf/equality_engine.cpp | |
parent | c431160c5c9d706cd6424dc6c4b9b316ff8a5941 (diff) |
Improving EqProof printing (#4329)
Diffstat (limited to 'src/theory/uf/equality_engine.cpp')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 44 |
1 files changed, 30 insertions, 14 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index e3d002138..60883e4ef 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -2432,26 +2432,42 @@ void EqProof::debug_print(std::ostream& os, } else { - os << d_id; + os << static_cast<MergeReasonType>(d_id); } - os << "("; - if( !d_children.empty() || !d_node.isNull() ){ - if( !d_node.isNull() ){ - os << std::endl; - for (unsigned i = 0; i < tb + 1; i++) + if (d_children.empty() && d_node.isNull()) + { + os << ")"; + return; + } + if (!d_node.isNull()) + { + os << std::endl; + for (unsigned i = 0; i < tb + 1; ++i) + { + os << " "; + } + os << d_node << (!d_children.empty() ? "," : ""); + } + unsigned size = d_children.size(); + for (unsigned i = 0; i < size; ++i) + { + os << std::endl; + d_children[i]->debug_print(os, tb + 1, prettyPrinter); + if (i < size - 1) + { + for (unsigned j = 0; j < tb + 1; ++j) { os << " "; } - os << d_node; + os << ","; } - for( unsigned i=0; i<d_children.size(); i++ ){ - if (i > 0 || !d_node.isNull()) - { - os << ","; - } - os << std::endl; - d_children[i]->debug_print(os, tb + 1, prettyPrinter); + } + if (size > 0) + { + for (unsigned i = 0; i < tb; ++i) + { + os << " "; } } os << ")" << std::endl; |