GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/eqc_info.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file eqc_info.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Equivalence class info for the theory of strings
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__STRINGS__EQC_INFO_H
18
#define CVC4__THEORY__STRINGS__EQC_INFO_H
19
20
#include <map>
21
22
#include "context/cdo.h"
23
#include "context/context.h"
24
#include "expr/node.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace strings {
29
30
/**
31
 * SAT-context-dependent information about an equivalence class. This
32
 * information is updated eagerly as assertions are processed by the theory of
33
 * strings at standard effort.
34
 */
35
class EqcInfo
36
{
37
 public:
38
  EqcInfo(context::Context* c);
39
21392
  ~EqcInfo() {}
40
  /** add prefix constant
41
   *
42
   * This informs this equivalence class info that a term t in its
43
   * equivalence class has a constant prefix (if isSuf=true) or suffix
44
   * (if isSuf=false). The constant c (if non-null) is the value of that
45
   * constant, if it has been computed already.
46
   *
47
   * If this method returns a non-null node ret, then ret is a conjunction
48
   * corresponding to a conflict that holds in the current context.
49
   */
50
  Node addEndpointConst(Node t, Node c, bool isSuf);
51
  /**
52
   * If non-null, this is a term x from this eq class such that str.len( x )
53
   * occurs as a term in this SAT context.
54
   */
55
  context::CDO<Node> d_lengthTerm;
56
  /**
57
   * If non-null, this is a term x from this eq class such that str.code( x )
58
   * occurs as a term in this SAT context.
59
   */
60
  context::CDO<Node> d_codeTerm;
61
  context::CDO<unsigned> d_cardinalityLemK;
62
  context::CDO<Node> d_normalizedLength;
63
  /**
64
   * A node that explains the longest constant prefix known of this
65
   * equivalence class. This can either be:
66
   * (1) A term from this equivalence class, including a constant "ABC" or
67
   * concatenation term (str.++ "ABC" ...), or
68
   * (2) A membership of the form (str.in.re x R) where x is in this
69
   * equivalence class and R is a regular expression of the form
70
   * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...).
71
   */
72
  context::CDO<Node> d_prefixC;
73
  /** same as above, for suffix. */
74
  context::CDO<Node> d_suffixC;
75
};
76
77
}  // namespace strings
78
}  // namespace theory
79
}  // namespace CVC4
80
81
#endif /* CVC4__THEORY__STRINGS__EQC_INFO_H */