Merge branch 'master' into stdAttrsstdAttrs

1 files changed, 10 insertions, 10 deletions

diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 27dcf651b..d3372a28e 100644
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -180,7 +180,7 @@ Node HoElim::eliminateHo(Node n)
       if (cur.isVar())
       {
         Node ret = cur;
-        if (options::hoElim())
+        if (options().quantifiers.hoElim)
         {
           if (tn.isFunction())
           {
@@ -203,7 +203,7 @@ Node HoElim::eliminateHo(Node n)
       else
       {
         d_visited[cur] = Node::null();
-        if (cur.getKind() == APPLY_UF && options::hoElim())
+        if (cur.getKind() == APPLY_UF && options().quantifiers.hoElim)
         {
           Node op = cur.getOperator();
           // convert apply uf with variable arguments eagerly to ho apply
@@ -275,7 +275,7 @@ Node HoElim::eliminateHo(Node n)
           children.insert(children.begin(), retOp);
         }
         // process ho apply
-        if (ret.getKind() == HO_APPLY && options::hoElim())
+        if (ret.getKind() == HO_APPLY && options().quantifiers.hoElim)
         {
           TypeNode tnr = ret.getType();
           tnr = getUSort(tnr);
@@ -315,7 +315,7 @@ PreprocessingPassResult HoElim::applyInternal(
     Node res = eliminateLambdaComplete(prev, newLambda);
     if (res != prev)
     {
-      res = theory::Rewriter::rewrite(res);
+      res = rewrite(res);
       Assert(!expr::hasFreeVar(res));
       assertionsToPreprocess->replace(i, res);
     }
@@ -361,7 +361,7 @@ PreprocessingPassResult HoElim::applyInternal(
   if (!axioms.empty())
   {
     Node conj = nm->mkAnd(axioms);
-    conj = theory::Rewriter::rewrite(conj);
+    conj = rewrite(conj);
     Assert(!expr::hasFreeVar(conj));
     assertionsToPreprocess->conjoin(0, conj);
   }
@@ -374,7 +374,7 @@ PreprocessingPassResult HoElim::applyInternal(
     Node res = eliminateHo(prev);
     if (res != prev)
     {
-      res = theory::Rewriter::rewrite(res);
+      res = rewrite(res);
       Assert(!expr::hasFreeVar(res));
       assertionsToPreprocess->replace(i, res);
     }
@@ -382,7 +382,7 @@ PreprocessingPassResult HoElim::applyInternal(
   // extensionality: process all function types
   for (const TypeNode& ftn : d_funTypes)
   {
-    if (options::hoElim())
+    if (options().quantifiers.hoElim)
     {
       Node h = getHoApplyUf(ftn);
       Trace("ho-elim-ax") << "Make extensionality for " << h << std::endl;
@@ -406,7 +406,7 @@ PreprocessingPassResult HoElim::applyInternal(
       // exists another function that acts like the "store" operator for
       // arrays, e.g. it is the same function with one I/O pair updated.
       // Without this axiom, the translation is model unsound.
-      if (options::hoElimStoreAx())
+      if (options().quantifiers.hoElimStoreAx)
       {
         Node u = nm->mkBoundVar("u", uf);
         Node v = nm->mkBoundVar("v", uf);
@@ -428,7 +428,7 @@ PreprocessingPassResult HoElim::applyInternal(
         Trace("ho-elim-ax") << "...store axiom : " << store << std::endl;
       }
     }
-    else if (options::hoElimStoreAx())
+    else if (options().quantifiers.hoElimStoreAx)
     {
       Node u = nm->mkBoundVar("u", ftn);
       Node v = nm->mkBoundVar("v", ftn);
@@ -456,7 +456,7 @@ PreprocessingPassResult HoElim::applyInternal(
   if (!axioms.empty())
   {
     Node conj = nm->mkAnd(axioms);
-    conj = theory::Rewriter::rewrite(conj);
+    conj = rewrite(conj);
     Assert(!expr::hasFreeVar(conj));
     assertionsToPreprocess->conjoin(0, conj);
   }