src/theory/fp/fp_converter.h

   1 /*********************                                                        */
   2 /*! \file fp_converter.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Martin Brain, Mathias Preiner, Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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  ** !!! This header is not to be included in any other headers !!!
  19  **/
  20
  21 #include "cvc4_private.h"
  22
  23 #ifndef CVC4__THEORY__FP__FP_CONVERTER_H
  24 #define CVC4__THEORY__FP__FP_CONVERTER_H
  25
  26 #include "base/check.h"
  27 #include "context/cdhashmap.h"
  28 #include "context/cdlist.h"
  29 #include "expr/node.h"
  30 #include "expr/node_builder.h"
  31 #include "expr/type_node.h"
  32 #include "theory/valuation.h"
  33 #include "util/bitvector.h"
  34 #include "util/floatingpoint_size.h"
  35 #include "util/hash.h"
  36
  37 #ifdef CVC4_USE_SYMFPU
  38 #include "symfpu/core/unpackedFloat.h"
  39 #endif
  40
  41 #ifdef CVC4_SYM_SYMBOLIC_EVAL
  42 // This allows debugging of the CVC4 symbolic back-end.
  43 // By enabling this and disabling constant folding in the rewriter,
  44 // SMT files that have operations on constants will be evaluated
  45 // during the encoding step, which means that the expressions
  46 // generated by the symbolic back-end can be debugged with gdb.
  47 #include "theory/rewriter.h"
  48 #endif
  49
  50 namespace CVC4 {
  51 namespace theory {
  52 namespace fp {
  53
  54 /**
  55  * This is a symfpu symbolic "back-end".  It allows the library to be used to
  56  * construct bit-vector expressions that compute floating-point operations.
  57  * This is effectively the glue between symfpu's notion of "signed bit-vector"
  58  * and CVC4's node.
  59  */
  60 namespace symfpuSymbolic {
  61
  62 // Forward declarations of the wrapped types so that traits can be defined early
  63 // and used in the implementations
  64 class symbolicRoundingMode;
  65 class floatingPointTypeInfo;
  66 class symbolicProposition;
  67 template <bool T>
  68 class symbolicBitVector;
  69
  70 // This is the template parameter for symfpu's templates.
  71 class traits
  72 {
  73  public:
  74   // The six key types that symfpu uses.
  75   typedef unsigned bwt;
  76   typedef symbolicRoundingMode rm;
  77   typedef floatingPointTypeInfo fpt;
  78   typedef symbolicProposition prop;
  79   typedef symbolicBitVector<true> sbv;
  80   typedef symbolicBitVector<false> ubv;
  81
  82   // Give concrete instances (wrapped nodes) for each rounding mode.
  83   static symbolicRoundingMode RNE(void);
  84   static symbolicRoundingMode RNA(void);
  85   static symbolicRoundingMode RTP(void);
  86   static symbolicRoundingMode RTN(void);
  87   static symbolicRoundingMode RTZ(void);
  88
  89   // Properties used by symfpu
  90   static void precondition(const bool b);
  91   static void postcondition(const bool b);
  92   static void invariant(const bool b);
  93   static void precondition(const prop &p);
  94   static void postcondition(const prop &p);
  95   static void invariant(const prop &p);
  96 };
  97
  98 // Use the same type names as symfpu.
  99 typedef traits::bwt bwt;
 100
 101 /**
 102  * Wrap the CVC4::Node types so that we can debug issues with this back-end
 103  */
 104 class nodeWrapper : public Node
 105 {
 106  protected:
 107 /* CVC4_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues.
 108  * Enable this and disabling constant folding will mean that operations
 109  * that are input with constant args are 'folded' using the symbolic encoding
 110  * allowing them to be traced via GDB.
 111  */
 112 #ifdef CVC4_SYM_SYMBOLIC_EVAL
 113   nodeWrapper(const Node &n) : Node(theory::Rewriter::rewrite(n)) {}
 114 #else
 115   nodeWrapper(const Node &n) : Node(n) {}
 116 #endif
 117 };
 118
 119 class symbolicProposition : public nodeWrapper
 120 {
 121  protected:
 122   bool checkNodeType(const TNode node);
 123
 124 #ifdef CVC4_USE_SYMFPU
 125   friend ::symfpu::ite<symbolicProposition, symbolicProposition>;  // For ITE
 126 #endif
 127
 128  public:
 129   symbolicProposition(const Node n);
 130   symbolicProposition(bool v);
 131   symbolicProposition(const symbolicProposition &old);
 132
 133   symbolicProposition operator!(void)const;
 134   symbolicProposition operator&&(const symbolicProposition &op) const;
 135   symbolicProposition operator||(const symbolicProposition &op) const;
 136   symbolicProposition operator==(const symbolicProposition &op) const;
 137   symbolicProposition operator^(const symbolicProposition &op) const;
 138 };
 139
 140 class symbolicRoundingMode : public nodeWrapper
 141 {
 142  protected:
 143   bool checkNodeType(const TNode n);
 144
 145 #ifdef CVC4_USE_SYMFPU
 146   friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>;  // For ITE
 147 #endif
 148
 149  public:
 150   symbolicRoundingMode(const Node n);
 151   symbolicRoundingMode(const unsigned v);
 152   symbolicRoundingMode(const symbolicRoundingMode &old);
 153
 154   symbolicProposition valid(void) const;
 155   symbolicProposition operator==(const symbolicRoundingMode &op) const;
 156 };
 157
 158 // Type function for mapping between types
 159 template <bool T>
 160 struct signedToLiteralType;
 161
 162 template <>
 163 struct signedToLiteralType<true>
 164 {
 165   typedef int literalType;
 166 };
 167 template <>
 168 struct signedToLiteralType<false>
 169 {
 170   typedef unsigned int literalType;
 171 };
 172
 173 template <bool isSigned>
 174 class symbolicBitVector : public nodeWrapper
 175 {
 176  protected:
 177   typedef typename signedToLiteralType<isSigned>::literalType literalType;
 178
 179   Node boolNodeToBV(Node node) const;
 180   Node BVToBoolNode(Node node) const;
 181
 182   Node fromProposition(Node node) const;
 183   Node toProposition(Node node) const;
 184   bool checkNodeType(const TNode n);
 185   friend symbolicBitVector<!isSigned>;  // To allow conversion between the types
 186
 187 #ifdef CVC4_USE_SYMFPU
 188   friend ::symfpu::ite<symbolicProposition,
 189                        symbolicBitVector<isSigned> >;  // For ITE
 190 #endif
 191
 192  public:
 193   symbolicBitVector(const Node n);
 194   symbolicBitVector(const bwt w, const unsigned v);
 195   symbolicBitVector(const symbolicProposition &p);
 196   symbolicBitVector(const symbolicBitVector<isSigned> &old);
 197   symbolicBitVector(const BitVector &old);
 198
 199   bwt getWidth(void) const;
 200
 201   /*** Constant creation and test ***/
 202   static symbolicBitVector<isSigned> one(const bwt &w);
 203   static symbolicBitVector<isSigned> zero(const bwt &w);
 204   static symbolicBitVector<isSigned> allOnes(const bwt &w);
 205
 206   symbolicProposition isAllOnes() const;
 207   symbolicProposition isAllZeros() const;
 208
 209   static symbolicBitVector<isSigned> maxValue(const bwt &w);
 210   static symbolicBitVector<isSigned> minValue(const bwt &w);
 211
 212   /*** Operators ***/
 213   symbolicBitVector<isSigned> operator<<(
 214       const symbolicBitVector<isSigned> &op) const;
 215   symbolicBitVector<isSigned> operator>>(
 216       const symbolicBitVector<isSigned> &op) const;
 217   symbolicBitVector<isSigned> operator|(
 218       const symbolicBitVector<isSigned> &op) const;
 219   symbolicBitVector<isSigned> operator&(
 220       const symbolicBitVector<isSigned> &op) const;
 221   symbolicBitVector<isSigned> operator+(
 222       const symbolicBitVector<isSigned> &op) const;
 223   symbolicBitVector<isSigned> operator-(
 224       const symbolicBitVector<isSigned> &op) const;
 225   symbolicBitVector<isSigned> operator*(
 226       const symbolicBitVector<isSigned> &op) const;
 227   symbolicBitVector<isSigned> operator/(
 228       const symbolicBitVector<isSigned> &op) const;
 229   symbolicBitVector<isSigned> operator%(
 230       const symbolicBitVector<isSigned> &op) const;
 231   symbolicBitVector<isSigned> operator-(void) const;
 232   symbolicBitVector<isSigned> operator~(void)const;
 233   symbolicBitVector<isSigned> increment() const;
 234   symbolicBitVector<isSigned> decrement() const;
 235   symbolicBitVector<isSigned> signExtendRightShift(
 236       const symbolicBitVector<isSigned> &op) const;
 237
 238   /*** Modular operations ***/
 239   // This back-end doesn't do any overflow checking so these are the same as
 240   // other operations
 241   symbolicBitVector<isSigned> modularLeftShift(
 242       const symbolicBitVector<isSigned> &op) const;
 243   symbolicBitVector<isSigned> modularRightShift(
 244       const symbolicBitVector<isSigned> &op) const;
 245   symbolicBitVector<isSigned> modularIncrement() const;
 246   symbolicBitVector<isSigned> modularDecrement() const;
 247   symbolicBitVector<isSigned> modularAdd(
 248       const symbolicBitVector<isSigned> &op) const;
 249   symbolicBitVector<isSigned> modularNegate() const;
 250
 251   /*** Comparisons ***/
 252   symbolicProposition operator==(const symbolicBitVector<isSigned> &op) const;
 253   symbolicProposition operator<=(const symbolicBitVector<isSigned> &op) const;
 254   symbolicProposition operator>=(const symbolicBitVector<isSigned> &op) const;
 255   symbolicProposition operator<(const symbolicBitVector<isSigned> &op) const;
 256   symbolicProposition operator>(const symbolicBitVector<isSigned> &op) const;
 257
 258   /*** Type conversion ***/
 259   // CVC4 nodes make no distinction between signed and unsigned, thus these are
 260   // trivial
 261   symbolicBitVector<true> toSigned(void) const;
 262   symbolicBitVector<false> toUnsigned(void) const;
 263
 264   /*** Bit hacks ***/
 265   symbolicBitVector<isSigned> extend(bwt extension) const;
 266   symbolicBitVector<isSigned> contract(bwt reduction) const;
 267   symbolicBitVector<isSigned> resize(bwt newSize) const;
 268   symbolicBitVector<isSigned> matchWidth(
 269       const symbolicBitVector<isSigned> &op) const;
 270   symbolicBitVector<isSigned> append(
 271       const symbolicBitVector<isSigned> &op) const;
 272
 273   // Inclusive of end points, thus if the same, extracts just one bit
 274   symbolicBitVector<isSigned> extract(bwt upper, bwt lower) const;
 275 };
 276
 277 // Use the same type information as the literal back-end but add an interface to
 278 // TypeNodes for convenience.
 279 class floatingPointTypeInfo : public FloatingPointSize
 280 {
 281  public:
 282   floatingPointTypeInfo(const TypeNode t);
 283   floatingPointTypeInfo(unsigned exp, unsigned sig);
 284   floatingPointTypeInfo(const floatingPointTypeInfo &old);
 285
 286   TypeNode getTypeNode(void) const;
 287 };
 288 }
 289
 290 /**
 291  * This class uses SymFPU to convert an expression containing floating-point
 292  * kinds and operations into a logically equivalent form with bit-vector
 293  * operations replacing the floating-point ones.  It also has a getValue method
 294  * to produce an expression which will reconstruct the value of the
 295  * floating-point terms from a valuation.
 296  *
 297  * Internally it caches all of the unpacked floats so that unnecessary packing
 298  * and unpacking operations are avoided and to make best use of structural
 299  * sharing.
 300  */
 301 class FpConverter
 302 {
 303  public:
 304   /** Constructor. */
 305   FpConverter(context::UserContext*);
 306   /** Destructor. */
 307   ~FpConverter();
 308
 309   /** Adds a node to the conversion, returns the converted node */
 310   Node convert(TNode);
 311
 312   /** Gives the node representing the value of a given variable */
 313   Node getValue(Valuation&, TNode);
 314
 315   context::CDList<Node> d_additionalAssertions;
 316
 317  protected:
 318 #ifdef CVC4_USE_SYMFPU
 319   typedef symfpuSymbolic::traits traits;
 320   typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf;
 321   typedef symfpuSymbolic::traits::rm rm;
 322   typedef symfpuSymbolic::traits::fpt fpt;
 323   typedef symfpuSymbolic::traits::prop prop;
 324   typedef symfpuSymbolic::traits::ubv ubv;
 325   typedef symfpuSymbolic::traits::sbv sbv;
 326
 327   typedef context::CDHashMap<Node, uf, NodeHashFunction> fpMap;
 328   typedef context::CDHashMap<Node, rm, NodeHashFunction> rmMap;
 329   typedef context::CDHashMap<Node, prop, NodeHashFunction> boolMap;
 330   typedef context::CDHashMap<Node, ubv, NodeHashFunction> ubvMap;
 331   typedef context::CDHashMap<Node, sbv, NodeHashFunction> sbvMap;
 332
 333   fpMap d_fpMap;
 334   rmMap d_rmMap;
 335   boolMap d_boolMap;
 336   ubvMap d_ubvMap;
 337   sbvMap d_sbvMap;
 338
 339   /* These functions take a symfpu object and convert it to a node.
 340    * These should ensure that constant folding it will give a
 341    * constant of the right type.
 342    */
 343
 344   Node ufToNode(const fpt &, const uf &) const;
 345   Node rmToNode(const rm &) const;
 346   Node propToNode(const prop &) const;
 347   Node ubvToNode(const ubv &) const;
 348   Node sbvToNode(const sbv &) const;
 349
 350   /* Creates the relevant components for a variable */
 351   uf buildComponents(TNode current);
 352 #endif
 353 };
 354
 355 }  // namespace fp
 356 }  // namespace theory
 357 }  // namespace CVC4
 358
 359 #endif /* CVC4__THEORY__FP__THEORY_FP_H */