Make Theory class use Env (#7011)

This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index b6cdfb67b..a4e07d2c9 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -19,6 +19,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "options/base_options.h"
+#include "options/smt_options.h"
 #include "printer/printer.h"
 #include "proof/conv_proof_generator.h"
 #include "smt/dump_manager.h"
@@ -80,6 +81,14 @@ NodeManager* Env::getNodeManager() const { return d_nodeManager; }
 
 ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
 
+bool Env::isTheoryProofProducing() const
+{
+  return d_proofNodeManager != nullptr
+         && (!d_options.smt.unsatCores
+             || d_options.smt.unsatCoresMode
+                    == options::UnsatCoresMode::FULL_PROOF);
+}
+
 theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
 
 theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions()