1 

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

/*! \file infer_info.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Mudathir Mohamed, 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 information utility 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__STRINGS__INFER_INFO_H 
18 

#define CVC4__THEORY__STRINGS__INFER_INFO_H 
19 


20 

#include <map> 
21 

#include <vector> 
22 


23 

#include "expr/node.h" 
24 

#include "theory/inference_id.h" 
25 

#include "theory/theory_inference.h" 
26 

#include "util/safe_print.h" 
27 


28 

namespace CVC4 { 
29 

namespace theory { 
30 

namespace strings { 
31 


32 

/** 
33 

* Length status, used for indicating the length constraints for Skolems 
34 

* introduced by the theory of strings. 
35 

*/ 
36 

enum LengthStatus 
37 

{ 
38 

// The length of the Skolem should not be constrained. This should be 
39 

// used for Skolems whose length is already implied. 
40 

LENGTH_IGNORE, 
41 

// The length of the Skolem is not specified, and should be split on. 
42 

LENGTH_SPLIT, 
43 

// The length of the Skolem is exactly one. 
44 

LENGTH_ONE, 
45 

// The length of the Skolem is greater than or equal to one. 
46 

LENGTH_GEQ_ONE 
47 

}; 
48 


49 

class InferenceManager; 
50 


51 

/** 
52 

* An inference. This is a class to track an unprocessed call to either 
53 

* send a fact, lemma, or conflict that is waiting to be asserted to the 
54 

* equality engine or sent on the output channel. 
55 

* 
56 

* For the sake of proofs, the premises in InferInfo have a particular 
57 

* ordering for many of the core strings rules, which is expected by 
58 

* InferProofCons for constructing proofs of F_CONST, F_UNIFY, N_CONST, etc. 
59 

* which apply to a pair of string terms t and s. At a high level, the ordering 
60 

* expected in d_ant is: 
61 

* (1) (multiple) literals that explain why t and s have the same prefix/suffix, 
62 

* (2) t = s, 
63 

* (3) (optionally) a length constraint. 
64 

* For example, say we have: 
65 

* { x ++ y ++ v1 = z ++ w ++ v2, x = z ++ u, u = "", len(y) = len(w) } 
66 

* We can conclude y = w by the N_UNIFY rule from the left side. The premise 
67 

* has the following form: 
68 

*  (prefix up to y/w equal) x = z ++ u, u = "", 
69 

*  (main equality) x ++ y ++ v1 = z ++ w ++ v2, 
70 

*  (length constraint) len(y) = len(w). 
71 

*/ 
72 
56326 
class InferInfo : public TheoryInference 
73 

{ 
74 

public: 
75 

InferInfo(InferenceId id); 
76 
134996 
~InferInfo() {} 
77 

/** Process lemma */ 
78 

TrustNode processLemma(LemmaProperty& p) override; 
79 

/** Process internal fact */ 
80 

Node processFact(std::vector<Node>& exp, ProofGenerator*& pg) override; 
81 

/** Pointer to the class used for processing this info */ 
82 

InferenceManager* d_sim; 
83 

/** Whether it is the reverse form of the above id */ 
84 

bool d_idRev; 
85 

/** The conclusion */ 
86 

Node d_conc; 
87 

/** 
88 

* The premise(s) of the inference, interpreted conjunctively. These are 
89 

* literals that currently hold in the equality engine. 
90 

*/ 
91 

std::vector<Node> d_premises; 
92 

/** 
93 

* The "new literal" premise(s) of the inference, interpreted 
94 

* conjunctively. These are literals that were needed to show the conclusion 
95 

* but do not currently hold in the equality engine. These should be a subset 
96 

* of d_ant. In other words, premises that are not explained are stored 
97 

* in *both* d_ant and d_noExplain. 
98 

*/ 
99 

std::vector<Node> d_noExplain; 
100 

/** 
101 

* A list of new skolems introduced as a result of this inference. They 
102 

* are mapped to by a length status, indicating the length constraint that 
103 

* can be assumed for them. 
104 

*/ 
105 

std::map<LengthStatus, std::vector<Node> > d_skolems; 
106 

/** Is this infer info trivial? True if d_conc is true. */ 
107 

bool isTrivial() const; 
108 

/** 
109 

* Does this infer info correspond to a conflict? True if d_conc is false 
110 

* and it has no new premises (d_noExplain). 
111 

*/ 
112 

bool isConflict() const; 
113 

/** 
114 

* Does this infer info correspond to a "fact". A fact is an inference whose 
115 

* conclusion should be added as an equality or predicate to the equality 
116 

* engine with no new external premises (d_noExplain). 
117 

*/ 
118 

bool isFact() const; 
119 

/** Get premises */ 
120 

Node getPremises() const; 
121 

}; 
122 


123 

/** 
124 

* Writes an inference info to a stream. 
125 

* 
126 

* @param out The stream to write to 
127 

* @param ii The inference info to write to the stream 
128 

* @return The stream 
129 

*/ 
130 

std::ostream& operator<<(std::ostream& out, const InferInfo& ii); 
131 


132 

} // namespace strings 
133 

} // namespace theory 
134 

} // namespace CVC4 
135 


136 

#endif /* CVC4__THEORY__STRINGS__INFER_INFO_H */ 