Merge branch 'master' into stdAttrsstdAttrs

2 files changed, 6 insertions, 9 deletions

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index 9b37a135f..9b7678388 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -23,7 +23,7 @@
 #include "theory/arith/nl/cad/projections.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
 #include "theory/arith/nl/nl_model.h"
-#include "theory/quantifiers/extended_rewrite.h"
+#include "theory/rewriter.h"
 
 namespace std {
 /** Generic streaming operator for std::vector. */
@@ -42,7 +42,7 @@ namespace nl {
 namespace cad {
 
 CDCAC::CDCAC(Env& env, const std::vector<poly::Variable>& ordering)
-    : d_env(env), d_variableOrdering(ordering)
+    : EnvObj(env), d_variableOrdering(ordering)
 {
   if (d_env.isTheoryProofProducing())
   {
@@ -276,9 +276,8 @@ PolyVector requiredCoefficientsLazardModified(
         Kind::EQUAL, nl::as_cvc_polynomial(coeff, vm), zero));
   }
   // if phi is false (i.e. p can not vanish)
-  quantifiers::ExtendedRewriter rew;
-  Node rewritten =
-      rew.extendedRewrite(NodeManager::currentNM()->mkAnd(conditions));
+  Node rewritten = Rewriter::callExtendedRewrite(
+      NodeManager::currentNM()->mkAnd(conditions));
   if (rewritten.isConst())
   {
     Assert(rewritten.getKind() == Kind::CONST_BOOLEAN);
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index b504998d8..be72e4063 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -26,6 +26,7 @@
 #include <vector>
 
 #include "smt/env.h"
+#include "smt/env_obj.h"
 #include "theory/arith/nl/cad/cdcac_utils.h"
 #include "theory/arith/nl/cad/constraints.h"
 #include "theory/arith/nl/cad/proof_generator.h"
@@ -44,7 +45,7 @@ namespace cad {
  * This class implements Cylindrical Algebraic Coverings as presented in
  * https://arxiv.org/pdf/2003.05633.pdf
  */
-class CDCAC
+class CDCAC : protected EnvObj
 {
  public:
   /** Initialize this method with the given variable ordering. */
@@ -184,9 +185,6 @@ class CDCAC
    */
   void pruneRedundantIntervals(std::vector<CACInterval>& intervals);
 
-  /** A reference to the environment */
-  Env& d_env;
-
   /**
    * The current assignment. When the method terminates with SAT, it contains a
    * model for the input constraints.