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
|
/********************* */
/*! \file proof_output_channel.cpp
** \verbatim
** Top contributors (to current version):
** Guy Katz, Tim King, Liana Hadarean
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "proof/proof_output_channel.h"
#include "base/check.h"
#include "theory/term_registration_visitor.h"
#include "theory/valuation.h"
namespace CVC4 {
ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(nullptr) {}
const Proof& ProofOutputChannel::getConflictProof() const
{
Assert(hasConflict());
return *d_proof;
}
void ProofOutputChannel::conflict(TNode n, std::unique_ptr<Proof> pf)
{
Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl;
Assert(!hasConflict());
Assert(!d_proof);
d_conflict = n;
d_proof = std::move(pf);
Assert(hasConflict());
Assert(d_proof);
}
bool ProofOutputChannel::propagate(TNode x) {
Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x
<< std::endl;
d_propagations.insert(x);
return true;
}
theory::LemmaStatus ProofOutputChannel::lemma(TNode n,
ProofRule rule,
theory::LemmaProperty p)
{
Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl;
// TODO(#1231): We should transition to supporting multiple lemmas. The
// following assertion cannot be enabled due to
// "test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt".
// Assert(
// d_lemma.isNull()) <<
// "Multiple calls to ProofOutputChannel::lemma() are not supported.";
d_lemma = n;
return theory::LemmaStatus(TNode::null(), 0);
}
theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) {
AlwaysAssert(false);
return theory::LemmaStatus(TNode::null(), 0);
}
void ProofOutputChannel::requirePhase(TNode n, bool b) {
Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl;
Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl;
}
void ProofOutputChannel::setIncomplete() {
Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl;
AlwaysAssert(false);
}
MyPreRegisterVisitor::MyPreRegisterVisitor(theory::Theory* theory)
: d_theory(theory)
, d_visited() {
}
bool MyPreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
return d_visited.find(current) != d_visited.end();
}
void MyPreRegisterVisitor::visit(TNode current, TNode parent) {
d_theory->preRegisterTerm(current);
d_visited.insert(current);
}
void MyPreRegisterVisitor::start(TNode node) {
}
void MyPreRegisterVisitor::done(TNode node) {
}
} /* namespace CVC4 */
|
