diff options
Diffstat (limited to 'src/theory/strings/extf_solver.h')
| -rw-r--r-- | src/theory/strings/extf_solver.h | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 9ca72fed2..e7e2512bd 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -17,8 +17,8 @@ #ifndef CVC4__THEORY__STRINGS__EXTF_SOLVER_H #define CVC4__THEORY__STRINGS__EXTF_SOLVER_H -#include <vector> #include <map> +#include <vector> #include "context/cdo.h" #include "expr/node.h" @@ -29,6 +29,7 @@ #include "theory/strings/sequences_stats.h" #include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" +#include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_preprocess.h" namespace CVC4 { @@ -87,10 +88,11 @@ class ExtfSolver SolverState& s, InferenceManager& im, SkolemCache& skc, + StringsRewriter& rewriter, BaseSolver& bs, CoreSolver& cs, ExtTheory* et, - SequencesStatistics& stats); + SequencesStatistics& statistics); ~ExtfSolver(); /** check extended functions evaluation @@ -180,6 +182,8 @@ class ExtfSolver InferenceManager& d_im; /** cache of all skolems */ SkolemCache& d_skCache; + /** The theory rewriter for this theory. */ + StringsRewriter& d_rewriter; /** reference to the base solver, used for certain queries */ BaseSolver& d_bsolver; /** reference to the core solver, used for certain queries */ |