From 2749e547cf546608749df79cc18b150618e5eb87 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Nov 2017 18:14:24 -0800 Subject: [PATCH] fix c example, remove more smtlib1 printing Signed-off-by: Nikolaj Bjorner --- examples/c/test_capi.c | 87 +++---------------------- src/api/api_ast.cpp | 7 +- src/ast/ast_smt_pp.cpp | 106 +------------------------------ src/ast/ast_smt_pp.h | 1 - src/ast/proofs/proof_checker.cpp | 2 +- src/smt/theory_arith_pp.h | 2 +- 6 files changed, 15 insertions(+), 190 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index f6d515389..d71771f98 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -395,11 +395,10 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) t_name = Z3_mk_string_symbol(ctx, "T"); - Z3_parse_smtlib_string(ctx, - "(benchmark comm :formula (forall (x T) (y T) (= (f x y) (f y x))))", + q = Z3_parse_smtlib2_string(ctx, + "(assert (forall ((x T) (y T)) (= (f x y) (f y x))))", 1, &t_name, &t, 1, &f_name, &f); - q = Z3_get_smtlib_formula(ctx, 0); printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q)); Z3_solver_assert(ctx, s, q); } @@ -1632,35 +1631,6 @@ void error_code_example2() { } } -/** - \brief Demonstrates how to use the SMTLIB parser. - */ -void parser_example1() -{ - Z3_context ctx = mk_context(); - Z3_solver s = mk_solver(ctx); - unsigned i, num_formulas; - - printf("\nparser_example1\n"); - LOG_MSG("parser_example1"); - - - Z3_parse_smtlib_string(ctx, - "(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))", - 0, 0, 0, - 0, 0, 0); - num_formulas = Z3_get_smtlib_num_formulas(ctx); - for (i = 0; i < num_formulas; i++) { - Z3_ast f = Z3_get_smtlib_formula(ctx, i); - printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f)); - Z3_solver_assert(ctx, s, f); - } - - check(ctx, s, Z3_L_TRUE); - - del_solver(ctx, s); - Z3_del_context(ctx); -} /** \brief Demonstrates how to initialize the parser symbol table. @@ -1690,12 +1660,11 @@ void parser_example2() names[0] = Z3_mk_string_symbol(ctx, "a"); names[1] = Z3_mk_string_symbol(ctx, "b"); - Z3_parse_smtlib_string(ctx, - "(benchmark tst :formula (> a b))", + f = Z3_parse_smtlib2_string(ctx, + "(assert (> a b))", 0, 0, 0, /* 'x' and 'y' declarations are inserted as 'a' and 'b' into the parser symbol table. */ 2, names, decls); - f = Z3_get_smtlib_formula(ctx, 0); printf("formula: %s\n", Z3_ast_to_string(ctx, f)); Z3_solver_assert(ctx, s, f); check(ctx, s, Z3_L_TRUE); @@ -1737,11 +1706,10 @@ void parser_example3() assert_comm_axiom(ctx, s, g); - Z3_parse_smtlib_string(ctx, - "(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (g x 0) (g 0 y)))))", + thm = Z3_parse_smtlib2_string(ctx, + "(assert (forall ((x Int) (y Int)) (=> (= x y) (= (g x 0) (g 0 y)))))", 0, 0, 0, 1, &g_name, &g); - thm = Z3_get_smtlib_formula(ctx, 0); printf("formula: %s\n", Z3_ast_to_string(ctx, thm)); prove(ctx, s, thm, Z3_TRUE); @@ -1749,41 +1717,6 @@ void parser_example3() Z3_del_context(ctx); } -/** - \brief Display the declarations, assumptions and formulas in a SMT-LIB string. -*/ -void parser_example4() -{ - Z3_context ctx; - unsigned i, num_decls, num_assumptions, num_formulas; - - printf("\nparser_example4\n"); - LOG_MSG("parser_example4"); - - ctx = mk_context(); - - Z3_parse_smtlib_string(ctx, - "(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))", - 0, 0, 0, - 0, 0, 0); - num_decls = Z3_get_smtlib_num_decls(ctx); - for (i = 0; i < num_decls; i++) { - Z3_func_decl d = Z3_get_smtlib_decl(ctx, i); - printf("declaration %d: %s\n", i, Z3_func_decl_to_string(ctx, d)); - } - num_assumptions = Z3_get_smtlib_num_assumptions(ctx); - for (i = 0; i < num_assumptions; i++) { - Z3_ast a = Z3_get_smtlib_assumption(ctx, i); - printf("assumption %d: %s\n", i, Z3_ast_to_string(ctx, a)); - } - num_formulas = Z3_get_smtlib_num_formulas(ctx); - for (i = 0; i < num_formulas; i++) { - Z3_ast f = Z3_get_smtlib_formula(ctx, i); - printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f)); - } - Z3_del_context(ctx); -} - /** \brief Demonstrates how to handle parser errors using Z3 error handling support. */ @@ -1802,9 +1735,9 @@ void parser_example5() { s = mk_solver(ctx); Z3_del_config(cfg); - Z3_parse_smtlib_string(ctx, + Z3_parse_smtlib2_string(ctx, /* the following string has a parsing error: missing parenthesis */ - "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))", + "(declare-const x Int) declare-const y Int) (assert (and (> x y) (> x 0)))", 0, 0, 0, 0, 0, 0); e = Z3_get_error_code(ctx); @@ -1817,7 +1750,7 @@ void parser_example5() { err: printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e)); if (ctx != NULL) { - printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx)); + printf("Error message: '%s'.\n",Z3_get_parser_error(ctx)); del_solver(ctx, s); Z3_del_context(ctx); } @@ -3065,10 +2998,8 @@ int main() { two_contexts_example1(); error_code_example1(); error_code_example2(); - parser_example1(); parser_example2(); parser_example3(); - parser_example4(); parser_example5(); numeral_example(); ite_example(); diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 76b0eb717..ae23ca100 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -872,12 +872,7 @@ extern "C" { for (unsigned i = 0; i < num_assumptions; ++i) { pp.add_assumption(to_expr(assumptions[i])); } - if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) { - pp.display_smt2(buffer, to_expr(formula)); - } - else { - pp.display(buffer, to_expr(formula)); - } + pp.display_smt2(buffer, to_expr(formula)); return mk_c(c)->mk_external_string(buffer.str()); Z3_CATCH_RETURN(""); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 352c8db98..bad4b1984 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -340,8 +340,7 @@ class smt_printer { } - void pp_arg(expr *arg, app *parent) - { + void pp_arg(expr *arg, app *parent) { pp_marked_expr(arg); } @@ -417,7 +416,7 @@ class smt_printer { else if (m_simplify_implies && m_manager.is_implies(decl) && m_manager.is_implies(n->get_arg(1))) { expr *curr = n; expr *arg; - m_out << "(implies (and"; + m_out << "(=> (and"; while (m_manager.is_implies(curr)) { arg = to_app(curr)->get_arg(0); @@ -476,8 +475,7 @@ class smt_printer { } } - void print_no_lets(expr *e) - { + void print_no_lets(expr *e) { 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); } @@ -894,15 +892,6 @@ ast_smt_pp::ast_smt_pp(ast_manager& m): m_simplify_implies(true) {} - -#if 0 -void ast_smt_pp::display_expr(std::ostream& strm, expr* n) { - ptr_vector 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 ql; smt_renaming rn; @@ -1022,92 +1011,3 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { p(n); } } - -void ast_smt_pp::display(std::ostream& strm, expr* n) { - ptr_vector ql; - decl_collector decls(m_manager); - smt_renaming rn; - - for (unsigned i = 0; i < m_assumptions.size(); ++i) { - decls.visit(m_assumptions[i].get()); - } - for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { - decls.visit(m_assumptions_star[i].get()); - } - decls.visit(n); - - strm << "(benchmark "; - - if (m_benchmark_name != symbol::null) { - strm << m_benchmark_name << "\n"; - } - else { - strm << "unnamed\n"; - } - if (m_source_info != symbol::null && m_source_info != symbol("")) { - strm << ":source { " << m_source_info << " }\n"; - } - strm << ":status " << m_status << "\n"; - if (m_category != symbol::null && m_category != symbol("")) { - strm << ":category { " << m_category << " }\n"; - } - if (m_logic != symbol::null && m_logic != symbol("")) { - strm << ":logic " << m_logic << "\n"; - } - - if (m_attributes.size() > 0) { - strm << m_attributes.c_str(); - } - - ast_mark sort_mark; - for (unsigned i = 0; i < decls.get_num_sorts(); ++i) { - sort* s = decls.get_sorts()[i]; - if (!(*m_is_declared)(s)) { - smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0); - p.pp_sort_decl(sort_mark, s); - } - } - - for (unsigned i = 0; i < decls.get_num_decls(); ++i) { - func_decl* d = decls.get_func_decls()[i]; - if (!(*m_is_declared)(d)) { - strm << ":extrafuns ("; - smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0); - p(d); - strm << ")\n"; - } - } - - for (unsigned i = 0; i < decls.get_num_preds(); ++i) { - func_decl* d = decls.get_pred_decls()[i]; - if (!(*m_is_declared)(d)) { - strm << ":extrapreds ("; - smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0); - p.visit_pred(d); - strm << ")\n"; - } - } - - for (unsigned i = 0; i < m_assumptions.size(); ++i) { - expr * e = m_assumptions[i].get(); - strm << ":assumption\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0); - p(e); - strm << "\n"; - } - - for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { - strm << ":assumption-core\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0); - p(m_assumptions_star[i].get()); - strm << "\n"; - } - - { - strm << ":formula\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0); - p(n); - strm << "\n"; - } - strm << ")\n"; -} diff --git a/src/ast/ast_smt_pp.h b/src/ast/ast_smt_pp.h index 41ed06a92..ac2e33140 100644 --- a/src/ast/ast_smt_pp.h +++ b/src/ast/ast_smt_pp.h @@ -75,7 +75,6 @@ public: void set_is_declared(is_declared* id) { m_is_declared = id; } - void display(std::ostream& strm, expr* n); void display_smt2(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); diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index 3f9438229..6fd876efc 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -1284,7 +1284,7 @@ void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecede pp.add_assumption(antecedents[i]); expr_ref n(m); n = m.mk_not(consequent); - pp.display(out, n); + pp.display_smt2(out, n); out.close(); m_proof_lemma_id++; } diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index 67fe5a572..997698411 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -526,7 +526,7 @@ namespace smt { } } } - pp.display(out, m.mk_true()); + pp.display_smt2(out, m.mk_true()); } template