diff options
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/proof.cpp | 4 | ||||
| -rw-r--r-- | src/expr/proof_checker.cpp | 2 | ||||
| -rw-r--r-- | src/expr/proof_node.cpp | 55 | ||||
| -rw-r--r-- | src/expr/proof_node.h | 27 | ||||
| -rw-r--r-- | src/expr/proof_rule.cpp | 2 | ||||
| -rw-r--r-- | src/expr/proof_rule.h | 27 |
6 files changed, 93 insertions, 24 deletions
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 6d2d70543..eff222b92 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -49,7 +49,7 @@ bool CDProof::addStep(Node expected, if (it != d_nodes.end()) { if (!forceOverwrite - && ((*it).second->getId() != PfRule::ASSUME || id == PfRule::ASSUME)) + && ((*it).second->getRule() != PfRule::ASSUME || id == PfRule::ASSUME)) { // we do not overwrite if forceOverwrite is false and the previously // provided step was not an assumption, or if the currently provided step @@ -144,7 +144,7 @@ bool CDProof::addProof(ProofNode* pn, bool forceOverwrite) } // can ensure children at this point bool res = addStep(curFact, - cur->getId(), + cur->getRule(), pexp, cur->getArguments(), true, diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp index f4c275c47..95e43620b 100644 --- a/src/expr/proof_checker.cpp +++ b/src/expr/proof_checker.cpp @@ -18,7 +18,7 @@ namespace CVC4 { Node ProofChecker::check(ProofNode* pn, Node expected) { - return check(pn->getId(), pn->getChildren(), pn->getArguments(), expected); + return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected); } Node ProofChecker::check( diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp index 94c175025..b5e391049 100644 --- a/src/expr/proof_node.cpp +++ b/src/expr/proof_node.cpp @@ -23,7 +23,7 @@ ProofNode::ProofNode(PfRule id, setValue(id, children, args); } -PfRule ProofNode::getId() const { return d_id; } +PfRule ProofNode::getRule() const { return d_rule; } const std::vector<std::shared_ptr<ProofNode>>& ProofNode::getChildren() const { @@ -34,11 +34,14 @@ const std::vector<Node>& ProofNode::getArguments() const { return d_args; } Node ProofNode::getResult() const { return d_proven; } -void ProofNode::getAssumptions(std::vector<Node>& assump) const +void ProofNode::getFreeAssumptions(std::vector<Node>& assump) const { - std::unordered_set<const ProofNode*> visited; - std::unordered_set<const ProofNode*>::iterator it; + // visited set false after preorder traversal, true after postorder traversal + std::unordered_map<const ProofNode*, bool> visited; + std::unordered_map<const ProofNode*, bool>::iterator it; std::vector<const ProofNode*> visit; + // the current set of formulas bound by SCOPE + std::unordered_set<Node, NodeHashFunction> currentScope; const ProofNode* cur; visit.push_back(this); do @@ -48,35 +51,69 @@ void ProofNode::getAssumptions(std::vector<Node>& assump) const it = visited.find(cur); if (it == visited.end()) { - visited.insert(cur); - if (cur->getId() == PfRule::ASSUME) + visited[cur] = true; + PfRule id = cur->getRule(); + if (id == PfRule::ASSUME) { - assump.push_back(cur->d_proven); + Assert(cur->d_args.size() == 1); + Node f = cur->d_args[0]; + if (currentScope.find(f) == currentScope.end()) + { + assump.push_back(f); + } } else { + if (id == PfRule::SCOPE) + { + // mark that its arguments are bound in the current scope + for (const Node& a : cur->d_args) + { + // should not have assumption shadowing + Assert(currentScope.find(a) != currentScope.end()); + currentScope.insert(a); + } + // will need to unbind the variables below + visited[cur] = false; + } for (const std::shared_ptr<ProofNode>& cp : cur->d_children) { visit.push_back(cp.get()); } } } + else if (!it->second) + { + Assert(cur->getRule() == PfRule::SCOPE); + // unbind its assumptions + for (const Node& a : cur->d_args) + { + currentScope.erase(a); + } + } } while (!visit.empty()); } +bool ProofNode::isClosed() const +{ + std::vector<Node> assumps; + getFreeAssumptions(assumps); + return assumps.empty(); +} + void ProofNode::setValue( PfRule id, const std::vector<std::shared_ptr<ProofNode>>& children, const std::vector<Node>& args) { - d_id = id; + d_rule = id; d_children = children; d_args = args; } void ProofNode::printDebug(std::ostream& os) const { - os << "(" << d_id; + os << "(" << d_rule; for (const std::shared_ptr<ProofNode>& c : d_children) { os << " "; diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index 9a460c59b..c3f1719e7 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -55,22 +55,29 @@ class ProofNode const std::vector<std::shared_ptr<ProofNode>>& children, const std::vector<Node>& args); ~ProofNode() {} - /** get the id of this proof node */ - PfRule getId() const; + /** get the rule of this proof node */ + PfRule getRule() const; /** Get children */ const std::vector<std::shared_ptr<ProofNode>>& getChildren() const; /** Get arguments */ const std::vector<Node>& getArguments() const; /** get what this node proves, or the null node if this is an invalid proof */ Node getResult() const; - /** Get assumptions + /** + * 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 adds to the vector assump all formulas that are "assumptions" of the - * proof whose root is this ProofNode. An assumption is a formula that is an - * argument (in d_args) of a ProofNode whose kind is ASSUME. This traverses - * the structure of the dag represented by this ProofNode. + * 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). */ - void getAssumptions(std::vector<Node>& assump) const; + bool isClosed() const; /** Print debug on output strem os */ void printDebug(std::ostream& os) const; @@ -82,8 +89,8 @@ class ProofNode void setValue(PfRule id, const std::vector<std::shared_ptr<ProofNode>>& children, const std::vector<Node>& args); - /** The proof step */ - PfRule d_id; + /** The proof rule */ + PfRule d_rule; /** The children of this proof node */ std::vector<std::shared_ptr<ProofNode>> d_children; /** arguments of this node */ diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 2c10e09e6..e555f5691 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -24,6 +24,8 @@ const char* toString(PfRule id) { //================================================= Core rules case PfRule::ASSUME: return "ASSUME"; + case PfRule::SCOPE: return "SCOPE"; + //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 16f4ca971..0d03bb347 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -35,19 +35,42 @@ namespace CVC4 { * The following PfRule values include core rules and those categorized by * theory, including the theory of equality. * - * The "core rules" include ASSUME, which represents an open leaf in a proof. + * The "core rules" include two distinguished rules which have special status: + * (1) ASSUME, which represents an open leaf in a proof. + * (2) SCOPE, which closes the scope of assumptions. * The core rules additionally correspond to generic operations that are done * internally on nodes, e.g. calling Rewriter::rewrite. */ enum class PfRule : uint32_t { //================================================= Core rules + //======================== Assume and Scope // ======== Assumption (a leaf) // Children: none // Arguments: (F) // -------------- - // Conclusion F + // Conclusion: F + // + // This rule has special status, in that an application of assume is an + // open leaf in a proof that is not (yet) justified. An assume leaf is + // analogous to a free variable in a term, where we say "F is a free + // assumption in proof P" if it contains an application of F that is not + // bound by SCOPE (see below). ASSUME, + // ======== Scope (a binder for assumptions) + // Children: (P:F) + // Arguments: (F1, ..., Fn) + // -------------- + // Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false + // + // This rule has a dual purpose with ASSUME. It is a way to close + // assumptions in a proof. We require that F1 ... Fn are free assumptions in + // P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they + // are bound by this application. For example, the proof node: + // (SCOPE (ASSUME F) :args F) + // has the conclusion (=> F F) and has no free assumptions. More generally, a + // proof with no free assumptions always concludes a valid formula. + SCOPE, //================================================= Unknown rule UNKNOWN, |