From cefa2d765014b8a41074676d7e4c71a463a2f3cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Nov 2012 13:11:34 -0800 Subject: [PATCH] add option to print with variable declarations Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index ec78f8e92..14de8550e 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -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 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); }