src/theory/fp/fp_converter.cpp

   1 /*********************                                                        */
   2 /*! \file fp_converter.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Martin Brain
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Conversion of floating-point operations to bit-vectors using symfpu.
  13  **/
  14
  15 #include "theory/fp/fp_converter.h"
  16
  17 #include <stack>
  18
  19 namespace CVC4 {
  20 namespace theory {
  21 namespace fp {
  22
  23 FpConverter::FpConverter(context::UserContext *user)
  24     : d_additionalAssertions(user) {}
  25
  26 Node FpConverter::convert(TNode node) {
  27   Unimplemented("Conversion not implemented.");
  28 }
  29
  30 Node FpConverter::getValue(Valuation &val, TNode var) {
  31   Unimplemented("Conversion not implemented.");
  32 }
  33
  34 }  // namespace fp
  35 }  // namespace theory
  36 }  // namespace CVC4