GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_generator.cpp Lines: 3 26 11.5 %
Date: 2021-03-23 Branches: 2 120 1.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
11
 **
12
 ** \brief Implementation of proof generator utility
13
 **/
14
15
#include "expr/proof_generator.h"
16
17
#include <sstream>
18
19
#include "expr/proof.h"
20
#include "expr/proof_node.h"
21
#include "expr/proof_node_algorithm.h"
22
#include "options/smt_options.h"
23
24
namespace CVC4 {
25
26
std::ostream& operator<<(std::ostream& out, CDPOverwrite opol)
27
{
28
  switch (opol)
29
  {
30
    case CDPOverwrite::ALWAYS: out << "ALWAYS"; break;
31
    case CDPOverwrite::ASSUME_ONLY: out << "ASSUME_ONLY"; break;
32
    case CDPOverwrite::NEVER: out << "NEVER"; break;
33
    default: out << "CDPOverwrite:unknown"; break;
34
  }
35
  return out;
36
}
37
38
1168037
ProofGenerator::ProofGenerator() {}
39
40
1168019
ProofGenerator::~ProofGenerator() {}
41
42
std::shared_ptr<ProofNode> ProofGenerator::getProofFor(Node f)
43
{
44
  Unreachable() << "ProofGenerator::getProofFor: " << identify()
45
                << " has no implementation" << std::endl;
46
  return nullptr;
47
}
48
49
bool ProofGenerator::addProofTo(Node f,
50
                                CDProof* pf,
51
                                CDPOverwrite opolicy,
52
                                bool doCopy)
53
{
54
  Trace("pfgen") << "ProofGenerator::addProofTo: " << f << "..." << std::endl;
55
  Assert(pf != nullptr);
56
  // plug in the proof provided by the generator, if it exists
57
  std::shared_ptr<ProofNode> apf = getProofFor(f);
58
  if (apf != nullptr)
59
  {
60
    Trace("pfgen") << "...got proof " << *apf.get() << std::endl;
61
    if (pf->addProof(apf, opolicy, doCopy))
62
    {
63
      Trace("pfgen") << "...success!" << std::endl;
64
      return true;
65
    }
66
    Trace("pfgen") << "...failed to add proof" << std::endl;
67
  }
68
  else
69
  {
70
    Trace("pfgen") << "...failed, no proof" << std::endl;
71
    Assert(false) << "Failed to get proof from generator for fact " << f;
72
  }
73
  return false;
74
}
75
76
26685
}  // namespace CVC4