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 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H 
18 

#define CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H 
19 


20 

#include <vector> 
21 


22 

#include "expr/node.h" 
23 

#include "expr/proof_checker.h" 
24 

#include "expr/proof_rule.h" 
25 

#include "theory/builtin/proof_checker.h" 
26 

#include "theory/strings/infer_info.h" 
27 

#include "theory/strings/sequences_stats.h" 
28 

#include "theory/theory_proof_step_buffer.h" 
29 

#include "theory/uf/proof_equality_engine.h" 
30 


31 

namespace CVC4 { 
32 

namespace theory { 
33 

namespace strings { 
34 


35 

/** 
36 

* Converts between the stringsspecific (untrustworthy) InferInfo class and 
37 

* information about how to construct a trustworthy proof step 
38 

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

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

* getProofFor, typically by the proof equality engine. 
41 

* 
42 

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

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

*/ 
45 

class InferProofCons : public ProofGenerator 
46 

{ 
47 

typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>, NodeHashFunction> 
48 

NodeInferInfoMap; 
49 


50 

public: 
51 

InferProofCons(context::Context* c, 
52 

ProofNodeManager* pnm, 
53 

SequencesStatistics& statistics); 
54 
1924 
~InferProofCons() {} 
55 

/** 
56 

* This is called to notify that ii is an inference that may need a proof 
57 

* in the future. 
58 

* 
59 

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

* getProofFor(ii.d_conc) 
61 

* in the remainder of the SAT context. This method copies ii and stores it 
62 

* in the contextdependent map d_lazyFactMap below. 
63 

* 
64 

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

* only for facts that are explained. 
66 

*/ 
67 

void notifyFact(const InferInfo& ii); 
68 


69 

/** 
70 

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

* a lazy proof generator. 
72 

* 
73 

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

* ii.d_conc is fact in this SAT context. 
75 

*/ 
76 

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

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

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


80 

private: 
81 

/** convert 
82 

* 
83 

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

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

* arguments of this method. 
86 

* 
87 

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

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

* information is either: 
90 

* 
91 

* (A) stored in the argument ps, which consists of: 
92 

*  A proof rule identifier (ProofStep::d_rule). 
93 

*  The premises of the proof step (ProofStep::d_children). 
94 

*  Arguments to the proof step (ProofStep::d_args). 
95 

* 
96 

* (B) If the proof for the inference cannot be captured by a single 
97 

* step, then the d_rule field of ps is not set, and useBuffer is set to 
98 

* true. In this case, the argument psb is updated to contain (possibly 
99 

* multiple) proof steps for how to construct a proof for the given inference. 
100 

* In particular, psb will contain a set of steps that form a proof 
101 

* whose conclusion is ii.d_conc and whose free assumptions are ii.d_ant. 
102 

*/ 
103 

void convert(InferenceId infer, 
104 

bool isRev, 
105 

Node conc, 
106 

const std::vector<Node>& exp, 
107 

ProofStep& ps, 
108 

TheoryProofStepBuffer& psb, 
109 

bool& useBuffer); 
110 

/** 
111 

* Convert length proof. If this method returns true, it adds proof step(s) 
112 

* to the buffer psb that conclude lenReq from premises lenExp. 
113 

*/ 
114 

bool convertLengthPf(Node lenReq, 
115 

const std::vector<Node>& lenExp, 
116 

TheoryProofStepBuffer& psb); 
117 

/** 
118 

* Helper method, adds the proof of (TRANS eqa eqb) into the proof step 
119 

* buffer psb, where eqa and eqb are flipped as needed. Returns the 
120 

* conclusion, or null if we were not able to construct a TRANS step. 
121 

*/ 
122 

Node convertTrans(Node eqa, Node eqb, TheoryProofStepBuffer& psb); 
123 

/** the proof node manager */ 
124 

ProofNodeManager* d_pnm; 
125 

/** The lazy fact map */ 
126 

NodeInferInfoMap d_lazyFactMap; 
127 

/** Reference to the statistics for the theory of strings/sequences. */ 
128 

SequencesStatistics& d_statistics; 
129 

}; 
130 


131 

} // namespace strings 
132 

} // namespace theory 
133 

} // namespace CVC4 
134 


135 

#endif /* CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H */ 