mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

print weight if it is different from default #2667

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-13 19:24:59 -08:00
parent 5f90e72d85
commit 784e2721dd
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast_smt2_pp.cpp
View file

@ -957,8 +957,8 @@ class smt2_printer {
unsigned num_lets = 0; unsigned num_lets = 0;
format * f_body = pp_let(m_format_stack.back(), num_lets); format * f_body = pp_let(m_format_stack.back(), num_lets);
// The current SMT2 frontend uses weight 1 as default. // The current SMT2 frontend uses weight 1 as default.
#define MIN_WEIGHT 1 #define DEFAULT_WEIGHT 1
if (q->has_patterns() || q->get_weight() > MIN_WEIGHT || if (q->has_patterns() || q->get_weight() != DEFAULT_WEIGHT ||
q->get_skid() != symbol::null || (q->get_qid() != symbol::null && !q->get_qid().is_numerical())) { q->get_skid() != symbol::null || (q->get_qid() != symbol::null && !q->get_qid().is_numerical())) {
ptr_buffer<format> buf; ptr_buffer<format> buf;
buf.push_back(f_body); buf.push_back(f_body);
@ -976,7 +976,7 @@ class smt2_printer {
buf.push_back(pp_attribute(":no-pattern ", *it)); buf.push_back(pp_attribute(":no-pattern ", *it));
} }
} }
if (q->get_weight() > MIN_WEIGHT) { if (q->get_weight() != DEFAULT_WEIGHT) {
buf.push_back(pp_simple_attribute(":weight ", q->get_weight())); buf.push_back(pp_simple_attribute(":weight ", q->get_weight()));
} }
if (q->get_skid() != symbol::null) { if (q->get_skid() != symbol::null) {