GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/infer_info.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 4 8 50.0 %

Line Exec Source
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) 2009-2021 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
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
56320
class InferInfo : public TheoryInference
73
{
74
 public:
75
  InferInfo(InferenceId id);
76
134974
  ~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 */