1 

/********************* */ 
2 

/*! \file infer_proof_cons.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Gereon Kremer 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief Inference to proof conversion for datatypes 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H 
18 

#define CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H 
19 


20 

#include "context/cdhashmap.h" 
21 

#include "expr/node.h" 
22 

#include "expr/proof_generator.h" 
23 

#include "theory/datatypes/inference.h" 
24 


25 

namespace CVC4 { 
26 


27 

class ProofNodeManager; 
28 


29 

namespace theory { 
30 

namespace datatypes { 
31 


32 

/** 
33 

* Converts between the datatypespecific (untrustworthy) DatatypesInference 
34 

* class and information about how to construct a trustworthy proof step 
35 

* (PfRule, children, args). It acts as a (lazy) proof generator where the 
36 

* former is registered via notifyFact and the latter is asked for in 
37 

* getProofFor, typically by the proof equality engine. 
38 

* 
39 

* The main (private) method of this class is convert below, which is 
40 

* called when we need to construct a proof node from an InferInfo. 
41 

*/ 
42 

class InferProofCons : public ProofGenerator 
43 

{ 
44 

typedef context:: 
45 

CDHashMap<Node, std::shared_ptr<DatatypesInference>, NodeHashFunction> 
46 

NodeDatatypesInferenceMap; 
47 


48 

public: 
49 

InferProofCons(context::Context* c, ProofNodeManager* pnm); 
50 
2681 
~InferProofCons() {} 
51 

/** 
52 

* This is called to notify that di is an inference that may need a proof 
53 

* in the future. 
54 

* 
55 

* In detail, this class should be prepared to respond to a call to: 
56 

* getProofFor(di.d_conc) 
57 

* in the remainder of the SAT context. This method copies di and stores it 
58 

* in the contextdependent map d_lazyFactMap below. 
59 

* 
60 

* This is used for lazy proof construction, where proofs are constructed 
61 

* only for facts that are explained. 
62 

*/ 
63 

void notifyFact(const std::shared_ptr<DatatypesInference>& di); 
64 


65 

/** 
66 

* This returns the proof for fact. This is required for using this class as 
67 

* a lazy proof generator. 
68 

* 
69 

* It should be the case that a call was made to notifyFact(di) where 
70 

* di.d_conc is fact in this SAT context. 
71 

*/ 
72 

std::shared_ptr<ProofNode> getProofFor(Node fact) override; 
73 

/** Identify this generator (for debugging, etc..) */ 
74 

virtual std::string identify() const override; 
75 


76 

private: 
77 

/** convert 
78 

* 
79 

* This method is called when the theory of strings makes an inference 
80 

* described by an InferInfo, whose fields are given by the first four 
81 

* arguments of this method. 
82 

* 
83 

* This method converts this call to instructions on what the proof rule 
84 

* step(s) are for concluding the conclusion of the inference. This 
85 

* information is stored in cdp. 
86 

*/ 
87 

void convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp); 
88 

/** A dummy context used by this class if none is provided */ 
89 

context::Context d_context; 
90 

/** the proof node manager */ 
91 

ProofNodeManager* d_pnm; 
92 

/** The lazy fact map */ 
93 

NodeDatatypesInferenceMap d_lazyFactMap; 
94 

}; 
95 


96 

} // namespace datatypes 
97 

} // namespace theory 
98 

} // namespace CVC4 
99 


100 

#endif /* CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H */ 