summaryrefslogtreecommitdiff
path: root/src/theory/strings/extf_solver.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/extf_solver.h')
-rw-r--r--src/theory/strings/extf_solver.h7
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index c5dd24f70..fb9b836db 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -91,7 +91,7 @@ class ExtfSolver
StringsRewriter& rewriter,
BaseSolver& bs,
CoreSolver& cs,
- ExtTheory* et,
+ ExtTheory& et,
SequencesStatistics& statistics);
~ExtfSolver();
@@ -147,6 +147,7 @@ class ExtfSolver
* checkExtfEval.
*/
const std::map<Node, ExtfInfoTmp>& getInfo() const;
+ //---------------------------------- information about ExtTheory
/** Are there any active extended functions? */
bool hasExtendedFunctions() const;
/**
@@ -154,7 +155,7 @@ class ExtfSolver
* context (see ExtTheory::getActive).
*/
std::vector<Node> getActive(Kind k) const;
-
+ //---------------------------------- end information about ExtTheory
private:
/** do reduction
*
@@ -190,7 +191,7 @@ class ExtfSolver
/** reference to the core solver, used for certain queries */
CoreSolver& d_csolver;
/** the extended theory object for the theory of strings */
- ExtTheory* d_extt;
+ ExtTheory& d_extt;
/** Reference to the statistics for the theory of strings/sequences. */
SequencesStatistics& d_statistics;
/** preprocessing utility, for performing strings reductions */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback