diff options
Diffstat (limited to 'src/proof/trust_node.cpp')
-rw-r--r-- | src/proof/trust_node.cpp | 150 |
1 files changed, 150 insertions, 0 deletions
diff --git a/src/proof/trust_node.cpp b/src/proof/trust_node.cpp new file mode 100644 index 000000000..d99e6de51 --- /dev/null +++ b/src/proof/trust_node.cpp @@ -0,0 +1,150 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of the trust node utility. + */ + +#include "proof/trust_node.h" + +#include "proof/proof_ensure_closed.h" +#include "proof/proof_generator.h" + +namespace cvc5 { +namespace theory { + +const char* toString(TrustNodeKind tnk) +{ + switch (tnk) + { + case TrustNodeKind::CONFLICT: return "CONFLICT"; + case TrustNodeKind::LEMMA: return "LEMMA"; + case TrustNodeKind::PROP_EXP: return "PROP_EXP"; + case TrustNodeKind::REWRITE: return "REWRITE"; + default: return "?"; + } +} + +std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk) +{ + out << toString(tnk); + return out; +} + +TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g) +{ + Node ckey = getConflictProven(conf); + // if a generator is provided, should confirm that it can prove it + Assert(g == nullptr || g->hasProofFor(ckey)); + return TrustNode(TrustNodeKind::CONFLICT, ckey, g); +} + +TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g) +{ + Node lkey = getLemmaProven(lem); + // if a generator is provided, should confirm that it can prove it + Assert(g == nullptr || g->hasProofFor(lkey)); + return TrustNode(TrustNodeKind::LEMMA, lkey, g); +} + +TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g) +{ + Node pekey = getPropExpProven(lit, exp); + Assert(g == nullptr || g->hasProofFor(pekey)); + return TrustNode(TrustNodeKind::PROP_EXP, pekey, g); +} + +TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g) +{ + Node rkey = getRewriteProven(n, nr); + Assert(g == nullptr || g->hasProofFor(rkey)); + return TrustNode(TrustNodeKind::REWRITE, rkey, g); +} + +TrustNode TrustNode::null() +{ + return TrustNode(TrustNodeKind::INVALID, Node::null()); +} + +TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g) + : d_tnk(tnk), d_proven(p), d_gen(g) +{ + // does not make sense to provide null node with generator + Assert(!d_proven.isNull() || d_gen == nullptr); +} + +TrustNodeKind TrustNode::getKind() const { return d_tnk; } + +Node TrustNode::getNode() const +{ + switch (d_tnk) + { + // the node of lemma is the node itself + case TrustNodeKind::LEMMA: return d_proven; + // the node of the rewrite is the right hand side of EQUAL + case TrustNodeKind::REWRITE: return d_proven[1]; + // the node of an explained propagation is the antecendant of an IMPLIES + // the node of a conflict is underneath a NOT + default: return d_proven[0]; + } +} + +Node TrustNode::getProven() const { return d_proven; } + +ProofGenerator* TrustNode::getGenerator() const { return d_gen; } + +bool TrustNode::isNull() const { return d_proven.isNull(); } + +std::shared_ptr<ProofNode> TrustNode::toProofNode() const +{ + if (d_gen == nullptr) + { + return nullptr; + } + return d_gen->getProofFor(d_proven); +} + +Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); } + +Node TrustNode::getLemmaProven(Node lem) { return lem; } + +Node TrustNode::getPropExpProven(TNode lit, Node exp) +{ + return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit); +} + +Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); } + +void TrustNode::debugCheckClosed(const char* c, + const char* ctx, + bool reqNullGen) +{ + pfgEnsureClosed(d_proven, d_gen, c, ctx, reqNullGen); +} + +std::string TrustNode::identifyGenerator() const +{ + if (d_gen == nullptr) + { + return "null"; + } + return d_gen->identify(); +} + +std::ostream& operator<<(std::ostream& out, TrustNode n) +{ + out << "(" << n.getKind() << " " << n.getProven() << " " + << n.identifyGenerator() << ")"; + return out; +} + +} // namespace theory +} // namespace cvc5 |