diff options
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 37b89cfb7..3f24c8bab 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -108,6 +108,7 @@ namespace smt { namespace theory { class TheoryModel; + class Rewriter; }/* CVC4::theory namespace */ // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the @@ -134,6 +135,7 @@ class CVC4_PUBLIC SmtEngine friend class ::CVC4::LogicRequest; friend class ::CVC4::Model; // to access d_modelCommands friend class ::CVC4::theory::TheoryModel; + friend class ::CVC4::theory::Rewriter; /* ....................................................................... */ public: @@ -876,6 +878,9 @@ class CVC4_PUBLIC SmtEngine /** Get a pointer to the ProofManager owned by this SmtEngine. */ ProofManager* getProofManager() { return d_proofManager.get(); }; + /** Get a pointer to the Rewriter owned by this SmtEngine. */ + theory::Rewriter* getRewriter() { return d_rewriter.get(); } + /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */ StatisticsRegistry* getStatisticsRegistry() { @@ -1085,6 +1090,14 @@ class CVC4_PUBLIC SmtEngine /** The proof manager */ std::unique_ptr<ProofManager> d_proofManager; + /** + * The rewriter associated with this SmtEngine. We have a different instance + * of the rewriter for each SmtEngine instance. This is because rewriters may + * hold references to objects that belong to theory solvers, which are + * specific to an SmtEngine/TheoryEngine instance. + */ + std::unique_ptr<theory::Rewriter> d_rewriter; + /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; |