From b269e6b35bba4fc09d3177024cde8424a7c18073 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 15:11:46 -0400 Subject: [PATCH] comments on proof_utils --- src/muz/base/proof_utils.cpp | 52 ++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/src/muz/base/proof_utils.cpp b/src/muz/base/proof_utils.cpp index bbf9da0a4..3b2d50fdc 100644 --- a/src/muz/base/proof_utils.cpp +++ b/src/muz/base/proof_utils.cpp @@ -12,12 +12,19 @@ Copyright (c) 2015 Microsoft Corporation class reduce_hypotheses { typedef obj_hashtable expr_set; ast_manager& m; + // reference for any expression created by the tranformation expr_ref_vector m_refs; + // currently computed result obj_map m_cache; + // map conclusions to closed proofs that derive them obj_map m_units; + // currently active units ptr_vector m_units_trail; + // size of m_units_trail at the last push unsigned_vector m_limits; + // map from proofs to active hypotheses obj_map m_hypmap; + // refernce train for hypotheses sets ptr_vector m_hyprefs; ptr_vector m_literals; @@ -151,19 +158,33 @@ public: p = result; return; } + //SASSERT (p.get () == result); switch(p->get_decl_kind()) { case PR_HYPOTHESIS: + // replace result by m_units[m.get_fact (p)] if defined + // AG: This is the main step. Replace a hypothesis by a derivation of its consequence if (!m_units.find(m.get_fact(p), result)) { + // restore ther result back to p result = p.get(); } + // compute hypothesis of the result + // not clear what 'result' is at this point. + // probably the proof at the top of the call + // XXX not clear why this is re-computed each time + // XXX moreover, m_units are guaranteed to be closed! + // XXX so no hypotheses are needed for them add_hypotheses(result); break; case PR_LEMMA: { SASSERT(m.get_num_parents(p) == 1); tmp = m.get_parent(p, 0); + // eliminate hypothesis recursively in the proof of the lemma elim(tmp); expr_set* hyps = m_hypmap.find(tmp); expr_set* new_hyps = 0; + // XXX if the proof is correct, the hypotheses of the tmp + // XXX should be exactly those of the consequence of the lemma + // XXX but if this code actually eliminates hypotheses, the set might be a subset if (hyps) { new_hyps = alloc(expr_set, *hyps); } @@ -178,13 +199,19 @@ public: get_literals(fact); } + // go over all the literals in the consequence of the lemma for (unsigned i = 0; i < m_literals.size(); ++i) { expr* e = m_literals[i]; + // if the literal is not in hypothesis, skip it if (!in_hypotheses(e, hyps)) { m_literals[i] = m_literals.back(); m_literals.pop_back(); --i; } + // if the literal is in hypothesis remove it because + // it is not in hypothesis set of the lemma + // XXX but we assume that lemmas have empty hypothesis set. + // XXX eventually every element of new_hyps must be removed! else { SASSERT(new_hyps); expr_ref not_e = complement_lit(e); @@ -192,10 +219,13 @@ public: new_hyps->remove(not_e); } } + // killed all hypotheses, so can stop at the lemma since + // we have a closed pf of false if (m_literals.empty()) { result = tmp; } else { + // create a new lemma, but might be re-creating existing one expr_ref clause(m); if (m_literals.size() == 1) { clause = m_literals[0]; @@ -212,6 +242,7 @@ public: new_hyps = 0; } m_hypmap.insert(result, new_hyps); + // might push 0 into m_hyprefs. No reason for that m_hyprefs.push_back(new_hyps); TRACE("proof_utils", tout << "New lemma: " << mk_pp(m.get_fact(p), m) @@ -229,19 +260,27 @@ public: } case PR_UNIT_RESOLUTION: { proof_ref_vector parents(m); + // get the clause being resolved with parents.push_back(m.get_parent(p, 0)); + // save state push(); bool found_false = false; + // for every derivation of a unit literal for (unsigned i = 1; i < m.get_num_parents(p); ++i) { + // see if it derives false tmp = m.get_parent(p, i); elim(tmp); if (m.is_false(m.get_fact(tmp))) { + // if derived false, the whole pf is false and we can bail out result = tmp; found_false = true; break; } + // -- otherwise, the fact has not changed. nothing to simplify SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i))); parents.push_back(tmp); + // remember that we have this derivation while we have not poped the trail + // but only if the proof is closed (i.e., a real unit) if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) { m_units.insert(m.get_fact(tmp), tmp); m_units_trail.push_back(m.get_fact(tmp)); @@ -251,10 +290,15 @@ public: pop(); break; } + // look at the clause being resolved with tmp = m.get_parent(p, 0); + // remember its fact expr* old_clause = m.get_fact(tmp); + // attempt to reduce its fact elim(tmp); + // update parents parents[0] = tmp; + // if the new fact is false, bail out expr* clause = m.get_fact(tmp); if (m.is_false(clause)) { m_refs.push_back(tmp); @@ -264,8 +308,10 @@ public: } // // case where clause is a literal in the old clause. + // i.e., reduce multi-literal clause to a unit // if (is_literal_in_clause(clause, old_clause)) { + // if the resulting literal was resolved, get a pf of false and bail out bool found = false; for (unsigned i = 1; !found && i < parents.size(); ++i) { if (m.is_complement(clause, m.get_fact(parents[i].get()))) { @@ -277,6 +323,7 @@ public: found = true; } } + // else if the resulting literal is not resolved, it is the new consequence if (!found) { result = parents[0].get(); } @@ -508,6 +555,11 @@ static void permute_unit_resolution(expr_ref_vector& refs, obj_map SASSERT(params[0].is_symbol()); family_id tid = m.mk_family_id(params[0].get_symbol()); SASSERT(tid != null_family_id); + // AG: This can break a theory lemma. In particular, for Farkas lemmas the coefficients + // AG: for the literals propagated from the unit resolution are missing. + // AG: Why is this a good thing to do? + // AG: This can lead to merging of the units with other terms in interpolation, + // AG: but without farkas coefficients this does not make sense prNew = m.mk_th_lemma(tid, m.get_fact(pr), premises.size(), premises.c_ptr(), num_params-1, params+1); }