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
|
/********************* */
/*! \file proof_output_channel.cpp
** \verbatim
** Top contributors (to current version):
** Guy Katz, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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 "base/cvc4_assert.h"
#include "proof_output_channel.h"
#include "theory/term_registration_visitor.h"
#include "theory/valuation.h"
namespace CVC4 {
ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() {
Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl;
Assert(d_conflict.isNull());
Assert(!n.isNull());
d_conflict = n;
Assert(pf != NULL);
d_proof = pf;
}
bool ProofOutputChannel::propagate(TNode x) throw() {
Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x
<< std::endl;
d_propagations.insert(x);
return true;
}
theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool,
bool, bool) {
Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl;
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) throw() {
Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl;
Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl;
}
bool ProofOutputChannel::flipDecision() throw() {
Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl;
AlwaysAssert(false);
return false;
}
void ProofOutputChannel::setIncomplete() throw() {
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 */
|
