mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

cleanup

Browse source
This commit is contained in:
Murphy Berzish 2017-05-03 17:45:56 -04:00
parent 41a242fab1
commit ab4fbe40b6
7 changed files with 11 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast_smt2_pp.h
View file

@ -55,8 +55,8 @@ public:
virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg);
virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec);
virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits);
virtual format_ns::format * pp_string_literal(app * t);
virtual format_ns::format * pp_datalog_literal(app * t);
virtual format_ns::format * pp_string_literal(app * t);
virtual format_ns::format * pp_sort(sort * s);
virtual format_ns::format * pp_fdecl_ref(func_decl * f);
format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len) const;

1
src/ast/ast_smt_pp.cpp
View file

@ -406,7 +406,6 @@ class smt_printer {
void visit_app(app* n) {
rational val;
const char *str;
bool is_int, pos;
buffer<symbol> names;
unsigned bv_size;

1
src/ast/rewriter/rewriter.txt
View file

@ -8,7 +8,6 @@ The following classes implement theory specific rewriting rules:
- datatype_rewriter
- fpa_rewriter
- seq_rewriter
- str_rewriter
Each of them provide the method
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result)