src/theory/fp/fp_converter.h

   1 /*********************                                                        */
   2 /*! \file fp_converter.h
   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 Converts floating-point nodes to bit-vector expressions.
  13  **
  14  ** Uses the symfpu library to convert from floating-point operations to
  15  ** bit-vectors and propositions allowing the theory to be solved by
  16  ** 'bit-blasting'.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__FP__FP_CONVERTER_H
  22 #define __CVC4__THEORY__FP__FP_CONVERTER_H
  23
  24 #include "context/cdhashmap.h"
  25 #include "context/cdlist.h"
  26 #include "theory/valuation.h"
  27 #include "util/floatingpoint.h"
  28 #include "util/hash.h"
  29
  30 namespace CVC4 {
  31 namespace theory {
  32 namespace fp {
  33
  34 typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction,
  35                          TypeNodeHashFunction>
  36     PairTypeNodeHashFunction;
  37
  38 class FpConverter {
  39  public:
  40   context::CDList<Node> d_additionalAssertions;
  41
  42   FpConverter(context::UserContext *);
  43
  44   /** Adds a node to the conversion, returns the converted node */
  45   Node convert(TNode);
  46
  47   /** Gives the node representing the value of a given variable */
  48   Node getValue(Valuation &, TNode);
  49 };
  50
  51 }  // namespace fp
  52 }  // namespace theory
  53 }  // namespace CVC4
  54
  55 #endif /* __CVC4__THEORY__FP__THEORY_FP_H */