mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 07:33:24 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2013-05-27 17:49:29 -07:00
commit fbbbfad564
4 changed files with 16 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/aig_exporter.cpp
View file

@ -265,6 +265,8 @@ namespace datalog {
case AST_VAR: case AST_VAR:
return get_var(e); return get_var(e);
default:
UNREACHABLE();
} }
UNREACHABLE(); UNREACHABLE();

3
src/muz_qe/clp_context.cpp
View file

@ -66,8 +66,9 @@ namespace datalog {
m_ctx.ensure_opened(); m_ctx.ensure_opened();
m_solver.reset(); m_solver.reset();
m_goals.reset(); m_goals.reset();
func_decl *head_decl = rm.mk_query(query, m_ctx.get_rules()); rm.mk_query(query, m_ctx.get_rules());
m_ctx.apply_default_transformation(); m_ctx.apply_default_transformation();
func_decl *head_decl = m_ctx.get_rules().get_output_predicate();
expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m); expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m);
ground(head); ground(head);

6
src/muz_qe/dl_mk_slice.cpp
View file

@ -710,6 +710,7 @@ namespace datalog {
void mk_slice::declare_predicates(rule_set const& src, rule_set& dst) { void mk_slice::declare_predicates(rule_set const& src, rule_set& dst) {
obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin(), end = m_sliceable.end(); obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin(), end = m_sliceable.end();
ptr_vector<sort> domain; ptr_vector<sort> domain;
bool has_output = false;
func_decl* f; func_decl* f;
for (; it != end; ++it) { for (; it != end; ++it) {
domain.reset(); domain.reset();
@ -731,8 +732,13 @@ namespace datalog {
} }
else if (src.is_output_predicate(p)) { else if (src.is_output_predicate(p)) {
dst.set_output_predicate(p); dst.set_output_predicate(p);
has_output = true;
} }
} }
// disable slicing if the output predicates don't occur in rules.
if (!has_output) {
m_predicates.reset();
}
} }
bool mk_slice::rule_updated(rule const& r) { bool mk_slice::rule_updated(rule const& r) {

6
src/muz_qe/pdr_dl_interface.cpp
View file

@ -133,6 +133,12 @@ lbool dl_interface::query(expr * query) {
--num_unfolds; --num_unfolds;
} }
} }
if (m_ctx.get_rules().get_output_predicates().empty()) {
m_context->set_unsat();
return l_false;
}
query_pred = m_ctx.get_rules().get_output_predicate(); query_pred = m_ctx.get_rules().get_output_predicate();
IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););