diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-22 10:07:44 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-22 10:07:44 -0600 |
| commit | 25d2ed390bf5ad825fadbc4ed21676100b01de68 (patch) | |
| tree | 156852139ee7a5bc5e42d1fc2564c75b291216fe /src/theory/strings/extf_solver.h | |
| parent | 9b20af281db3e77a25540305dfb73cbe56519f75 (diff) | |
Move check memberships to reg exp solver (#3793)
There was previously a function in TheoryStrings to make the proper call to checkMembership. In the refactored code, this is no longer necessary and the interface to RegExp can be simplified.
Diffstat (limited to 'src/theory/strings/extf_solver.h')
| -rw-r--r-- | src/theory/strings/extf_solver.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index e0e41bc3d..4c848f430 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -145,6 +145,11 @@ class ExtfSolver const std::map<Node, ExtfInfoTmp>& getInfo() const; /** Are there any active extended functions? */ bool hasExtendedFunctions() const; + /** + * Get the function applications of kind k that are active in the current + * context (see ExtTheory::getActive). + */ + std::vector<Node> getActive(Kind k) const; private: /** do reduction |