diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-15 20:52:46 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-15 20:52:46 -0500 |
| commit | 37a080c02e769cc2fe5427c11a5f0dc362c25465 (patch) | |
| tree | 25af1b1c878abbaae07b88c2facc1a36d24e1a19 /src/theory/strings/theory_strings.h | |
| parent | b9f0e5df83a9e8cfd489112a385e4ee3520de771 (diff) | |
Make strings fmf apply to all but internally generated Skolems (#1780)
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index cff49ccb8..22406adef 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -489,6 +489,8 @@ private: sk_id_deq_z, }; std::map<Node, std::map<Node, std::map<int, Node> > > d_skolem_cache; + /** the set of all skolems we have generated */ + std::unordered_set<Node, NodeHashFunction> d_all_skolems; Node mkSkolemCached( Node a, Node b, int id, const char* c, int isLenSplit = 0); inline Node mkSkolemS(const char* c, int isLenSplit = 0); |