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

expose additional external options for muz

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-10-29 09:00:38 -07:00
parent f14cc76caa
commit 3bf6af44bf
2 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_context.cpp
View file

@ -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);

7
src/muz_qe/pdr_dl_interface.cpp
View file

@ -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");
}