diff options
Diffstat (limited to 'src/expr/proof_node_manager.h')
| -rw-r--r-- | src/expr/proof_node_manager.h | 36 |
1 files changed, 33 insertions, 3 deletions
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 ), |