From 7e66a65e980402cb5c6ee464ae9fdb7b669bfd93 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Dec 2012 10:32:00 -0800 Subject: [PATCH] Add blast_distinct_threshold option to rewriter. Enable blast_distinct in the QF_LIA default strategy Signed-off-by: Leonardo de Moura --- src/ast/rewriter/bool_rewriter.cpp | 3 ++- src/ast/rewriter/bool_rewriter.h | 1 + src/ast/rewriter/bool_rewriter_params.pyg | 4 +++- src/tactic/smtlogics/qflia_tactic.cpp | 2 ++ 4 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index b5f18a461..5b0c38616 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -27,6 +27,7 @@ void bool_rewriter::updt_params(params_ref const & _p) { m_local_ctx = p.local_ctx(); m_local_ctx_limit = p.local_ctx_limit(); m_blast_distinct = p.blast_distinct(); + m_blast_distinct_threshold = p.blast_distinct_threshold(); m_ite_extra_rules = p.ite_extra_rules(); } @@ -746,7 +747,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args return BR_DONE; } - if (m_blast_distinct) { + if (m_blast_distinct && num_args < m_blast_distinct_threshold) { ptr_buffer new_diseqs; for (unsigned i = 0; i < num_args; i++) { for (unsigned j = i + 1; j < num_args; j++) diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index b1a177247..ef6dc2d38 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -55,6 +55,7 @@ class bool_rewriter { bool m_local_ctx; bool m_elim_and; bool m_blast_distinct; + unsigned m_blast_distinct_threshold; bool m_ite_extra_rules; unsigned m_local_ctx_limit; unsigned m_local_ctx_cost; diff --git a/src/ast/rewriter/bool_rewriter_params.pyg b/src/ast/rewriter/bool_rewriter_params.pyg index a5bcf6f5d..531bf4db9 100644 --- a/src/ast/rewriter/bool_rewriter_params.pyg +++ b/src/ast/rewriter/bool_rewriter_params.pyg @@ -6,4 +6,6 @@ def_module_params(module_name='rewriter', ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"), ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"), ("local_ctx_limit", UINT, UINT_MAX, "limit for applying local context simplifier"), - ("blast_distinct", BOOL, False, "expand a distinct predicate into a quadratic number of disequalities"))) + ("blast_distinct", BOOL, False, "expand a distinct predicate into a quadratic number of disequalities"), + ("blast_distinct_threshold", UINT, UINT_MAX, "when blast_distinct is true, only distinct expressions with less than this number of arguments are blasted") + )) diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index 6b05cff96..6fbf34255 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -172,6 +172,8 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; main_p.set_bool("elim_and", true); main_p.set_bool("som", true); + main_p.set_bool("blast_distinct", true); + main_p.set_uint("blast_distinct_threshold", 128); // main_p.set_bool("push_ite_arith", true); params_ref pull_ite_p;