Final cleanup of hypothesis_reducer

src/muz/spacer/spacer_proof_utils.cpp

@@ -173,6 +173,24 @@ proof_ref theory_axiom_reducer::reduce(proof* pr) {
     return proof_ref(res, m);
 }
 
+/* ------------------------------------------------------------------------- */
+/* hypothesis_reducer */
+/* ------------------------------------------------------------------------- */
+
+proof_ref hypothesis_reducer::reduce(proof* pr) {
+    compute_hypsets(pr);
+    collect_units(pr);
+
+    proof_ref res(reduce_core(pr), m);
+    SASSERT(res);
+    reset();
+
+    DEBUG_CODE(proof_checker pc(m);
+               expr_ref_vector side(m);
+               SASSERT(pc.check(res, side)););
+    return res;
+}
+
 void hypothesis_reducer::reset() {
     m_parent_hyps.reset();
     m_active_hyps.reset();
@@ -198,7 +216,7 @@ void hypothesis_reducer::compute_hypsets(proof *pr) {
             continue;
         }
 
-        bool dirty = false;
+        unsigned todo_sz = todo.size();
         for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
             SASSERT(m.is_proof(p->get_arg(i)));
             proof *parent = to_app(p->get_arg(i));
@@ -206,10 +224,9 @@ void hypothesis_reducer::compute_hypsets(proof *pr) {
             if (!m_active_hyps.contains(parent)) {
                 SASSERT(!m_parent_hyps.contains(parent));
                 todo.push_back(parent);
-                dirty = true;
             }
         }
-        if (dirty) continue;
+        if (todo.size() > todo_sz) continue;
 
         todo.pop_back();
 
@@ -262,21 +279,10 @@ void hypothesis_reducer::collect_units(proof* pr) {
     }
 }
 
-proof_ref hypothesis_reducer::reduce(proof* pr) {
-    compute_hypsets(pr);
-    collect_units(pr);
 
-    proof_ref res(compute_transformed_proof(pr), m);
+proof* hypothesis_reducer::reduce_core(proof* pf) {
-    SASSERT(res);
+    SASSERT(m.is_false(m.get_fact(pf)));
-    reset();
 
-    DEBUG_CODE(proof_checker pc(m);
-               expr_ref_vector side(m);
-               SASSERT(pc.check(res, side)););
-    return res;
-}
-
-proof* hypothesis_reducer::compute_transformed_proof(proof* pf) {
     proof *res = NULL;
 
     ptr_vector<proof> todo;
@@ -284,7 +290,7 @@ proof* hypothesis_reducer::compute_transformed_proof(proof* pf) {
     ptr_buffer<proof> args;
     bool dirty = false;
 
-    while (!todo.empty()) {
+    while (true) {
         proof *p, *tmp, *pp;
         unsigned todo_sz;
 
@@ -311,58 +317,59 @@ proof* hypothesis_reducer::compute_transformed_proof(proof* pf) {
 
         todo.pop_back();
 
-        // transform the proof
+        // transform the current proof node
 
-        // INV: whenever p is visited, active_hyps and parent_hyps
-        // have already been computed for everything in args.
         if (m.is_hypothesis(p)) {
-            // hyp: replace by a corresponding unit
+            // if possible, replace a hypothesis by a unit derivation
             if (m_units.find(m.get_fact(p), tmp)) {
-                // look up the proof of the unit:
+                // use already transformed proof of the unit if it is available
-                // if there is a transformed proof use that one
-                // otherwise use the original proof
                 proof* proof_of_unit;
                 if (!m_cache.find(tmp, proof_of_unit)) {
                     proof_of_unit = tmp;
                 }
 
-                // compute hypsets (have not been computed in general,
+                // make sure hypsets for the unit are computed
-                // since the unit can be anywhere in the proof)
+                // AG: is this needed?
                 compute_hypsets(proof_of_unit);
+                SASSERT(m_parent_hyps.contains(proof_of_unit));
 
                 // if the transformation doesn't create a cycle, perform it
-                SASSERT(m_parent_hyps.contains(proof_of_unit));
                 expr_set* parent_hyps = m_parent_hyps.find(proof_of_unit);
-                if (!parent_hyps->contains(p))
+                if (!parent_hyps->contains(p)) {
-                    // hypsets have already been computed for proof_of_unit
                     res = proof_of_unit;
-                // otherwise don't transform the proof and just use
+                }
-                // the hypothesis
+                else {
-                else
+                    // -- failed to transform the proof, perhaps bad
-                    // hypsets have already been computed for p
+                    // -- choice of the proof of unit
                     res = p;
+                }
             }
-            else
+            else {
-                // hypsets have already been computed for p
+                // -- no unit found to replace the hypothesis
                 res = p;
+            }
         }
-        else if (!dirty)
+
-            res = p;
+        else if (!dirty) {res = p;}
+
         else if (m.is_lemma(p)) {
-            //lemma: reduce the premise; remove reduced consequences
+            // lemma: reduce the premise; remove reduced consequences
-            //from conclusion
+            // from conclusion
             SASSERT(args.size() == 1);
             res = mk_lemma_core(args[0], m.get_fact(p));
+            // -- re-compute hypsets
             compute_hypsets(res);
         }
         else if (m.is_unit_resolution(p)) {
             // unit: reduce untis; reduce the first premise; rebuild
             // unit resolution
             res = mk_unit_resolution_core(args);
+            // -- re-compute hypsets
             compute_hypsets(res);
         }
         else {
             res = mk_proof_core(p, args);
+            // -- re-compute hypsets
             compute_hypsets(res);
         }
 

src/muz/spacer/spacer_proof_utils.h

@@ -76,19 +76,24 @@ private:
     // maps a unit literal to its derivation
     obj_map<expr, proof*> m_units;
 
-    // maps a proof to the set of proofs of active hypotheses
+    // maps a proof node to the set of its  active (i.e., in scope) hypotheses
     obj_map<proof, proof_set*> m_active_hyps;
-    // maps a proof to the hypothesis-fact that are transitive
+
-    // parents of that proof.  Used for cycle detection and avoidance.
+    // maps a proof node to the set of all hypothesis-facts (active or
+    // not) that can reach it. Used for cycle detection and avoidance
+    // during  proof transformation
     obj_map<proof, expr_set*> m_parent_hyps;
 
     void reset();
 
-    // compute active_hyps and parent_hyps for pr
+    // compute active_hyps and parent_hyps for a given proof node and
+    // all its ancestors
     void compute_hypsets(proof* pr);
     // compute m_units
     void collect_units(proof* pr);
-    proof* compute_transformed_proof(proof* pf);
+
+    // -- rewrite proof to reduce number of hypotheses used
+    proof* reduce_core(proof* pf);
 
     proof* mk_lemma_core(proof *pf, expr *fact);
     proof* mk_unit_resolution_core(ptr_buffer<proof>& args);