From 219b47822b8912c1d8846820635589cf12d25dbb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jun 2016 10:13:16 -0700 Subject: [PATCH] avoid qsat when formulas are quantifier-free. Go directly to SMT Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 1 + src/muz/pdr/pdr_prop_solver.h | 3 +++ src/tactic/smtlogics/quant_tactics.cpp | 6 ++++-- 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 1c25b015d..3a735165a 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -889,6 +889,7 @@ namespace pdr { void model_node::dequeue(model_node*& root) { TRACE("pdr", tout << this << " " << state() << "\n";); + root = 0; if (!m_next && !m_prev) return; SASSERT(m_next); SASSERT(m_prev); diff --git a/src/muz/pdr/pdr_prop_solver.h b/src/muz/pdr/pdr_prop_solver.h index ad7e1fd9a..58bd611a9 100644 --- a/src/muz/pdr/pdr_prop_solver.h +++ b/src/muz/pdr/pdr_prop_solver.h @@ -87,6 +87,9 @@ namespace pdr { void set_subset_based_core(bool f) { m_subset_based_core = f; } void set_consequences(expr_ref_vector* consequences) { m_consequences = consequences; } + + void set_background_assumptions(expr_ref_vector const& assumptions); + bool assumes_level() const { return m_assumes_level; } void add_level(); diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 045b0ec87..bc3585d09 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -114,8 +114,10 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { #else tactic * st = and_then(mk_quant_preprocessor(m), mk_qe_lite_tactic(m, p), - or_else(mk_qsat_tactic(m, p), - and_then(mk_qe_tactic(m), mk_smt_tactic()))); + cond(mk_has_quantifier_probe(), + or_else(mk_qsat_tactic(m, p), + and_then(mk_qe_tactic(m), mk_smt_tactic())), + mk_smt_tactic())); #endif st->updt_params(p); return st;