From 24961dc5f16645b345f99c13cb30b5b46764040a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jul 2014 14:42:00 -0700 Subject: [PATCH] feat(ast/ast_smt_pp): display quantifier QID when printing proofs, feature requested by Dan Rosen Signed-off-by: Leonardo de Moura --- src/ast/ast_smt_pp.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index f684879ae..59e5c04b9 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -569,8 +569,8 @@ class smt_printer { m_out << ")"; } - if (m_is_smt2 && q->get_num_patterns() > 0) { - m_out << "(!"; + if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) { + m_out << "(! "; } { smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_is_smt2, m_simplify_implies, m_indent, m_num_var_names, m_var_names); @@ -609,7 +609,11 @@ class smt_printer { m_out << "}"; } } - if (m_is_smt2 && q->get_num_patterns() > 0) { + + if (q->get_qid() != symbol::null) + m_out << " :qid " << q->get_qid(); + + if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) { m_out << ")"; } m_out << ")";