From 3bf6af44bf56264aa4b1aa23c0653a728d291e7d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Oct 2012 09:00:38 -0700 Subject: [PATCH] expose additional external options for muz Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 2 +- src/muz_qe/pdr_dl_interface.cpp | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index b72e6353a..bf25e0277 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -968,7 +968,7 @@ namespace datalog { p.insert(":fix-unbound-vars", CPK_BOOL, "fix unbound variables in tail"); p.insert(":default-table-checker", CPK_SYMBOL, "see :default-table-checked"); - PRIVATE_PARAMS(p.insert(":inline-linear", CPK_BOOL, "try linear inlining method");); + p.insert(":inline-linear", CPK_BOOL, "try linear inlining method"); PRIVATE_PARAMS(p.insert(":inline-linear-branch", CPK_BOOL, "try linear inlining method with potential expansion");); pdr::dl_interface::collect_params(p); diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index d6fc1c931..d229361bb 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -122,8 +122,10 @@ lbool dl_interface::query(expr * query) { if (m_ctx.get_params().get_uint(":unfold-rules",0) > 0) { unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules",0); datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx); - //transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx)); - //m_ctx.transform_rules(transformer1, mc, pc); + if (m_ctx.get_params().get_uint(":coalesce-rules", false)) { + transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx)); + m_ctx.transform_rules(transformer1, mc, pc); + } transformer2.register_plugin(alloc(datalog::mk_unfold, m_ctx)); while (num_unfolds > 0) { m_ctx.transform_rules(transformer2, mc, pc); @@ -216,4 +218,5 @@ void dl_interface::collect_params(param_descrs& p) { PRIVATE_PARAMS(p.insert(":simplify-formulas-pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation");); PRIVATE_PARAMS(p.insert(":simplify-formulas-post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation");); p.insert(":slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing"); + p.insert(":coalesce-rules", CPK_BOOL, "PDR: (default false) coalesce rules"); }