1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
/********************* */
/*! \file infer_info.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Mudathir Mohamed, Gereon Kremer
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Inference information utility
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__STRINGS__INFER_INFO_H
#define CVC4__THEORY__STRINGS__INFER_INFO_H
#include <map>
#include <vector>
#include "expr/node.h"
#include "theory/inference_id.h"
#include "theory/theory_inference.h"
#include "util/safe_print.h"
namespace cvc5 {
namespace theory {
namespace strings {
/**
* Length status, used for indicating the length constraints for Skolems
* introduced by the theory of strings.
*/
enum LengthStatus
{
// The length of the Skolem should not be constrained. This should be
// used for Skolems whose length is already implied.
LENGTH_IGNORE,
// The length of the Skolem is not specified, and should be split on.
LENGTH_SPLIT,
// The length of the Skolem is exactly one.
LENGTH_ONE,
// The length of the Skolem is greater than or equal to one.
LENGTH_GEQ_ONE
};
class InferenceManager;
/**
* An inference. This is a class to track an unprocessed call to either
* send a fact, lemma, or conflict that is waiting to be asserted to the
* equality engine or sent on the output channel.
*
* For the sake of proofs, the premises in InferInfo have a particular
* ordering for many of the core strings rules, which is expected by
* InferProofCons for constructing proofs of F_CONST, F_UNIFY, N_CONST, etc.
* which apply to a pair of string terms t and s. At a high level, the ordering
* expected in d_ant is:
* (1) (multiple) literals that explain why t and s have the same prefix/suffix,
* (2) t = s,
* (3) (optionally) a length constraint.
* For example, say we have:
* { x ++ y ++ v1 = z ++ w ++ v2, x = z ++ u, u = "", len(y) = len(w) }
* We can conclude y = w by the N_UNIFY rule from the left side. The premise
* has the following form:
* - (prefix up to y/w equal) x = z ++ u, u = "",
* - (main equality) x ++ y ++ v1 = z ++ w ++ v2,
* - (length constraint) len(y) = len(w).
*/
class InferInfo : public TheoryInference
{
public:
InferInfo(InferenceId id);
~InferInfo() {}
/** Process lemma */
TrustNode processLemma(LemmaProperty& p) override;
/** Process internal fact */
Node processFact(std::vector<Node>& exp, ProofGenerator*& pg) override;
/** Pointer to the class used for processing this info */
InferenceManager* d_sim;
/** Whether it is the reverse form of the above id */
bool d_idRev;
/** The conclusion */
Node d_conc;
/**
* The premise(s) of the inference, interpreted conjunctively. These are
* literals that currently hold in the equality engine.
*/
std::vector<Node> d_premises;
/**
* The "new literal" premise(s) of the inference, interpreted
* conjunctively. These are literals that were needed to show the conclusion
* but do not currently hold in the equality engine. These should be a subset
* of d_ant. In other words, premises that are not explained are stored
* in *both* d_ant and d_noExplain.
*/
std::vector<Node> d_noExplain;
/**
* A list of new skolems introduced as a result of this inference. They
* are mapped to by a length status, indicating the length constraint that
* can be assumed for them.
*/
std::map<LengthStatus, std::vector<Node> > d_skolems;
/** Is this infer info trivial? True if d_conc is true. */
bool isTrivial() const;
/**
* Does this infer info correspond to a conflict? True if d_conc is false
* and it has no new premises (d_noExplain).
*/
bool isConflict() const;
/**
* Does this infer info correspond to a "fact". A fact is an inference whose
* conclusion should be added as an equality or predicate to the equality
* engine with no new external premises (d_noExplain).
*/
bool isFact() const;
/** Get premises */
Node getPremises() const;
};
/**
* Writes an inference info to a stream.
*
* @param out The stream to write to
* @param ii The inference info to write to the stream
* @return The stream
*/
std::ostream& operator<<(std::ostream& out, const InferInfo& ii);
} // namespace strings
} // namespace theory
} // namespace cvc5
#endif /* CVC4__THEORY__STRINGS__INFER_INFO_H */
|
