Added simplifier plugin for FP

src/ast/simplifier/fpa_simplifier_plugin.cpp

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    fpa_simplifier_plugin.cpp
+
+Abstract:
+
+    Simplifier for the floating-point theory
+
+Author:
+
+    Christoph (cwinter) 2015-01-14
+
+--*/
+#include"fpa_simplifier_plugin.h"
+
+fpa_simplifier_plugin::fpa_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b) :
+simplifier_plugin(symbol("fpa"), m),
+m_util(m),
+m_bsimp(b),
+m_rw(m) {}
+
+fpa_simplifier_plugin::~fpa_simplifier_plugin() {}
+
+bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    set_reduce_invoked();    
+
+    SASSERT(f->get_family_id() == get_family_id());
+    /*switch (f->get_decl_kind()) {
+    case OP_FPA_FP: break;
+    }*/    
+
+    return m_rw.mk_app_core(f, num_args, args, result) == BR_DONE;
+}
+
+bool fpa_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
+    set_reduce_invoked();
+
+    return m_rw.mk_eq_core(lhs, rhs, result) == BR_DONE;
+}
+

src/ast/simplifier/fpa_simplifier_plugin.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    fpa_simplifier_plugin.h
+
+Abstract:
+
+    Simplifier for the floating-point theory
+
+Author:
+
+    Christoph (cwinter) 2015-01-14
+
+--*/
+#ifndef _FPA_SIMPLIFIER_PLUGIN_H_
+#define _FPA_SIMPLIFIER_PLUGIN_H_
+
+#include"basic_simplifier_plugin.h"
+#include"fpa_decl_plugin.h"
+#include"fpa_rewriter.h"
+
+class fpa_simplifier_plugin : public simplifier_plugin {
+    fpa_util                  m_util;
+    basic_simplifier_plugin & m_bsimp;
+    fpa_rewriter              m_rw;
+
+public:
+    fpa_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b);
+    ~fpa_simplifier_plugin();
+
+
+    virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+
+    virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
+
+};
+
+#endif /* _FPA_SIMPLIFIER_PLUGIN_H_ */