This rule is dual to ASSUME. It is a way of closing free assumptions to conclude an implication.
It also changes getId -> getRule.
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
}
// can ensure children at this point
bool res = addStep(curFact,
- cur->getId(),
+ cur->getRule(),
pexp,
cur->getArguments(),
true,
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(
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
{
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
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 << " ";
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;
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 */
{
//================================================= Core rules
case PfRule::ASSUME: return "ASSUME";
+ case PfRule::SCOPE: return "SCOPE";
+
//================================================= Unknown rule
case PfRule::UNKNOWN: return "UNKNOWN";
default: return "?";
* 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,
projects / cvc5.git / commitdiff