GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/prop_proof_manager.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file prop_proof_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Gereon Kremer
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 The proof manager of PropEngine
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__PROP_PROOF_MANAGER_H
18
#define CVC4__PROP_PROOF_MANAGER_H
19
20
#include "context/cdlist.h"
21
#include "expr/proof.h"
22
#include "expr/proof_node_manager.h"
23
#include "prop/proof_post_processor.h"
24
#include "prop/sat_proof_manager.h"
25
26
namespace CVC4 {
27
28
namespace prop {
29
30
class CDCLTSatSolverInterface;
31
32
/**
33
 * This class is responsible for managing the proof output of PropEngine, both
34
 * building and checking it.
35
 *
36
 * The expected proof to be built is a refutation proof with preprocessed
37
 * assertions as free assumptions.
38
 */
39
966
class PropPfManager
40
{
41
 public:
42
  PropPfManager(context::UserContext* userContext,
43
                ProofNodeManager* pnm,
44
                CDCLTSatSolverInterface* satSolver,
45
                ProofCnfStream* cnfProof);
46
47
  /** Saves assertion for later checking whether refutation proof is closed.
48
   *
49
   * The assertions registered via this interface are preprocessed assertions
50
   * from SMT engine as they are asserted to the prop engine.
51
   */
52
  void registerAssertion(Node assertion);
53
  /**
54
   * Generates the prop engine proof: a proof of false resulting from the
55
   * connection of the refutation proof in d_satPM with the justification for
56
   * its assumptions, which are retrieved from the CNF conversion proof, if any.
57
   *
58
   * The connection is done by running the proof post processor d_pfpp over the
59
   * proof of false provided by d_satPM. See ProofPostProcessor for more
60
   * details.
61
   */
62
  std::shared_ptr<ProofNode> getProof();
63
64
  /**
65
   * Checks that the prop engine proof is closed w.r.t. the given assertions and
66
   * previously registered assertions in d_assertions.
67
   *
68
   * A common use of other assertions on top of the ones already registered on
69
   * d_assertions is checking closedness w.r.t. preprocessed *and* input
70
   * assertions. This is necessary if a prop engine's proof is modified
71
   * externally (which can happen, for example, when connecting the prop
72
   * engine's proof with the preprocessing proof) and these changes survive for
73
   * a next check-sat call.
74
   */
75
  void checkProof(context::CDList<Node>* assertions);
76
77
 private:
78
  /** A node manager */
79
  ProofNodeManager* d_pnm;
80
  /** The proof post-processor */
81
  std::unique_ptr<prop::ProofPostproccess> d_pfpp;
82
  /**
83
   * The SAT solver of this prop engine, which should provide a refutation
84
   * proof when requested */
85
  CDCLTSatSolverInterface* d_satSolver;
86
  /** Assertions corresponding to the leaves of the prop engine's proof.
87
   *
88
   * These are kept in a context-dependent manner since the prop engine's proof
89
   * is also kept in a context-dependent manner.
90
   */
91
  context::CDList<Node> d_assertions;
92
}; /* class PropPfManager */
93
94
}  // namespace prop
95
}  // namespace CVC4
96
97
#endif /* CVC4__PROP__PROOF_MANAGER_H */