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