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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index e22528490..6ab74cf9a 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -668,6 +668,11 @@ const std::map<Node, ExtfInfoTmp>& ExtfSolver::getInfo() const } bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); } +std::vector<Node> ExtfSolver::getActive(Kind k) const +{ + return d_extt->getActive(k); +} + } // namespace strings } // namespace theory } // namespace CVC4 |