FP: Use EnvObj::rewrite() and options() in theory_fp. (#7169)

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 075a6633f695f9146b6a2c639b4a96bd2b216745..5e0752f0dd2ea11b0811442eb7da6a2fbe09bed1 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -27,7 +27,6 @@
 #include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/output_channel.h"
-#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 #include "util/floatingpoint.h"
 
@@ -313,7 +312,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
 
     Node evaluate =
         nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, floatValue, undefValue);
-    Node concreteValue = Rewriter::rewrite(evaluate);
+    Node concreteValue = rewrite(evaluate);
     Assert(concreteValue.isConst());
 
     Trace("fp-refineAbstraction")
@@ -359,7 +358,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
       handleLemma(fl, InferenceId::FP_PREPROCESS);
 
       // Then the backwards constraints
-      Node floatAboveAbstract = Rewriter::rewrite(
+      Node floatAboveAbstract = rewrite(
           nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
                      nm->mkConst(FloatingPointToFPReal(
                          concrete[0].getType().getConst<FloatingPointSize>())),
@@ -376,7 +375,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
               nm->mkNode(kind::GEQ, abstract, abstractValue)));
       handleLemma(bg, InferenceId::FP_PREPROCESS);
 
-      Node floatBelowAbstract = Rewriter::rewrite(
+      Node floatBelowAbstract = rewrite(
           nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
                      nm->mkConst(FloatingPointToFPReal(
                          concrete[0].getType().getConst<FloatingPointSize>())),
@@ -429,7 +428,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
                        concrete.getType().getConst<FloatingPointSize>())),
                    rmValue,
                    realValue);
-    Node concreteValue = Rewriter::rewrite(evaluate);
+    Node concreteValue = rewrite(evaluate);
     Assert(concreteValue.isConst());
 
     Trace("fp-refineAbstraction")
@@ -473,9 +472,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
       if (!abstractValue.getConst<FloatingPoint>().isInfinite())
       {
         Node realValueOfAbstract =
-            Rewriter::rewrite(nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
-                                         abstractValue,
-                                         nm->mkConst(Rational(0U))));
+            rewrite(nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
+                               abstractValue,
+                               nm->mkConst(Rational(0U))));
 
         Node bg = nm->mkNode(
             kind::IMPLIES,
@@ -656,7 +655,7 @@ void TheoryFp::registerTerm(TNode node)
 
     /* When not word-blasting lazier, we word-blast every term on
      * registration. */
-    if (!options::fpLazyWb())
+    if (!options().fp.fpLazyWb)
     {
       convertAndEquateTerm(node);
     }
@@ -671,7 +670,7 @@ bool TheoryFp::isRegistered(TNode node)
 
 void TheoryFp::preRegisterTerm(TNode node)
 {
-  if (!options::fpExp())
+  if (!options().fp.fpExp)
   {
     TypeNode tn = node.getType();
     if (tn.isFloatingPoint())
@@ -757,7 +756,8 @@ bool TheoryFp::preNotifyFact(
     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 {
   /* Word-blast lazier if configured. */
-  if (options::fpLazyWb() && d_wbFactsCache.find(atom) == d_wbFactsCache.end())
+  if (options().fp.fpLazyWb
+      && d_wbFactsCache.find(atom) == d_wbFactsCache.end())
   {
     d_wbFactsCache.insert(atom);
     convertAndEquateTerm(atom);
@@ -790,7 +790,7 @@ bool TheoryFp::preNotifyFact(
 void TheoryFp::notifySharedTerm(TNode n)
 {
   /* Word-blast lazier if configured. */
-  if (options::fpLazyWb() && d_wbFactsCache.find(n) == d_wbFactsCache.end())
+  if (options().fp.fpLazyWb && d_wbFactsCache.find(n) == d_wbFactsCache.end())
   {
     d_wbFactsCache.insert(n);
     convertAndEquateTerm(n);