diff options
Diffstat (limited to 'src/theory/arith/nl/cad/cdcac.cpp')
| -rw-r--r-- | src/theory/arith/nl/cad/cdcac.cpp | 9 |
1 files changed, 4 insertions, 5 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); |