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.

1 files changed, 16 insertions, 15 deletions

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