3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

print lemmas2console faster

- add option pp.no_lets (default = false) to print formulas without let (used by the low-level SMT2 printer).
- print lemmas2console faster by using the low level printer
This commit is contained in:
Nikolaj Bjorner 2023-03-20 17:06:14 +01:00
parent a9e6e567b0
commit c6e3fb446a
4 changed files with 8 additions and 2 deletions

View file

@ -34,6 +34,7 @@ Revision History:
#include "ast/for_each_ast.h"
#include "ast/decl_collector.h"
#include "math/polynomial/algebraic_numbers.h"
#include "ast/pp_params.hpp"
// ---------------------------------------
@ -911,7 +912,9 @@ ast_smt_pp::ast_smt_pp(ast_manager& m):
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, m_simplify_implies, indent, num_var_names, var_names);
pp_params params;
bool no_lets = params.no_lets();
smt_printer p(strm, m_manager, ql, rn, m_logic, no_lets, m_simplify_implies, indent, num_var_names, var_names);
p(n);
}

View file

@ -6,6 +6,7 @@ def_module_params('pp',
('max_width', UINT, 80, 'max. width in pretty printer'),
('max_ribbon', UINT, 80, 'max. ribbon (width - indentation) in pretty printer'),
('max_depth', UINT, 5, 'max. term depth (when pretty printing SMT2 terms/formulas)'),
('no_lets', BOOL, False, 'dont print lets in low level SMT printer'),
('min_alias_size', UINT, 10, 'min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)'),
('decimal', BOOL, False, 'pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise'),
('decimal_precision', UINT, 10, 'maximum number of decimal places to be used when pp.decimal=true'),

View file

@ -22,6 +22,8 @@ Author:
class elim_unconstrained : public dependent_expr_simplifier {
friend class seq_simplifier;
struct node {
unsigned m_refcount = 0;
expr* m_term = nullptr;

View file

@ -1536,7 +1536,7 @@ namespace smt {
fml = mk_or(fmls);
m_lemma_visitor.collect(fml);
m_lemma_visitor.display_skolem_decls(std::cout);
m_lemma_visitor.display_assert(std::cout, fml.get(), true);
m_lemma_visitor.display_assert(std::cout, fml.get(), false);
}
}