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

fix slice bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-20 21:51:41 -08:00
parent 93dfafb6d4
commit 21eca20b9e
4 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_cmds.cpp
View file

@ -315,7 +315,7 @@ private:
if (m_params.get_bool(":print-certificate", false)) { if (m_params.get_bool(":print-certificate", false)) {
datalog::context& dlctx = m_dl_ctx->dlctx(); datalog::context& dlctx = m_dl_ctx->dlctx();
if (!dlctx.display_certificate(ctx.regular_stream())) { if (!dlctx.display_certificate(ctx.regular_stream())) {
throw cmd_exception("certificates are not supported for selected DL_ENGINE"); throw cmd_exception("certificates are not supported for the selected engine");
} }
ctx.regular_stream() << "\n"; ctx.regular_stream() << "\n";
} }

2
src/muz_qe/dl_context.cpp
View file

@ -1523,7 +1523,7 @@ namespace datalog {
switch(get_engine()) { switch(get_engine()) {
case DATALOG_ENGINE: case DATALOG_ENGINE:
return false; return false;
case PDR_ENGINE: case QPDR_ENGINE:
ensure_pdr(); ensure_pdr();
m_pdr->display_certificate(out); m_pdr->display_certificate(out);
return true; return true;

1
src/muz_qe/dl_mk_rule_inliner.cpp
View file

@ -194,6 +194,7 @@ namespace datalog {
} }
} }
// TBD: replace by r.has_quantifiers() and test
bool mk_rule_inliner::has_quantifier(rule const& r) const { bool mk_rule_inliner::has_quantifier(rule const& r) const {
unsigned utsz = r.get_uninterpreted_tail_size(); unsigned utsz = r.get_uninterpreted_tail_size();
for (unsigned i = utsz; i < r.get_tail_size(); ++i) { for (unsigned i = utsz; i < r.get_tail_size(); ++i) {

5
src/muz_qe/dl_mk_slice.cpp
View file

@ -818,6 +818,11 @@ namespace datalog {
} }
rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc, proof_converter_ref& pc) {
for (unsigned i = 0; i < src.get_num_rules(); ++i) {
if (src.get_rule(i)->has_quantifiers()) {
return 0;
}
}
ref<slice_proof_converter> spc; ref<slice_proof_converter> spc;
ref<slice_model_converter> smc; ref<slice_model_converter> smc;
if (pc) { if (pc) {