d59c8b5250fac7042bd990483e82123b3c5c22d6
1 /********************* */
2 /*! \file proof_generator.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Implementation of proof generator utility
15 #include "expr/proof_generator.h"
17 #include "expr/proof.h"
21 ProofGenerator::ProofGenerator() {}
23 ProofGenerator::~ProofGenerator() {}
25 std::shared_ptr
<ProofNode
> ProofGenerator::getProofFor(Node f
)
27 Unreachable() << "ProofGenerator::getProofFor: " << identify()
28 << " has no implementation" << std::endl
;
32 bool ProofGenerator::addProofTo(Node f
, CDProof
* pf
, CDPOverwrite opolicy
)
34 Trace("pfgen") << "ProofGenerator::addProofTo: " << f
<< "..." << std::endl
;
35 Assert(pf
!= nullptr);
36 // plug in the proof provided by the generator, if it exists
37 std::shared_ptr
<ProofNode
> apf
= getProofFor(f
);
40 if (Trace
.isOn("pfgen"))
44 Trace("pfgen") << "...got proof " << ss
.str() << std::endl
;
46 // Add the proof, without deep copying.
47 if (pf
->addProof(apf
, opolicy
, false))
49 Trace("pfgen") << "...success!" << std::endl
;
52 Trace("pfgen") << "...failed to add proof" << std::endl
;
56 Trace("pfgen") << "...failed, no proof" << std::endl
;
57 Assert(false) << "Failed to get proof from generator for fact " << f
;
62 PRefProofGenerator::PRefProofGenerator(CDProof
* cd
) : d_proof(cd
) {}
64 PRefProofGenerator::~PRefProofGenerator() {}
66 std::shared_ptr
<ProofNode
> PRefProofGenerator::getProofFor(Node f
)
68 Trace("pfgen") << "PRefProofGenerator::getProofFor: " << f
<< std::endl
;
69 return d_proof
->mkProof(f
);
72 std::string
PRefProofGenerator::identify() const
74 return "PRefProofGenerator";