mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
remove SMTLIB1 printing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d1ee5431a7
commit
b8e5fc9f43
|
@ -832,30 +832,9 @@ extern "C" {
|
|||
case Z3_PRINT_LOW_LEVEL:
|
||||
buffer << mk_ll_pp(to_ast(a), mk_c(c)->m());
|
||||
break;
|
||||
case Z3_PRINT_SMTLIB_COMPLIANT: {
|
||||
ast_smt_pp pp(mk_c(c)->m());
|
||||
pp_params params;
|
||||
pp.set_simplify_implies(params.simplify_implies());
|
||||
ast* a1 = to_ast(a);
|
||||
pp.set_logic(mk_c(c)->fparams().m_logic);
|
||||
if (!is_expr(a1)) {
|
||||
buffer << mk_pp(a1, mk_c(c)->m());
|
||||
break;
|
||||
}
|
||||
if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB_COMPLIANT) {
|
||||
pp.display_expr(buffer, to_expr(a1));
|
||||
break;
|
||||
}
|
||||
if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) {
|
||||
pp.display_expr_smt2(buffer, to_expr(a1));
|
||||
break;
|
||||
}
|
||||
break;
|
||||
}
|
||||
case Z3_PRINT_SMTLIB2_COMPLIANT: {
|
||||
case Z3_PRINT_SMTLIB2_COMPLIANT:
|
||||
buffer << mk_ismt2_pp(to_ast(a), mk_c(c)->m());
|
||||
break;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
|
|
@ -1314,13 +1314,11 @@ typedef enum {
|
|||
|
||||
- Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format.
|
||||
- Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
|
||||
- Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format.
|
||||
- Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x compliant format.
|
||||
*/
|
||||
typedef enum {
|
||||
Z3_PRINT_SMTLIB_FULL,
|
||||
Z3_PRINT_LOW_LEVEL,
|
||||
Z3_PRINT_SMTLIB_COMPLIANT,
|
||||
Z3_PRINT_SMTLIB2_COMPLIANT
|
||||
} Z3_ast_print_mode;
|
||||
|
||||
|
@ -5116,7 +5114,7 @@ extern "C" {
|
|||
To print shared common subexpressions only once,
|
||||
use the Z3_PRINT_LOW_LEVEL mode.
|
||||
To print in way that conforms to SMT-LIB standards and uses let
|
||||
expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.
|
||||
expressions to share common sub-expressions use Z3_PRINT_SMTLIB2_COMPLIANT.
|
||||
|
||||
\sa Z3_ast_to_string
|
||||
\sa Z3_pattern_to_string
|
||||
|
|
|
@ -478,7 +478,7 @@ class smt_printer {
|
|||
|
||||
void print_no_lets(expr *e)
|
||||
{
|
||||
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, true, m_simplify_implies, true, m_indent, m_num_var_names, m_var_names);
|
||||
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, true, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
|
||||
p(e);
|
||||
}
|
||||
|
||||
|
@ -511,7 +511,7 @@ class smt_printer {
|
|||
m_out << "(! ";
|
||||
}
|
||||
{
|
||||
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, true, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
|
||||
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
|
||||
p(q->get_expr());
|
||||
}
|
||||
|
||||
|
@ -704,7 +704,7 @@ class smt_printer {
|
|||
|
||||
public:
|
||||
smt_printer(std::ostream& out, ast_manager& m, ptr_vector<quantifier>& ql, smt_renaming& rn,
|
||||
symbol logic, bool no_lets, bool is_smt2, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = 0) :
|
||||
symbol logic, bool no_lets, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = 0) :
|
||||
m_out(out),
|
||||
m_manager(m),
|
||||
m_qlists(ql),
|
||||
|
@ -895,24 +895,25 @@ ast_smt_pp::ast_smt_pp(ast_manager& m):
|
|||
{}
|
||||
|
||||
|
||||
#if 0
|
||||
void ast_smt_pp::display_expr(std::ostream& strm, expr* n) {
|
||||
ptr_vector<quantifier> ql;
|
||||
smt_renaming rn;
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0);
|
||||
ptr_vector<quantifier> ql; smt_renaming rn;
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, false, m_simplify_implies, 0);
|
||||
p(n);
|
||||
}
|
||||
#endif
|
||||
|
||||
void ast_smt_pp::display_expr_smt2(std::ostream& strm, expr* n, unsigned indent, unsigned num_var_names, char const* const* var_names) {
|
||||
ptr_vector<quantifier> ql;
|
||||
smt_renaming rn;
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, indent, num_var_names, var_names);
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, false, m_simplify_implies, indent, num_var_names, var_names);
|
||||
p(n);
|
||||
}
|
||||
|
||||
void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, unsigned num_var_names, char const* const* var_names) {
|
||||
ptr_vector<quantifier> ql;
|
||||
smt_renaming rn;
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, indent, num_var_names, var_names);
|
||||
smt_printer p(strm, m_manager, ql, rn, m_logic, false, m_simplify_implies, indent, num_var_names, var_names);
|
||||
if (is_expr(a)) {
|
||||
p(to_expr(a));
|
||||
}
|
||||
|
|
|
@ -77,7 +77,6 @@ public:
|
|||
|
||||
void display(std::ostream& strm, expr* n);
|
||||
void display_smt2(std::ostream& strm, expr* n);
|
||||
void display_expr(std::ostream& strm, expr* n);
|
||||
void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);
|
||||
void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);
|
||||
|
||||
|
|
Loading…
Reference in a new issue