1 /********************* */
2 /*! \file trust_node.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Implementation of the trust node utility
15 #include "theory/trust_node.h"
17 #include "expr/proof_generator.h"
22 const char* toString(TrustNodeKind tnk
)
26 case TrustNodeKind::CONFLICT
: return "CONFLICT";
27 case TrustNodeKind::LEMMA
: return "LEMMA";
28 case TrustNodeKind::PROP_EXP
: return "PROP_EXP";
29 case TrustNodeKind::REWRITE
: return "REWRITE";
34 std::ostream
& operator<<(std::ostream
& out
, TrustNodeKind tnk
)
40 TrustNode
TrustNode::mkTrustConflict(Node conf
, ProofGenerator
* g
)
42 Node ckey
= getConflictProven(conf
);
43 // if a generator is provided, should confirm that it can prove it
44 Assert(g
== nullptr || g
->hasProofFor(ckey
));
45 return TrustNode(TrustNodeKind::CONFLICT
, ckey
, g
);
48 TrustNode
TrustNode::mkTrustLemma(Node lem
, ProofGenerator
* g
)
50 Node lkey
= getLemmaProven(lem
);
51 // if a generator is provided, should confirm that it can prove it
52 Assert(g
== nullptr || g
->hasProofFor(lkey
));
53 return TrustNode(TrustNodeKind::LEMMA
, lkey
, g
);
56 TrustNode
TrustNode::mkTrustPropExp(TNode lit
, Node exp
, ProofGenerator
* g
)
58 Node pekey
= getPropExpProven(lit
, exp
);
59 Assert(g
== nullptr || g
->hasProofFor(pekey
));
60 return TrustNode(TrustNodeKind::PROP_EXP
, pekey
, g
);
63 TrustNode
TrustNode::mkTrustRewrite(TNode n
, Node nr
, ProofGenerator
* g
)
65 Node rkey
= getRewriteProven(n
, nr
);
66 Assert(g
== nullptr || g
->hasProofFor(rkey
));
67 return TrustNode(TrustNodeKind::REWRITE
, rkey
, g
);
70 TrustNode
TrustNode::null()
72 return TrustNode(TrustNodeKind::INVALID
, Node::null());
75 TrustNode::TrustNode(TrustNodeKind tnk
, Node p
, ProofGenerator
* g
)
76 : d_tnk(tnk
), d_proven(p
), d_gen(g
)
78 // does not make sense to provide null node with generator
79 Assert(!d_proven
.isNull() || d_gen
== nullptr);
82 TrustNodeKind
TrustNode::getKind() const { return d_tnk
; }
84 Node
TrustNode::getNode() const
88 // the node of lemma is the node itself
89 case TrustNodeKind::LEMMA
: return d_proven
;
90 // the node of the rewrite is the right hand side of EQUAL
91 case TrustNodeKind::REWRITE
: return d_proven
[1];
92 // the node of an explained propagation is the antecendant of an IMPLIES
93 // the node of a conflict is underneath a NOT
94 default: return d_proven
[0];
98 Node
TrustNode::getProven() const { return d_proven
; }
100 ProofGenerator
* TrustNode::getGenerator() const { return d_gen
; }
102 bool TrustNode::isNull() const { return d_proven
.isNull(); }
104 std::shared_ptr
<ProofNode
> TrustNode::toProofNode() const
106 if (d_gen
== nullptr)
110 return d_gen
->getProofFor(d_proven
);
113 Node
TrustNode::getConflictProven(Node conf
) { return conf
.notNode(); }
115 Node
TrustNode::getLemmaProven(Node lem
) { return lem
; }
117 Node
TrustNode::getPropExpProven(TNode lit
, Node exp
)
119 return NodeManager::currentNM()->mkNode(kind::IMPLIES
, exp
, lit
);
122 Node
TrustNode::getRewriteProven(TNode n
, Node nr
) { return n
.eqNode(nr
); }
124 void TrustNode::debugCheckClosed(const char* c
,
128 pfgEnsureClosed(d_proven
, d_gen
, c
, ctx
, reqNullGen
);
131 std::string
TrustNode::identifyGenerator() const
133 if (d_gen
== nullptr)
137 return d_gen
->identify();
140 std::ostream
& operator<<(std::ostream
& out
, TrustNode n
)
142 out
<< "(" << n
.getKind() << " " << n
.getProven() << " "
143 << n
.identifyGenerator() << ")";
147 } // namespace theory