diff options
Diffstat (limited to 'src/theory/theory.h')
| -rw-r--r-- | src/theory/theory.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index d6b02e070..63ca46b41 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -42,6 +42,7 @@ #include "theory/logic_info.h" #include "theory/output_channel.h" #include "theory/theory_id.h" +#include "theory/theory_rewriter.h" #include "theory/valuation.h" #include "util/statistics_registry.h" @@ -317,6 +318,11 @@ public: virtual ~Theory(); /** + * Creates a new theory rewriter for the theory. + */ + virtual std::unique_ptr<TheoryRewriter> mkTheoryRewriter() = 0; + + /** * Subclasses of Theory may add additional efforts. DO NOT CHECK * equality with one of these values (e.g. if STANDARD xxx) but * rather use range checks (or use the helper functions below). |