diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-10 19:44:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-10 19:44:33 -0500 |
commit | 40fd0e4c958b215a3eba9da17f6f194cacb021be (patch) | |
tree | 67a1cfdcf61b428a3754558bbb49af9651c52af0 /src/theory/eager_proof_generator.cpp | |
parent | 2f30f5dc342fa19b42842d744034f53a1dee3f43 (diff) |
(proof-new) Add eager proof generator utility. (#4592)
Adds the eager proof generator. This lives in theory/ since it has utilities for generating TrustNode, which is specific to theory/.
Diffstat (limited to 'src/theory/eager_proof_generator.cpp')
-rw-r--r-- | src/theory/eager_proof_generator.cpp | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp new file mode 100644 index 000000000..27bc9f5ca --- /dev/null +++ b/src/theory/eager_proof_generator.cpp @@ -0,0 +1,125 @@ +/********************* */ +/*! \file eager_proof_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief Implementation of the abstract proof generator class + **/ + +#include "theory/eager_proof_generator.h" + +#include "expr/proof_node_manager.h" + +namespace CVC4 { +namespace theory { + +EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, + context::Context* c) + : d_pnm(pnm), d_proofs(c == nullptr ? &d_context : c) +{ +} + +void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf) +{ + // pf should prove f + Assert(pf->getResult() == f); + d_proofs[f] = pf; +} +void EagerProofGenerator::setProofForConflict(Node conf, + std::shared_ptr<ProofNode> pf) +{ + // Normalize based on key + Node ckey = TrustNode::getConflictProven(conf); + setProofFor(ckey, pf); +} + +void EagerProofGenerator::setProofForLemma(Node lem, + std::shared_ptr<ProofNode> pf) +{ + // Normalize based on key + Node lkey = TrustNode::getLemmaProven(lem); + setProofFor(lkey, pf); +} + +void EagerProofGenerator::setProofForPropExp(TNode lit, + Node exp, + std::shared_ptr<ProofNode> pf) +{ + // Normalize based on key + Node pekey = TrustNode::getPropExpProven(lit, exp); + setProofFor(pekey, pf); +} + +std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f) +{ + NodeProofNodeMap::iterator it = d_proofs.find(f); + if (it == d_proofs.end()) + { + return nullptr; + } + return (*it).second; +} + +bool EagerProofGenerator::hasProofFor(Node f) +{ + return d_proofs.find(f) != d_proofs.end(); +} + +TrustNode EagerProofGenerator::mkTrustNode(Node n, + std::shared_ptr<ProofNode> pf, + bool isConflict) +{ + if (pf == nullptr) + { + return TrustNode::null(); + } + if (isConflict) + { + // this shouldnt modify the key + setProofForConflict(n, pf); + // we can now return the trust node + return TrustNode::mkTrustConflict(n, this); + } + // this shouldnt modify the key + setProofForLemma(n, pf); + // we can now return the trust node + return TrustNode::mkTrustLemma(n, this); +} + +TrustNode EagerProofGenerator::mkTrustNode(Node n, + PfRule id, + const std::vector<Node>& args, + bool isConflict) +{ + std::vector<std::shared_ptr<ProofNode>> children; + std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, children, args, n); + return mkTrustNode(n, pf, isConflict); +} + +TrustNode EagerProofGenerator::mkTrustedPropagation( + Node n, Node exp, std::shared_ptr<ProofNode> pf) +{ + if (pf == nullptr) + { + return TrustNode::null(); + } + setProofForPropExp(n, exp, pf); + return TrustNode::mkTrustPropExp(n, exp, this); +} + +TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f) +{ + // make the lemma + Node lem = f.orNode(f.notNode()); + std::vector<Node> args; + return mkTrustNode(lem, PfRule::SPLIT, args, false); +} + +} // namespace theory +} // namespace CVC4 |