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

Line Exec Source
1
/*********************                                                        */
2
/*! \file regexp_solver.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang, Andres Noetzli
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 Regular expression solver for the theory of strings.
13
 **
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__STRINGS__REGEXP_SOLVER_H
19
#define CVC4__THEORY__STRINGS__REGEXP_SOLVER_H
20
21
#include <map>
22
#include "context/cdhashset.h"
23
#include "context/cdlist.h"
24
#include "context/context.h"
25
#include "expr/node.h"
26
#include "theory/strings/extf_solver.h"
27
#include "theory/strings/inference_manager.h"
28
#include "theory/strings/skolem_cache.h"
29
#include "theory/strings/regexp_operation.h"
30
#include "theory/strings/sequences_stats.h"
31
#include "theory/strings/solver_state.h"
32
#include "util/string.h"
33
34
namespace CVC4 {
35
namespace theory {
36
namespace strings {
37
38
class RegExpSolver
39
{
40
  typedef context::CDList<Node> NodeList;
41
  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
42
  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
43
  typedef context::CDHashMap<Node, unsigned, NodeHashFunction> NodeUIntMap;
44
  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
45
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
46
47
 public:
48
  RegExpSolver(SolverState& s,
49
               InferenceManager& im,
50
               SkolemCache* skc,
51
               CoreSolver& cs,
52
               ExtfSolver& es,
53
               SequencesStatistics& stats);
54
8992
  ~RegExpSolver() {}
55
56
  /** check regular expression memberships
57
   *
58
   * This checks the satisfiability of all regular expression memberships
59
   * of the form (not) s in R. We use various heuristic techniques based on
60
   * unrolling, combined with techniques from Liang et al, "A Decision Procedure
61
   * for Regular Membership and Length Constraints over Unbounded Strings",
62
   * FroCoS 2015.
63
   */
64
  void checkMemberships();
65
66
 private:
67
  /** check
68
   *
69
   * Tells this solver to check whether the regular expressions in mems
70
   * are consistent. If they are not, then this class will call the
71
   * sendInference method of its parent TheoryString object, indicating that
72
   * it requires a conflict or lemma to be processed.
73
   *
74
   * The argument mems maps representative string terms r to memberships of the
75
   * form (t in R) or ~(t in R), where t = r currently holds in the equality
76
   * engine of the theory of strings.
77
   */
78
  void check(const std::map<Node, std::vector<Node>>& mems);
79
  /**
80
   * Check memberships in equivalence class for regular expression
81
   * inclusion.
82
   *
83
   * This method returns false if it discovered a conflict for this set of
84
   * assertions, and true otherwise. It discovers a conflict e.g. if mems
85
   * contains str.in.re(xi, Ri) and ~str.in.re(xj, Rj) and Rj includes Ri.
86
   *
87
   * @param mems Vector of memberships of the form: (~)str.in.re(x1, R1)
88
   *             ... (~)str.in.re(xn, Rn) where x1 = ... = xn in the
89
   *             current context. The function removes elements from this
90
   *             vector that were marked as reduced.
91
   * @param expForRe Additional explanations for regular expressions.
92
   * @return False if a conflict was detected, true otherwise
93
   */
94
  bool checkEqcInclusion(std::vector<Node>& mems);
95
96
  /**
97
   * Check memberships for equivalence class.
98
   * The vector mems is a vector of memberships of the form:
99
   *   (~) (x1 in R1 ) ... (~) (xn in Rn)
100
   * where x1 = ... = xn in the current context.
101
   *
102
   * This method may add lemmas or conflicts via the inference manager.
103
   *
104
   * This method returns false if it discovered a conflict for this set of
105
   * assertions, and true otherwise. It discovers a conflict e.g. if mems
106
   * contains (xi in Ri) and (xj in Rj) and intersect(xi,xj) is empty.
107
   */
108
  bool checkEqcIntersect(const std::vector<Node>& mems);
109
  // Constants
110
  Node d_emptyString;
111
  Node d_emptyRegexp;
112
  Node d_true;
113
  Node d_false;
114
  /** The solver state of the parent of this object */
115
  SolverState& d_state;
116
  /** the output channel of the parent of this object */
117
  InferenceManager& d_im;
118
  /** reference to the core solver, used for certain queries */
119
  CoreSolver& d_csolver;
120
  /** reference to the extended function solver of the parent */
121
  ExtfSolver& d_esolver;
122
  /** Reference to the statistics for the theory of strings/sequences. */
123
  SequencesStatistics& d_statistics;
124
  // check membership constraints
125
  Node mkAnd(Node c1, Node c2);
126
  /**
127
   * Check partial derivative
128
   *
129
   * Returns false if a lemma pertaining to checking the partial derivative
130
   * of x in r was added. In this case, addedLemma is updated to true.
131
   *
132
   * The argument atom is the assertion that explains x in r, which is the
133
   * normalized form of atom that may be modified using a substitution whose
134
   * explanation is nf_exp.
135
   */
136
  bool checkPDerivative(
137
      Node x, Node r, Node atom, bool& addedLemma, std::vector<Node>& nf_exp);
138
  Node getMembership(Node n, bool isPos, unsigned i);
139
  unsigned getNumMemberships(Node n, bool isPos);
140
  CVC4::String getHeadConst(Node x);
141
  bool deriveRegExp(Node x, Node r, Node atom, std::vector<Node>& ant);
142
  Node getNormalSymRegExp(Node r, std::vector<Node>& nf_exp);
143
  // regular expression memberships
144
  NodeSet d_regexp_ucached;
145
  NodeSet d_regexp_ccached;
146
  // semi normal forms for symbolic expression
147
  std::map<Node, Node> d_nf_regexps;
148
  std::map<Node, std::vector<Node> > d_nf_regexps_exp;
149
  // processed memberships
150
  NodeSet d_processed_memberships;
151
  /** regular expression operation module */
152
  RegExpOpr d_regexp_opr;
153
}; /* class TheoryStrings */
154
155
}  // namespace strings
156
}  // namespace theory
157
}  // namespace CVC4
158
159
#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */