fp_converter: Properly separate out symbolic glue code. (#5501)

File fp_converter.h encapsulates the symbolic glue code for symFPU and
implements the actual word-blaster (class FpConverter).
This header should not be included in any other headers in order to no
pull in symFPU headers where it's not needed. However, it was included
in src/theory/fp/theory_fp.h.

This properly separates it out and does some clean up in TheoryFP, which
still needs more love to conform to code style guidelines, and also
more documentation. More love and documentation is postponed to future
PRs to make reviewing easier.

4 files changed, 85 insertions, 74 deletions

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 85482bf6d..858710746 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -755,18 +755,20 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const
 }
 
 FpConverter::FpConverter(context::UserContext* user)
-    :
+    : d_additionalAssertions(user)
 #ifdef CVC4_USE_SYMFPU
+      ,
       d_fpMap(user),
       d_rmMap(user),
       d_boolMap(user),
       d_ubvMap(user),
-      d_sbvMap(user),
+      d_sbvMap(user)
 #endif
-      d_additionalAssertions(user)
 {
 }
 
+FpConverter::~FpConverter() {}
+
 #ifdef CVC4_USE_SYMFPU
 Node FpConverter::ufToNode(const fpt &format, const uf &u) const
 {
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index e48d651bd..6688e8607 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -14,6 +14,8 @@
  ** Uses the symfpu library to convert from floating-point operations to
  ** bit-vectors and propositions allowing the theory to be solved by
  ** 'bit-blasting'.
+ **
+ ** !!! This header is not to be included in any other headers !!!
  **/
 
 #include "cvc4_private.h"
@@ -49,10 +51,6 @@ namespace CVC4 {
 namespace theory {
 namespace fp {
 
-typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction,
-                         TypeNodeHashFunction>
-    PairTypeNodeHashFunction;
-
 /**
  * This is a symfpu symbolic "back-end".  It allows the library to be used to
  * construct bit-vector expressions that compute floating-point operations.
@@ -302,6 +300,20 @@ class floatingPointTypeInfo : public FloatingPointSize
  */
 class FpConverter
 {
+ public:
+  /** Constructor. */
+  FpConverter(context::UserContext*);
+  /** Destructor. */
+  ~FpConverter();
+
+  /** Adds a node to the conversion, returns the converted node */
+  Node convert(TNode);
+
+  /** Gives the node representing the value of a given variable */
+  Node getValue(Valuation&, TNode);
+
+  context::CDList<Node> d_additionalAssertions;
+
  protected:
 #ifdef CVC4_USE_SYMFPU
   typedef symfpuSymbolic::traits traits;
@@ -338,17 +350,6 @@ class FpConverter
   /* Creates the relevant components for a variable */
   uf buildComponents(TNode current);
 #endif
-
- public:
-  context::CDList<Node> d_additionalAssertions;
-
-  FpConverter(context::UserContext *);
-
-  /** Adds a node to the conversion, returns the converted node */
-  Node convert(TNode);
-
-  /** Gives the node representing the value of a given variable */
-  Node getValue(Valuation &, TNode);
 };
 
 }  // namespace fp
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 0b15486e2..01fab92c8 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "options/fp_options.h"
+#include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -108,7 +109,7 @@ TheoryFp::TheoryFp(context::Context* c,
     : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
       d_notification(*this),
       d_registeredTerms(u),
-      d_conv(u),
+      d_conv(new FpConverter(u)),
       d_expansionRequested(false),
       d_conflictNode(c, Node::null()),
       d_minMap(u),
@@ -116,9 +117,9 @@ TheoryFp::TheoryFp(context::Context* c,
       d_toUBVMap(u),
       d_toSBVMap(u),
       d_toRealMap(u),
-      realToFloatMap(u),
-      floatToRealMap(u),
-      abstractionMap(u),
+      d_realToFloatMap(u),
+      d_floatToRealMap(u),
+      d_abstractionMap(u),
       d_state(c, u, valuation)
 {
   // indicate we are using the default theory state object
@@ -341,10 +342,10 @@ Node TheoryFp::abstractRealToFloat(Node node)
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
-  ComparisonUFMap::const_iterator i(realToFloatMap.find(t));
+  ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t));
 
   Node fun;
-  if (i == realToFloatMap.end())
+  if (i == d_realToFloatMap.end())
   {
     std::vector<TypeNode> args(2);
     args[0] = node[0].getType();
@@ -353,7 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
                        nm->mkFunctionType(args, node.getType()),
                        "floatingpoint_abstract_real_to_float",
                        NodeManager::SKOLEM_EXACT_NAME);
-    realToFloatMap.insert(t, fun);
+    d_realToFloatMap.insert(t, fun);
   }
   else
   {
@@ -361,7 +362,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
   }
   Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
 
-  abstractionMap.insert(uf, node);
+  d_abstractionMap.insert(uf, node);
 
   return uf;
 }
@@ -373,10 +374,10 @@ Node TheoryFp::abstractFloatToReal(Node node)
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
-  ComparisonUFMap::const_iterator i(floatToRealMap.find(t));
+  ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t));
 
   Node fun;
-  if (i == floatToRealMap.end())
+  if (i == d_floatToRealMap.end())
   {
     std::vector<TypeNode> args(2);
     args[0] = t;
@@ -385,7 +386,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
                        nm->mkFunctionType(args, nm->realType()),
                        "floatingpoint_abstract_float_to_real",
                        NodeManager::SKOLEM_EXACT_NAME);
-    floatToRealMap.insert(t, fun);
+    d_floatToRealMap.insert(t, fun);
   }
   else
   {
@@ -393,7 +394,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
   }
   Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
 
-  abstractionMap.insert(uf, node);
+  d_abstractionMap.insert(uf, node);
 
   return uf;
 }
@@ -737,9 +738,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
 
 void TheoryFp::convertAndEquateTerm(TNode node) {
   Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
-  size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size();
+  size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size();
 
-  Node converted(d_conv.convert(node));
+  Node converted(d_conv->convert(node));
 
   if (converted != node) {
     Debug("fp-convertTerm")
@@ -748,11 +749,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
         << "TheoryFp::convertTerm(): after  " << converted << std::endl;
   }
 
-  size_t newAdditionalAssertions = d_conv.d_additionalAssertions.size();
+  size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size();
   Assert(oldAdditionalAssertions <= newAdditionalAssertions);
 
   while (oldAdditionalAssertions < newAdditionalAssertions) {
-    Node addA = d_conv.d_additionalAssertions[oldAdditionalAssertions];
+    Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions];
 
     Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion  "
                             << addA << std::endl;
@@ -953,8 +954,8 @@ void TheoryFp::postCheck(Effort level)
     TheoryModel* m = getValuation().getModel();
     bool lemmaAdded = false;
 
-    for (abstractionMapType::const_iterator i = abstractionMap.begin();
-         i != abstractionMap.end();
+    for (AbstractionMap::const_iterator i = d_abstractionMap.begin();
+         i != d_abstractionMap.end();
          ++i)
     {
       if (m->hasTerm((*i).first))
@@ -1016,7 +1017,7 @@ TrustNode TheoryFp::explain(TNode n)
 }
 
 Node TheoryFp::getModelValue(TNode var) {
-  return d_conv.getValue(d_valuation, var);
+  return d_conv->getValue(d_valuation, var);
 }
 
 bool TheoryFp::collectModelInfo(TheoryModel* m,
@@ -1069,14 +1070,16 @@ bool TheoryFp::collectModelValues(TheoryModel* m,
   }
 
   for (std::set<TNode>::const_iterator i(relevantVariables.begin());
-       i != relevantVariables.end(); ++i) {
+       i != relevantVariables.end();
+       ++i)
+  {
     TNode node = *i;
 
     Trace("fp-collectModelInfo")
         << "TheoryFp::collectModelInfo(): relevantVariable " << node
         << std::endl;
 
-    if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true))
+    if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true))
     {
       return false;
     }
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 42c009893..fe91a39bd 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -24,7 +24,6 @@
 #include <utility>
 
 #include "context/cdo.h"
