mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

horn clause bit blasting: propagate output predicates for predicates without rules (most likely an UNSAT prog)

Browse source 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-05-15 13:17:00 -07:00
parent e6c8149873
commit 5efdc58194
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -279,6 +279,13 @@ namespace datalog {
result->add_rule(r);
}
}
// copy output predicates without any rule (bit-blasting not really needed)
const func_decl_set& decls = source.get_output_predicates();
for (func_decl_set::iterator I = decls.begin(), E = decls.end(); I != E; ++I) {
if (!result->contains(*I))
result->set_output_predicate(*I);
}
if (m_context.get_model_converter()) {
filter_model_converter* fmc = alloc(filter_model_converter, m);