diff options
Diffstat (limited to 'src/expr/proof_node.h')
-rw-r--r-- | src/expr/proof_node.h | 42 |
1 files changed, 30 insertions, 12 deletions
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index c3f1719e7..41575200f 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -45,6 +45,33 @@ class ProofNodeManager; * ProofNode objects in trusted ways that ensure that the node maintains * the invariant above. Furthermore, notice that this class is not responsible * for setting d_proven; this is done externally by a ProofNodeManager class. + * + * Notice that all fields of ProofNode are stored in ***Skolem form***. Their + * correctness is checked in ***witness form*** (for details on this + * terminology, see expr/skolem_manager.h). As a simple example, say a + * theory solver has a term t, and wants to introduce a unit lemma (= k t) + * where k is a fresh Skolem variable. It creates this variable via: + * k = SkolemManager::mkPurifySkolem(t,"k"); + * A checked ProofNode for the fact (= k t) then may have fields: + * d_rule := MACRO_SR_PRED_INTRO, + * d_children := {}, + * d_args := {(= k t)} + * d_proven := (= k t). + * Its justification via the rule MACRO_SR_PRED_INTRO (see documentation + * in theory/builtin/proof_kinds) is in terms of the witness form of the + * argument: + * (= (witness ((z T)) (= z t)) t) + * which, by that rule's side condition, is such that: + * Rewriter::rewrite((= (witness ((z T)) (= z t)) t)) = true. + * Notice that the correctness of the rule is justified here by rewriting + * the witness form of (= k t). The conversion to/from witness form is + * managed by ProofRuleChecker::check. + * + * An external proof checker is expected to formalize the ProofNode only in + * terms of *witness* forms. + * + * However, the rest of CVC4 sees only the *Skolem* form of arguments and + * conclusions in ProofNode, since this is what is used throughout CVC4. */ class ProofNode { @@ -64,22 +91,13 @@ class ProofNode /** get what this node proves, or the null node if this is an invalid proof */ Node getResult() const; /** - * This adds to the vector assump all formulas that are "free assumptions" of - * the proof whose root is this ProofNode. A free assumption is a formula F - * that is an argument (in d_args) of a ProofNode whose kind is ASSUME, and - * that proof node is not beneath an application of SCOPE containing F as an - * argument. - * - * This traverses the structure of the dag represented by this ProofNode. - * Its implementation is analogous to expr::getFreeVariables. - */ - void getFreeAssumptions(std::vector<Node>& assump) const; - /** * Returns true if this is a closed proof (i.e. it has no free assumptions). */ - bool isClosed() const; + bool isClosed(); /** Print debug on output strem os */ void printDebug(std::ostream& os) const; + /** Clone, create a deep copy of this */ + std::shared_ptr<ProofNode> clone() const; private: /** |