mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-09-06 21:49:14 -07:00
commit 0f9160a738
2 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -52,10 +52,14 @@ namespace datalog {
ptr_vector<func_decl> todo; ptr_vector<func_decl> todo;
rule_set::decl2rules body2rules; rule_set::decl2rules body2rules;
// initialization for reachability // initialization for reachability
rel_context_base* rc = m_context.get_rel_context();
for (rule_set::iterator it = source.begin(); it != source.end(); ++it) { for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
rule * r = *it; rule * r = *it;
all.insert(r->get_decl()); all.insert(r->get_decl());
if (r->get_uninterpreted_tail_size() == 0) { bool non_empty =
(rc && !rc->is_empty_relation(r->get_decl())) ||
r->get_uninterpreted_tail_size() == 0;
if (non_empty) {
if (!reached.contains(r->get_decl())) { if (!reached.contains(r->get_decl())) {
reached.insert(r->get_decl()); reached.insert(r->get_decl());
todo.insert(r->get_decl()); todo.insert(r->get_decl());

6
src/qe/qe.cpp
View file

@ -482,7 +482,7 @@ namespace qe {
} }
void nnf_iff(app* a, bool p) { void nnf_iff(app* a, bool p) {
SASSERT(m.is_iff(a) || m.is_xor(a)); SASSERT(m.is_iff(a) || m.is_xor(a) || m.is_eq(a));
expr* a0 = a->get_arg(0); expr* a0 = a->get_arg(0);
expr* a1 = a->get_arg(1); expr* a1 = a->get_arg(1);
@ -616,7 +616,7 @@ namespace qe {
else if (m.is_ite(a)) { else if (m.is_ite(a)) {
nnf_ite(a, p); nnf_ite(a, p);
} }
else if (m.is_iff(a)) { else if (m.is_iff(a) || (m.is_eq(a) && m.is_bool(a->get_arg(0)))) {
nnf_iff(a, p); nnf_iff(a, p);
} }
else if (m.is_xor(a)) { else if (m.is_xor(a)) {
@ -1926,6 +1926,7 @@ namespace qe {
plugin(x).get_num_branches(contains(x), fml, num_branches)) { plugin(x).get_num_branches(contains(x), fml, num_branches)) {
return true; return true;
} }
TRACE("qe", tout << "setting variable " << mk_pp(x, m) << " free\n";);
m_free_vars.push_back(x); m_free_vars.push_back(x);
m_current->del_var(x); m_current->del_var(x);
} }
@ -2493,6 +2494,7 @@ namespace qe {
// callback to replace variable at index 'idx' with definition 'def' and updated formula 'fml' // callback to replace variable at index 'idx' with definition 'def' and updated formula 'fml'
virtual void elim_var(unsigned idx, expr* fml, expr* def) { virtual void elim_var(unsigned idx, expr* fml, expr* def) {
TRACE("qe", tout << mk_pp(m_vars->get(idx), m) << " " << mk_pp(fml, m) << "\n";);
*m_fml = fml; *m_fml = fml;
m_vars->set(idx, m_vars->get(m_vars->size()-1)); m_vars->set(idx, m_vars->get(m_vars->size()-1));
m_vars->pop_back(); m_vars->pop_back();