mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

quantifiers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-14 16:54:59 -08:00
parent 635aabf2d5
commit 0a3f95bdaa
2 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_bmc_engine.cpp
View file

@ -459,7 +459,7 @@ namespace datalog {
void setup() { void setup() {
b.m_fparams.m_model = true; b.m_fparams.m_model = true;
b.m_fparams.m_model_compact = 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; b.m_fparams.m_relevancy_lvl = 2;
} }

13
src/muz_qe/dl_mk_extract_quantifiers2.cpp
View file

@ -307,17 +307,18 @@ namespace datalog {
bmc bmc(m_ctx); bmc bmc(m_ctx);
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
bmc.compile(source, fmls, 0); // TBD: use cancel_eh to terminate without base-case. unsigned depth = 2;
bmc.compile(source, fmls, 1); // TBD: use cancel_eh to terminate without base-case.
bmc.compile(source, fmls, 2); for (unsigned i = 0; i <= depth; ++i) {
// bmc.compile(source, fmls, 3); bmc.compile(source, fmls, i);
expr_ref query = bmc.compile_query(m_query_pred, 2); }
expr_ref query = bmc.compile_query(m_query_pred, depth);
fmls.push_back(query); fmls.push_back(query);
smt_params fparams; smt_params fparams;
fparams.m_relevancy_lvl = 0; fparams.m_relevancy_lvl = 0;
fparams.m_model = true; fparams.m_model = true;
fparams.m_model_compact = true; fparams.m_model_compact = true;
fparams.m_mbqi = true; fparams.m_mbqi = false;
smt::kernel solver(m, fparams); smt::kernel solver(m, fparams);
TRACE("dl", TRACE("dl",
for (unsigned i = 0; i < fmls.size(); ++i) { for (unsigned i = 0; i < fmls.size(); ++i) {