Add skeleton of the FP theory solver (#1130)

This commit adds the skeleton of the theory solver using a dummy version of the converter (fp_converter.{h,cpp}). The converter is a class that is used to produce bit-vector expressions equivalent to floating-point ones. The commit sets up the equality engine and the infrastructure for interacting with the main theory components. The majority of this code is still agnostic to how the conversion is actually implemented / what kind of theory solver this is. This is pretty much the template code you need to write any kind of theory solver. This includes equality reasoning and so should be able to solve some basic problems.

1 files changed, 55 insertions, 0 deletions

diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
new file mode 100644
index 000000000..8a054e03a
--- /dev/null
+++ b/src/theory/fp/fp_converter.h
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file fp_converter.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Martin Brain
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Converts floating-point nodes to bit-vector expressions.
+ **
+ ** Uses the symfpu library to convert from floating-point operations to
+ ** bit-vectors and propositions allowing the theory to be solved by
+ ** 'bit-blasting'.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__FP_CONVERTER_H
+#define __CVC4__THEORY__FP__FP_CONVERTER_H
+
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "theory/valuation.h"
+#include "util/floatingpoint.h"
+#include "util/hash.h"
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction,
+                         TypeNodeHashFunction>
+    PairTypeNodeHashFunction;
+
+class FpConverter {
+ 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
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__FP__THEORY_FP_H */