From 0a3f95bdaaedb22d7357debd697bbecd9cd44ad2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 14 Dec 2012 16:54:59 -0800 Subject: [PATCH] quantifiers Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_bmc_engine.cpp | 2 +- src/muz_qe/dl_mk_extract_quantifiers2.cpp | 13 +++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index b5ffa808a..a01d4c322 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -459,7 +459,7 @@ namespace datalog { void setup() { b.m_fparams.m_model = true; b.m_fparams.m_model_compact = true; - b.m_fparams.m_mbqi = true; + // b.m_fparams.m_mbqi = true; b.m_fparams.m_relevancy_lvl = 2; } diff --git a/src/muz_qe/dl_mk_extract_quantifiers2.cpp b/src/muz_qe/dl_mk_extract_quantifiers2.cpp index 97976a6be..33b33f0aa 100644 --- a/src/muz_qe/dl_mk_extract_quantifiers2.cpp +++ b/src/muz_qe/dl_mk_extract_quantifiers2.cpp @@ -307,17 +307,18 @@ namespace datalog { bmc bmc(m_ctx); expr_ref_vector fmls(m); - bmc.compile(source, fmls, 0); // TBD: use cancel_eh to terminate without base-case. - bmc.compile(source, fmls, 1); - bmc.compile(source, fmls, 2); -// bmc.compile(source, fmls, 3); - expr_ref query = bmc.compile_query(m_query_pred, 2); + unsigned depth = 2; + // TBD: use cancel_eh to terminate without base-case. + for (unsigned i = 0; i <= depth; ++i) { + bmc.compile(source, fmls, i); + } + expr_ref query = bmc.compile_query(m_query_pred, depth); fmls.push_back(query); smt_params fparams; fparams.m_relevancy_lvl = 0; fparams.m_model = true; fparams.m_model_compact = true; - fparams.m_mbqi = true; + fparams.m_mbqi = false; smt::kernel solver(m, fparams); TRACE("dl", for (unsigned i = 0; i < fmls.size(); ++i) {