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

add option to print with variable declarations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-29 13:11:34 -08:00
parent 0733db382f
commit cefa2d7650
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/dl_context.cpp
View file

@ -995,6 +995,7 @@ namespace datalog {
p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
p.insert(":print-low-level-smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
p.insert(":print-with-variable-declarations", CPK_BOOL, "(default true) use variable declarations when displaying rules (instead of attempting to use original names)");
PRIVATE_PARAMS(
p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL,
@ -1652,6 +1653,7 @@ namespace datalog {
svector<symbol> names;
bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
bool print_low_level = m_params.get_bool(":print-low-level-smt2", false);
bool do_declare_vars = m_params.get_bool(":print-with-variable-declarations", true);
#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params);
@ -1708,7 +1710,7 @@ namespace datalog {
out << "))\n";
}
if (use_fixedpoint_extensions) {
if (use_fixedpoint_extensions && do_declare_vars) {
declare_vars(rules, fresh_names, out);
}