GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/prop_proof_manager.cpp Lines: 19 50 38.0 %
Date: 2021-03-23 Branches: 19 182 10.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file prop_proof_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa
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 the proof manager for the PropPfManager
13
 **/
14
15
#include "prop/prop_proof_manager.h"
16
17
#include "expr/proof_ensure_closed.h"
18
#include "expr/proof_node_algorithm.h"
19
#include "prop/prop_proof_manager.h"
20
#include "prop/sat_solver.h"
21
22
namespace CVC4 {
23
namespace prop {
24
25
966
PropPfManager::PropPfManager(context::UserContext* userContext,
26
                             ProofNodeManager* pnm,
27
                             CDCLTSatSolverInterface* satSolver,
28
966
                             ProofCnfStream* cnfProof)
29
    : d_pnm(pnm),
30
966
      d_pfpp(new ProofPostproccess(pnm, cnfProof)),
31
      d_satSolver(satSolver),
32
1932
      d_assertions(userContext)
33
{
34
  // add trivial assumption. This is so that we can check the that the prop
35
  // engine's proof is closed, as the SAT solver's refutation proof may use True
36
  // as an assumption even when True is not given as an assumption. An example
37
  // is when a propagated literal has an empty explanation (i.e., it is a valid
38
  // literal), which leads to adding True as its explanation, since for creating
39
  // a learned clause we need at least two literals.
40
966
  d_assertions.push_back(NodeManager::currentNM()->mkConst(true));
41
966
}
42
43
17103
void PropPfManager::registerAssertion(Node assertion)
44
{
45
17103
  d_assertions.push_back(assertion);
46
17103
}
47
48
void PropPfManager::checkProof(context::CDList<Node>* assertions)
49
{
50
  Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution "
51
                        "proof of false is closed\n";
52
  std::shared_ptr<ProofNode> conflictProof = d_satSolver->getProof();
53
  Assert(conflictProof);
54
  // connect it with CNF proof
55
  d_pfpp->process(conflictProof);
56
  // add given assertions d_assertions
57
  for (const Node& assertion : *assertions)
58
  {
59
    d_assertions.push_back(assertion);
60
  }
61
  std::vector<Node> avec{d_assertions.begin(), d_assertions.end()};
62
  pfnEnsureClosedWrt(
63
      conflictProof.get(), avec, "sat-proof", "PropPfManager::checkProof");
64
}
65
66
2292
std::shared_ptr<ProofNode> PropPfManager::getProof()
67
{
68
  // retrieve the SAT solver's refutation proof
69
4584
  Trace("sat-proof")
70
2292
      << "PropPfManager::getProof: Getting resolution proof of false\n";
71
2292
  std::shared_ptr<ProofNode> conflictProof = d_satSolver->getProof();
72
2292
  Assert(conflictProof);
73
2292
  if (Trace.isOn("sat-proof"))
74
  {
75
    std::vector<Node> fassumps;
76
    expr::getFreeAssumptions(conflictProof.get(), fassumps);
77
    Trace("sat-proof")
78
        << "PropPfManager::getProof: initial free assumptions are:\n";
79
    for (const Node& a : fassumps)
80
    {
81
      Trace("sat-proof") << "- " << a << "\n";
82
    }
83
    Trace("sat-proof-debug")
84
        << "PropPfManager::getProof: proof is " << *conflictProof.get() << "\n";
85
    Trace("sat-proof")
86
        << "PropPfManager::getProof: Connecting with CNF proof\n";
87
  }
88
  // connect it with CNF proof
89
2292
  d_pfpp->process(conflictProof);
90
2292
  if (Trace.isOn("sat-proof"))
91
  {
92
    std::vector<Node> fassumps;
93
    expr::getFreeAssumptions(conflictProof.get(), fassumps);
94
    Trace("sat-proof")
95
        << "PropPfManager::getProof: new free assumptions are:\n";
96
    for (const Node& a : fassumps)
97
    {
98
      Trace("sat-proof") << "- " << a << "\n";
99
    }
100
    Trace("sat-proof") << "PropPfManager::getProof: assertions are:\n";
101
    for (const Node& a : d_assertions)
102
    {
103
      Trace("sat-proof") << "- " << a << "\n";
104
    }
105
    Trace("sat-proof-debug")
106
        << "PropPfManager::getProof: proof is " << *conflictProof.get() << "\n";
107
  }
108
2292
  return conflictProof;
109
}
110
111
}  // namespace prop
112
26685
}  // namespace CVC4