Doc

2 files changed, 40 insertions, 6 deletions

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index f1ec78aab..637896a20 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -63,7 +63,8 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
 std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
     std::shared_ptr<ProofNode> pf,
     std::vector<Node>& assumps,
-    bool ensureClosed)
+    bool ensureClosed,
+    bool doMinimize)
 {
   std::vector<std::shared_ptr<ProofNode>> pfChildren;
   pfChildren.push_back(pf);
@@ -152,8 +153,11 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
       }
     }
   }
-  assumps.clear();
-  assumps.insert(assumps.end(), acu.begin(), acu.end());
+  if (doMinimize)
+  {
+    assumps.clear();
+    assumps.insert(assumps.end(), acu.begin(), acu.end());
+  }
   return mkNode(PfRule::SCOPE, pfChildren, assumps);
 }
 
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 527f2562d..6562d3e02 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -78,12 +78,42 @@ class ProofNodeManager
                                     std::shared_ptr<ProofNode> child1,
                                     const std::vector<Node>& args,
                                     Node expected = Node::null());
-  /** Make assume */
+  /**
+   * Make the proof node corresponding to the assumption of fact.
+   * 
+   * @param fact The fact to assume.
+   * @return The assume proof of fact.
+   */
   std::shared_ptr<ProofNode> mkAssume(Node fact);
-  /** Make scope */
+  /** 
+   * Make scope having body pf and arguments (assumptions-to-close) assump.
+   * If ensureClosed is true, then this method throws an assertion failure if
+   * the returned proof is not closed. This is the case if a free assumption
+   * of pf is missing from the vector assumps. 
+   * 
+   * For conveinence, the proof pf may be modified to ensure that the overall
+   * result is closed. For instance, given input:
+   *   pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) )
+   *   assumps = { y=x, y=z }
+   * This method will modify pf to be:
+   *   pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) )
+   * so that y=x matches the free assumption. The returned proof is:
+   *   SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z })
+   * 
+   * Additionally, if both ensureClosed and doMinimize are true, assumps is
+   * updated to contain exactly the free asumptions of pf. The minimized
+   * vector is passed as arguments to the SCOPE.
+   * 
+   * @param pf The body of the proof,
+   * @param assumps The assumptions-to-close of the scope,
+   * @param ensureClosed Whether to ensure that the proof is closed,
+   * @param doMinimize Whether to minimize assumptions.
+   * @return The scoped proof.
+   */
   std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf,
                                      std::vector<Node>& assumps,
-                                     bool ensureClosed = true);
+                                     bool ensureClosed = true,
+                                     bool doMinimize = false);
 
   /**
    * This method updates pn to be a proof of the form <id>( children, args ),