-#include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -33,7 +32,10 @@ namespace CVC4 {
 namespace theory {
 namespace fp {
 
-class TheoryFp : public Theory {
+class FpConverter;
+
+class TheoryFp : public Theory
+{
  public:
   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
   TheoryFp(context::Context* c,
@@ -42,8 +44,9 @@ class TheoryFp : public Theory {
            Valuation valuation,
            const LogicInfo& logicInfo,
            ProofNodeManager* pnm = nullptr);
+
   //--------------------------------- initialization
-  /** get the official theory rewriter of this theory */
+  /** Get the official theory rewriter of this theory. */
   TheoryRewriter* getTheoryRewriter() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
@@ -51,7 +54,7 @@ class TheoryFp : public Theory {
    * documentation in Theory::needsEqualityEngine.
    */
   bool needsEqualityEngine(EeSetupInfo& esi) override;
-  /** finish initialization */
+  /** Finish initialization. */
   void finishInit() override;
   //--------------------------------- end initialization
 
@@ -77,8 +80,10 @@ class TheoryFp : public Theory {
   Node getModelValue(TNode var) override;
   bool collectModelInfo(TheoryModel* m,
                         const std::set<Node>& relevantTerms) override;
-  /** Collect model values in m based on the relevant terms given by
-   * relevantTerms */
+  /**
+   * Collect model values in m based on the relevant terms given by
+   * relevantTerms.
+   */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& relevantTerms) override;
 
@@ -87,7 +92,20 @@ class TheoryFp : public Theory {
   TrustNode explain(TNode n) override;
 
  protected:
-  /** Equality engine */
+  using PairTypeNodeHashFunction = PairHashFunction<TypeNode,
+                                                    TypeNode,
+                                                    TypeNodeHashFunction,
+                                                    TypeNodeHashFunction>;
+  /** Uninterpreted functions for undefined cases of non-total operators. */
+  using ComparisonUFMap =
+      context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
+  /** Uninterpreted functions for lazy handling of conversions. */
+  using ConversionUFMap = context::
+      CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>;
+  using ConversionAbstractionMap = ComparisonUFMap;
+  using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+
+  /** Equality engine. */
   class NotifyClass : public eq::EqualityEngineNotify {
    protected:
     TheoryFp& d_theorySolver;
@@ -108,14 +126,15 @@ class TheoryFp : public Theory {
 
   NotifyClass d_notification;
 
-  /** General utility **/
+  /** General utility. */
   void registerTerm(TNode node);
   bool isRegistered(TNode node);
 
   context::CDHashSet<Node, NodeHashFunction> d_registeredTerms;
 
-  /** Bit-blasting conversion */
-  FpConverter d_conv;
+  /** The word-blaster. Translates FP -> BV. */
+  std::unique_ptr<FpConverter> d_conv;
+
   bool d_expansionRequested;
 
   void convertAndEquateTerm(TNode node);
@@ -133,44 +152,30 @@ class TheoryFp : public Theory {
    */
   void conflictEqConstantMerge(TNode t1, TNode t2);
 
-  context::CDO<Node> d_conflictNode;
-
-  typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>
-      ComparisonUFMap;
-
-  ComparisonUFMap d_minMap;
-  ComparisonUFMap d_maxMap;
+  bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
 
   Node minUF(Node);
   Node maxUF(Node);
 
-  typedef context::CDHashMap<std::pair<TypeNode, TypeNode>, Node,
-                             PairTypeNodeHashFunction>
-      ConversionUFMap;
-
-  ConversionUFMap d_toUBVMap;
-  ConversionUFMap d_toSBVMap;
-
   Node toUBVUF(Node);
   Node toSBVUF(Node);
 
-  ComparisonUFMap d_toRealMap;
-
   Node toRealUF(Node);
 
-  /** Uninterpretted functions for lazy handling of conversions */
-  typedef ComparisonUFMap conversionAbstractionMap;
-
-  conversionAbstractionMap realToFloatMap;
-  conversionAbstractionMap floatToRealMap;
-
   Node abstractRealToFloat(Node);
   Node abstractFloatToReal(Node);
 
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> abstractionMapType;
-  abstractionMapType abstractionMap;  // abstract -> original
+ private:
+  context::CDO<Node> d_conflictNode;
 
-  bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
+  ComparisonUFMap d_minMap;
+  ComparisonUFMap d_maxMap;
+  ConversionUFMap d_toUBVMap;
+  ConversionUFMap d_toSBVMap;
+  ComparisonUFMap d_toRealMap;
+  ConversionAbstractionMap d_realToFloatMap;
+  ConversionAbstractionMap d_floatToRealMap;
+  AbstractionMap d_abstractionMap;  // abstract -> original
 
   /** The theory rewriter for this theory. */
   TheoryFpRewriter d_rewriter;