1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Techniques for eliminating regular expressions. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
#ifndef CVC5__THEORY__STRINGS__REGEXP_ELIM_H |
18 |
|
#define CVC5__THEORY__STRINGS__REGEXP_ELIM_H |
19 |
|
|
20 |
|
#include "expr/node.h" |
21 |
|
#include "theory/eager_proof_generator.h" |
22 |
|
#include "theory/trust_node.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
namespace strings { |
27 |
|
|
28 |
|
/** Regular expression membership elimination |
29 |
|
* |
30 |
|
* This class implements techniques for reducing regular expression memberships |
31 |
|
* to bounded integer quantifiers + extended function constraints. |
32 |
|
* |
33 |
|
* It is used by TheoryStrings during ppRewrite. |
34 |
|
*/ |
35 |
9460 |
class RegExpElimination |
36 |
|
{ |
37 |
|
public: |
38 |
|
/** |
39 |
|
* @param isAgg Whether aggressive eliminations are enabled |
40 |
|
* @param pnm The proof node manager to use (for proofs) |
41 |
|
* @param c The context to use (for proofs) |
42 |
|
*/ |
43 |
|
RegExpElimination(bool isAgg = false, |
44 |
|
ProofNodeManager* pnm = nullptr, |
45 |
|
context::Context* c = nullptr); |
46 |
|
/** eliminate membership |
47 |
|
* |
48 |
|
* This method takes as input a regular expression membership atom of the |
49 |
|
* form (str.in.re x R). If this method returns a non-null node ret, then ret |
50 |
|
* is equivalent to atom. |
51 |
|
* |
52 |
|
* @param atom The node to eliminate |
53 |
|
* @param isAgg Whether we apply aggressive elimination techniques |
54 |
|
* @return The node with regular expressions eliminated, or null if atom |
55 |
|
* was unchanged. |
56 |
|
*/ |
57 |
|
static Node eliminate(Node atom, bool isAgg); |
58 |
|
|
59 |
|
/** |
60 |
|
* Return the trust node corresponding to rewriting n based on eliminate |
61 |
|
* above. |
62 |
|
*/ |
63 |
|
TrustNode eliminateTrusted(Node atom); |
64 |
|
|
65 |
|
private: |
66 |
|
/** return elimination |
67 |
|
* |
68 |
|
* This method is called when atom is rewritten to atomElim, and returns |
69 |
|
* atomElim. id is an identifier indicating the reason for the elimination. |
70 |
|
*/ |
71 |
|
static Node returnElim(Node atom, Node atomElim, const char* id); |
72 |
|
/** elimination for regular expression concatenation */ |
73 |
|
static Node eliminateConcat(Node atom, bool isAgg); |
74 |
|
/** elimination for regular expression star */ |
75 |
|
static Node eliminateStar(Node atom, bool isAgg); |
76 |
|
/** Are proofs enabled? */ |
77 |
|
bool isProofEnabled() const; |
78 |
|
/** Are aggressive eliminations enabled? */ |
79 |
|
bool d_isAggressive; |
80 |
|
/** Pointer to the proof node manager */ |
81 |
|
ProofNodeManager* d_pnm; |
82 |
|
/** An eager proof generator for storing proofs in eliminate trusted above */ |
83 |
|
std::unique_ptr<EagerProofGenerator> d_epg; |
84 |
|
}; /* class RegExpElimination */ |
85 |
|
|
86 |
|
} // namespace strings |
87 |
|
} // namespace theory |
88 |
|
} // namespace cvc5 |
89 |
|
|
90 |
|
#endif /* CVC5__THEORY__STRINGS__REGEXP_ELIM_H */ |