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, 38 insertions, 0 deletions

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
new file mode 100644
index 000000000..6ce2195cb
--- /dev/null
+++ b/src/theory/fp/fp_converter.cpp
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file fp_converter.cpp
+ ** \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 Conversion of floating-point operations to bit-vectors using symfpu.
+ **/
+
+#include "theory/fp/fp_converter.h"
+
+#include <stack>
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+FpConverter::FpConverter(context::UserContext *user)
+    : d_additionalAssertions(user) {}
+
+Node FpConverter::convert(TNode node) {
+  Unimplemented("Conversion not implemented.");
+  return node;
+}
+
+Node FpConverter::getValue(Valuation &val, TNode var) {
+  Unimplemented("Conversion not implemented.");
+  return Node::null();
+}
+
+}  // namespace fp
+}  // namespace theory
+}  // namespace CVC4