1 /********************* */
2 /*! \file eager_proof_generator.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 abstract proof generator class
15 #include "theory/eager_proof_generator.h"
17 #include "expr/proof.h"
18 #include "expr/proof_node_manager.h"
23 EagerProofGenerator::EagerProofGenerator(ProofNodeManager
* pnm
,
26 : d_pnm(pnm
), d_name(name
), d_proofs(c
== nullptr ? &d_context
: c
)
30 void EagerProofGenerator::setProofFor(Node f
, std::shared_ptr
<ProofNode
> pf
)
33 Assert(pf
->getResult() == f
);
36 void EagerProofGenerator::setProofForConflict(Node conf
,
37 std::shared_ptr
<ProofNode
> pf
)
39 // Normalize based on key
40 Node ckey
= TrustNode::getConflictProven(conf
);
41 setProofFor(ckey
, pf
);
44 void EagerProofGenerator::setProofForLemma(Node lem
,
45 std::shared_ptr
<ProofNode
> pf
)
47 // Normalize based on key
48 Node lkey
= TrustNode::getLemmaProven(lem
);
49 setProofFor(lkey
, pf
);
52 void EagerProofGenerator::setProofForPropExp(TNode lit
,
54 std::shared_ptr
<ProofNode
> pf
)
56 // Normalize based on key
57 Node pekey
= TrustNode::getPropExpProven(lit
, exp
);
58 setProofFor(pekey
, pf
);
61 std::shared_ptr
<ProofNode
> EagerProofGenerator::getProofFor(Node f
)
63 NodeProofNodeMap::iterator it
= d_proofs
.find(f
);
64 if (it
== d_proofs
.end())
71 bool EagerProofGenerator::hasProofFor(Node f
)
73 return d_proofs
.find(f
) != d_proofs
.end();
76 TrustNode
EagerProofGenerator::mkTrustNode(Node n
,
77 std::shared_ptr
<ProofNode
> pf
,
82 return TrustNode::null();
86 // this shouldnt modify the key
87 setProofForConflict(n
, pf
);
88 // we can now return the trust node
89 return TrustNode::mkTrustConflict(n
, this);
91 // this shouldnt modify the key
92 setProofForLemma(n
, pf
);
93 // we can now return the trust node
94 return TrustNode::mkTrustLemma(n
, this);
97 TrustNode
EagerProofGenerator::mkTrustNode(Node conc
,
99 const std::vector
<Node
>& exp
,
100 const std::vector
<Node
>& args
,
103 // if no children, its easy
106 std::shared_ptr
<ProofNode
> pf
= d_pnm
->mkNode(id
, {}, args
, conc
);
107 return mkTrustNode(conc
, pf
, isConflict
);
109 // otherwise, we use CDProof + SCOPE
111 cdp
.addStep(conc
, id
, exp
, args
);
112 std::shared_ptr
<ProofNode
> pf
= cdp
.getProofFor(conc
);
113 // We use mkNode instead of mkScope, since there is no reason to check
114 // whether the free assumptions of pf are in exp, since they are by the
115 // construction above.
116 std::shared_ptr
<ProofNode
> pfs
= d_pnm
->mkNode(PfRule::SCOPE
, {pf
}, exp
);
117 return mkTrustNode(pfs
->getResult(), pfs
, isConflict
);
120 TrustNode
EagerProofGenerator::mkTrustedPropagation(
121 Node n
, Node exp
, std::shared_ptr
<ProofNode
> pf
)
125 return TrustNode::null();
127 setProofForPropExp(n
, exp
, pf
);
128 return TrustNode::mkTrustPropExp(n
, exp
, this);
131 TrustNode
EagerProofGenerator::mkTrustNodeSplit(Node f
)
134 Node lem
= f
.orNode(f
.notNode());
135 return mkTrustNode(lem
, PfRule::SPLIT
, {}, {f
}, false);
138 std::string
EagerProofGenerator::identify() const { return d_name
; }
140 } // namespace theory