abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
epd.h File Reference

Go to the source code of this file.

Data Structures

struct  IeeeDoubleStruct
 
struct  IeeeNanStruct
 
union  EpTypeUnion
 
struct  EpDoubleStruct
 

Macros

#define EPD_MAX_BIN   1023
 
#define EPD_MAX_DEC   308
 
#define EPD_EXP_INF   0x7ff
 

Typedefs

typedef struct EpDoubleStruct EpDouble
 
typedef struct IeeeDoubleStruct IeeeDouble
 
typedef struct IeeeNanStruct IeeeNan
 
typedef union EpTypeUnion EpType
 

Functions

EpDoubleEpdAlloc (void)
 
int EpdCmp (const char *key1, const char *key2)
 
void EpdFree (EpDouble *epd)
 
void EpdGetString (EpDouble *epd, char *str)
 
void EpdConvert (double value, EpDouble *epd)
 
void EpdMultiply (EpDouble *epd1, double value)
 
void EpdMultiply2 (EpDouble *epd1, EpDouble *epd2)
 
void EpdMultiply2Decimal (EpDouble *epd1, EpDouble *epd2)
 
void EpdMultiply3 (EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 
void EpdMultiply3Decimal (EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 
void EpdDivide (EpDouble *epd1, double value)
 
void EpdDivide2 (EpDouble *epd1, EpDouble *epd2)
 
void EpdDivide3 (EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 
void EpdAdd (EpDouble *epd1, double value)
 
void EpdAdd2 (EpDouble *epd1, EpDouble *epd2)
 
void EpdAdd3 (EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 
void EpdSubtract (EpDouble *epd1, double value)
 
void EpdSubtract2 (EpDouble *epd1, EpDouble *epd2)
 
void EpdSubtract3 (EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 
void EpdPow2 (int n, EpDouble *epd)
 
void EpdPow2Decimal (int n, EpDouble *epd)
 
void EpdNormalize (EpDouble *epd)
 
void EpdNormalizeDecimal (EpDouble *epd)
 
void EpdGetValueAndDecimalExponent (EpDouble *epd, double *value, int *exponent)
 
int EpdGetExponent (double value)
 
int EpdGetExponentDecimal (double value)
 
void EpdMakeInf (EpDouble *epd, int sign)
 
void EpdMakeZero (EpDouble *epd, int sign)
 
void EpdMakeNan (EpDouble *epd)
 
void EpdCopy (EpDouble *from, EpDouble *to)
 
int EpdIsInf (EpDouble *epd)
 
int EpdIsZero (EpDouble *epd)
 
int EpdIsNan (EpDouble *epd)
 
int EpdIsNanOrInf (EpDouble *epd)
 
int IsInfDouble (double value)
 
int IsNanDouble (double value)
 
int IsNanOrInfDouble (double value)
 

Macro Definition Documentation

#define EPD_EXP_INF   0x7ff

Definition at line 62 of file epd.h.

#define EPD_MAX_BIN   1023

CHeaderFile*****************************************************************

FileName [epd.h]

PackageName [epd]

Synopsis [The University of Colorado extended double precision package.]

Description [arithmetic functions with extended double precision.]

SeeAlso []

Author [In-Ho Moon]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Revision [

Id:
epd.h,v 1.9 2004/08/13 18:20:30 fabio Exp

]

Definition at line 60 of file epd.h.

#define EPD_MAX_DEC   308

Definition at line 61 of file epd.h.

Typedef Documentation

typedef struct EpDoubleStruct EpDouble

Definition at line 143 of file epd.h.

typedef union EpTypeUnion EpType

Definition at line 146 of file epd.h.

typedef struct IeeeDoubleStruct IeeeDouble

Definition at line 144 of file epd.h.

typedef struct IeeeNanStruct IeeeNan

Definition at line 145 of file epd.h.

Function Documentation

void EpdAdd ( EpDouble epd1,
double  value 
)

Function********************************************************************

Synopsis [Adds two arbitrary precision double values.]

Description [Adds two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 536 of file epd.c.

537 {
538  EpDouble epd2;
539  double tmp;
540  int exponent, diff;
541 
542  if (EpdIsNan(epd1) || IsNanDouble(value)) {
543  EpdMakeNan(epd1);
544  return;
545  } else if (EpdIsInf(epd1) || IsInfDouble(value)) {
546  int sign;
547 
548  EpdConvert(value, &epd2);
549  if (EpdIsInf(epd1) && IsInfDouble(value)) {
550  sign = epd1->type.bits.sign ^ epd2.type.bits.sign;
551  if (sign == 1)
552  EpdMakeNan(epd1);
553  } else if (EpdIsInf(&epd2)) {
554  EpdCopy(&epd2, epd1);
555  }
556  return;
557  }
558 
559  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
560 
561  EpdConvert(value, &epd2);
562  if (epd1->exponent > epd2.exponent) {
563  diff = epd1->exponent - epd2.exponent;
564  if (diff <= EPD_MAX_BIN)
565  tmp = epd1->type.value + epd2.type.value / pow((double)2.0, (double)diff);
566  else
567  tmp = epd1->type.value;
568  exponent = epd1->exponent;
569  } else if (epd1->exponent < epd2.exponent) {
570  diff = epd2.exponent - epd1->exponent;
571  if (diff <= EPD_MAX_BIN)
572  tmp = epd1->type.value / pow((double)2.0, (double)diff) + epd2.type.value;
573  else
574  tmp = epd2.type.value;
575  exponent = epd2.exponent;
576  } else {
577  tmp = epd1->type.value + epd2.type.value;
578  exponent = epd1->exponent;
579  }
580  epd1->type.value = tmp;
581  epd1->exponent = exponent;
582  EpdNormalize(epd1);
583 }
int IsNanDouble(double value)
Definition: epd.c:1305
double value
Definition: epd.h:130
void EpdConvert(double value, EpDouble *epd)
Definition: epd.c:185
unsigned int sign
Definition: epd.h:89
void EpdCopy(EpDouble *from, EpDouble *to)
Definition: epd.c:1182
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
int IsInfDouble(double value)
Definition: epd.c:1276
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdAdd2 ( EpDouble epd1,
EpDouble epd2 
)

Function********************************************************************

Synopsis [Adds two arbitrary precision double values.]

Description [Adds two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 598 of file epd.c.

599 {
600  double value;
601  int exponent, diff;
602 
603  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
604  EpdMakeNan(epd1);
605  return;
606  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
607  int sign;
608 
609  if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
610  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
611  if (sign == 1)
612  EpdMakeNan(epd1);
613  } else if (EpdIsInf(epd2)) {
614  EpdCopy(epd2, epd1);
615  }
616  return;
617  }
618 
619  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
620  assert(epd2->type.bits.exponent == EPD_MAX_BIN);
621 
622  if (epd1->exponent > epd2->exponent) {
623  diff = epd1->exponent - epd2->exponent;
624  if (diff <= EPD_MAX_BIN) {
625  value = epd1->type.value +
626  epd2->type.value / pow((double)2.0, (double)diff);
627  } else
628  value = epd1->type.value;
629  exponent = epd1->exponent;
630  } else if (epd1->exponent < epd2->exponent) {
631  diff = epd2->exponent - epd1->exponent;
632  if (diff <= EPD_MAX_BIN) {
633  value = epd1->type.value / pow((double)2.0, (double)diff) +
634  epd2->type.value;
635  } else
636  value = epd2->type.value;
637  exponent = epd2->exponent;
638  } else {
639  value = epd1->type.value + epd2->type.value;
640  exponent = epd1->exponent;
641  }
642  epd1->type.value = value;
643  epd1->exponent = exponent;
644  EpdNormalize(epd1);
645 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
void EpdCopy(EpDouble *from, EpDouble *to)
Definition: epd.c:1182
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdAdd3 ( EpDouble epd1,
EpDouble epd2,
EpDouble epd3 
)

Function********************************************************************

Synopsis [Adds two arbitrary precision double values.]

Description [Adds two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 660 of file epd.c.

661 {
662  double value;
663  int exponent, diff;
664 
665  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
666  EpdMakeNan(epd3);
667  return;
668  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
669  int sign;
670 
671  if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
672  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
673  if (sign == 1)
674  EpdMakeNan(epd3);
675  else
676  EpdCopy(epd1, epd3);
677  } else if (EpdIsInf(epd1)) {
678  EpdCopy(epd1, epd3);
679  } else {
680  EpdCopy(epd2, epd3);
681  }
682  return;
683  }
684 
685  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
686  assert(epd2->type.bits.exponent == EPD_MAX_BIN);
687 
688  if (epd1->exponent > epd2->exponent) {
689  diff = epd1->exponent - epd2->exponent;
690  if (diff <= EPD_MAX_BIN) {
691  value = epd1->type.value +
692  epd2->type.value / pow((double)2.0, (double)diff);
693  } else
694  value = epd1->type.value;
695  exponent = epd1->exponent;
696  } else if (epd1->exponent < epd2->exponent) {
697  diff = epd2->exponent - epd1->exponent;
698  if (diff <= EPD_MAX_BIN) {
699  value = epd1->type.value / pow((double)2.0, (double)diff) +
700  epd2->type.value;
701  } else
702  value = epd2->type.value;
703  exponent = epd2->exponent;
704  } else {
705  value = epd1->type.value + epd2->type.value;
706  exponent = epd1->exponent;
707  }
708  epd3->type.value = value;
709  epd3->exponent = exponent;
710  EpdNormalize(epd3);
711 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
void EpdCopy(EpDouble *from, EpDouble *to)
Definition: epd.c:1182
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
EpDouble* EpdAlloc ( void  )

AutomaticStart

CFile***********************************************************************

FileName [epd.c]

PackageName [epd]

Synopsis [Arithmetic functions with extended double precision.]

Description []

SeeAlso []

Author [In-Ho Moon]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Revision [

Id:
epd.c,v 1.10 2004/08/13 18:20:30 fabio Exp

] Function********************************************************************

Synopsis [Allocates an EpDouble struct.]

Description [Allocates an EpDouble struct.]

SideEffects []

SeeAlso []

Definition at line 72 of file epd.c.

73 {
74  EpDouble *epd;
75 
76  epd = ABC_ALLOC(EpDouble, 1);
77  return(epd);
78 }
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int EpdCmp ( const char *  key1,
const char *  key2 
)

Function********************************************************************

Synopsis [Compares two EpDouble struct.]

Description [Compares two EpDouble struct.]

SideEffects []

SeeAlso []

Definition at line 93 of file epd.c.

94 {
95  EpDouble *epd1 = (EpDouble *) key1;
96  EpDouble *epd2 = (EpDouble *) key2;
97  if (epd1->type.value != epd2->type.value ||
98  epd1->exponent != epd2->exponent) {
99  return(1);
100  }
101  return(0);
102 }
double value
Definition: epd.h:130
union EpTypeUnion type
Definition: epd.h:136
int exponent
Definition: epd.h:137
void EpdConvert ( double  value,
EpDouble epd 
)

Function********************************************************************

Synopsis [Converts double to EpDouble struct.]

Description [Converts double to EpDouble struct.]

SideEffects []

SeeAlso []

Definition at line 185 of file epd.c.

186 {
187  epd->type.value = value;
188  epd->exponent = 0;
189  EpdNormalize(epd);
190 }
double value
Definition: epd.h:130
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
union EpTypeUnion type
Definition: epd.h:136
int value
int exponent
Definition: epd.h:137
void EpdCopy ( EpDouble from,
EpDouble to 
)

Function********************************************************************

Synopsis [Copies a EpDouble struct.]

Description [Copies a EpDouble struct.]

SideEffects []

SeeAlso []

Definition at line 1182 of file epd.c.

1183 {
1184  to->type.value = from->type.value;
1185  to->exponent = from->exponent;
1186 }
double value
Definition: epd.h:130
union EpTypeUnion type
Definition: epd.h:136
int exponent
Definition: epd.h:137
void EpdDivide ( EpDouble epd1,
double  value 
)

Function********************************************************************

Synopsis [Divides two arbitrary precision double values.]

Description [Divides two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 386 of file epd.c.

387 {
388  EpDouble epd2;
389  double tmp;
390  int exponent;
391 
392  if (EpdIsNan(epd1) || IsNanDouble(value)) {
393  EpdMakeNan(epd1);
394  return;
395  } else if (EpdIsInf(epd1) || IsInfDouble(value)) {
396  int sign;
397 
398  EpdConvert(value, &epd2);
399  if (EpdIsInf(epd1) && IsInfDouble(value)) {
400  EpdMakeNan(epd1);
401  } else if (EpdIsInf(epd1)) {
402  sign = epd1->type.bits.sign ^ epd2.type.bits.sign;
403  EpdMakeInf(epd1, sign);
404  } else {
405  sign = epd1->type.bits.sign ^ epd2.type.bits.sign;
406  EpdMakeZero(epd1, sign);
407  }
408  return;
409  }
410 
411  if (value == 0.0) {
412  EpdMakeNan(epd1);
413  return;
414  }
415 
416  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
417 
418  EpdConvert(value, &epd2);
419  tmp = epd1->type.value / epd2.type.value;
420  exponent = epd1->exponent - epd2.exponent;
421  epd1->type.value = tmp;
422  epd1->exponent = exponent;
423  EpdNormalize(epd1);
424 }
int IsNanDouble(double value)
Definition: epd.c:1305
double value
Definition: epd.h:130
void EpdConvert(double value, EpDouble *epd)
Definition: epd.c:185
unsigned int sign
Definition: epd.h:89
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
int IsInfDouble(double value)
Definition: epd.c:1276
union EpTypeUnion type
Definition: epd.h:136
void EpdMakeZero(EpDouble *epd, int sign)
Definition: epd.c:1137
struct IeeeDoubleStruct bits
Definition: epd.h:131
void EpdMakeInf(EpDouble *epd, int sign)
Definition: epd.c:1115
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdDivide2 ( EpDouble epd1,
EpDouble epd2 
)

Function********************************************************************

Synopsis [Divides two arbitrary precision double values.]

Description [Divides two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 439 of file epd.c.

440 {
441  double value;
442  int exponent;
443 
444  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
445  EpdMakeNan(epd1);
446  return;
447  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
448  int sign;
449 
450  if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
451  EpdMakeNan(epd1);
452  } else if (EpdIsInf(epd1)) {
453  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
454  EpdMakeInf(epd1, sign);
455  } else {
456  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
457  EpdMakeZero(epd1, sign);
458  }
459  return;
460  }
461 
462  if (epd2->type.value == 0.0) {
463  EpdMakeNan(epd1);
464  return;
465  }
466 
467  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
468  assert(epd2->type.bits.exponent == EPD_MAX_BIN);
469 
470  value = epd1->type.value / epd2->type.value;
471  exponent = epd1->exponent - epd2->exponent;
472  epd1->type.value = value;
473  epd1->exponent = exponent;
474  EpdNormalize(epd1);
475 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
union EpTypeUnion type
Definition: epd.h:136
void EpdMakeZero(EpDouble *epd, int sign)
Definition: epd.c:1137
struct IeeeDoubleStruct bits
Definition: epd.h:131
void EpdMakeInf(EpDouble *epd, int sign)
Definition: epd.c:1115
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdDivide3 ( EpDouble epd1,
EpDouble epd2,
EpDouble epd3 
)

Function********************************************************************

Synopsis [Divides two arbitrary precision double values.]

Description [Divides two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 490 of file epd.c.

491 {
492  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
493  EpdMakeNan(epd3);
494  return;
495  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
496  int sign;
497 
498  if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
499  EpdMakeNan(epd3);
500  } else if (EpdIsInf(epd1)) {
501  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
502  EpdMakeInf(epd3, sign);
503  } else {
504  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
505  EpdMakeZero(epd3, sign);
506  }
507  return;
508  }
509 
510  if (epd2->type.value == 0.0) {
511  EpdMakeNan(epd3);
512  return;
513  }
514 
515  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
516  assert(epd2->type.bits.exponent == EPD_MAX_BIN);
517 
518  epd3->type.value = epd1->type.value / epd2->type.value;
519  epd3->exponent = epd1->exponent - epd2->exponent;
520  EpdNormalize(epd3);
521 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
union EpTypeUnion type
Definition: epd.h:136
void EpdMakeZero(EpDouble *epd, int sign)
Definition: epd.c:1137
struct IeeeDoubleStruct bits
Definition: epd.h:131
void EpdMakeInf(EpDouble *epd, int sign)
Definition: epd.c:1115
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdFree ( EpDouble epd)

Function********************************************************************

Synopsis [Frees an EpDouble struct.]

Description [Frees an EpDouble struct.]

SideEffects []

SeeAlso []

Definition at line 117 of file epd.c.

118 {
119  ABC_FREE(epd);
120 }
#define ABC_FREE(obj)
Definition: abc_global.h:232
int EpdGetExponent ( double  value)

Function********************************************************************

Synopsis [Returns the exponent value of a double.]

Description [Returns the exponent value of a double.]

SideEffects []

SeeAlso []

Definition at line 1068 of file epd.c.

1069 {
1070  int exponent;
1071  EpDouble epd;
1072 
1073  epd.type.value = value;
1074  exponent = epd.type.bits.exponent;
1075  return(exponent);
1076 }
double value
Definition: epd.h:130
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
int value
int EpdGetExponentDecimal ( double  value)

Function********************************************************************

Synopsis [Returns the decimal exponent value of a double.]

Description [Returns the decimal exponent value of a double.]

SideEffects []

SeeAlso []

Definition at line 1091 of file epd.c.

1092 {
1093  char *pos, str[24];
1094  int exponent;
1095 
1096  sprintf(str, "%E", value);
1097  pos = strstr(str, "E");
1098  sscanf(pos, "E%d", &exponent);
1099  return(exponent);
1100 }
bool pos
Definition: globals.c:30
char * strstr()
char * sprintf()
int value
void EpdGetString ( EpDouble epd,
char *  str 
)

Function********************************************************************

Synopsis [Converts an arbitrary precision double value to a string.]

Description [Converts an arbitrary precision double value to a string.]

SideEffects []

SeeAlso []

Definition at line 135 of file epd.c.

136 {
137  double value;
138  int exponent;
139  char *pos;
140 
141  if (IsNanDouble(epd->type.value)) {
142  sprintf(str, "NaN");
143  return;
144  } else if (IsInfDouble(epd->type.value)) {
145  if (epd->type.bits.sign == 1)
146  sprintf(str, "-Inf");
147  else
148  sprintf(str, "Inf");
149  return;
150  }
151 
152  assert(epd->type.bits.exponent == EPD_MAX_BIN ||
153  epd->type.bits.exponent == 0);
154 
155  EpdGetValueAndDecimalExponent(epd, &value, &exponent);
156  sprintf(str, "%e", value);
157  pos = strstr(str, "e");
158  if (exponent >= 0) {
159  if (exponent < 10)
160  sprintf(pos + 1, "+0%d", exponent);
161  else
162  sprintf(pos + 1, "+%d", exponent);
163  } else {
164  exponent *= -1;
165  if (exponent < 10)
166  sprintf(pos + 1, "-0%d", exponent);
167  else
168  sprintf(pos + 1, "-%d", exponent);
169  }
170 }
int IsNanDouble(double value)
Definition: epd.c:1305
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
void EpdGetValueAndDecimalExponent(EpDouble *epd, double *value, int *exponent)
Definition: epd.c:1034
bool pos
Definition: globals.c:30
int IsInfDouble(double value)
Definition: epd.c:1276
union EpTypeUnion type
Definition: epd.h:136
char * strstr()
char * sprintf()
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
int value
#define assert(ex)
Definition: util_old.h:213
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdGetValueAndDecimalExponent ( EpDouble epd,
double *  value,
int *  exponent 
)

Function********************************************************************

Synopsis [Returns value and decimal exponent of EpDouble.]

Description [Returns value and decimal exponent of EpDouble.]

SideEffects []

SeeAlso []

Definition at line 1034 of file epd.c.

1035 {
1036  EpDouble epd1, epd2;
1037 
1038  if (EpdIsNanOrInf(epd))
1039  return;
1040 
1041  if (EpdIsZero(epd)) {
1042  *value = 0.0;
1043  *exponent = 0;
1044  return;
1045  }
1046 
1047  epd1.type.value = epd->type.value;
1048  epd1.exponent = 0;
1049  EpdPow2Decimal(epd->exponent, &epd2);
1050  EpdMultiply2Decimal(&epd1, &epd2);
1051 
1052  *value = epd1.type.value;
1053  *exponent = epd1.exponent;
1054 }
double value
Definition: epd.h:130
union EpTypeUnion type
Definition: epd.h:136
void EpdPow2Decimal(int n, EpDouble *epd)
Definition: epd.c:946
int EpdIsZero(EpDouble *epd)
Definition: epd.c:1219
void EpdMultiply2Decimal(EpDouble *epd1, EpDouble *epd2)
Definition: epd.c:285
int value
int exponent
Definition: epd.h:137
int EpdIsNanOrInf(EpDouble *epd)
Definition: epd.c:1258
int EpdIsInf ( EpDouble epd)

Function********************************************************************

Synopsis [Checks whether the value is Inf.]

Description [Checks whether the value is Inf.]

SideEffects []

SeeAlso []

Definition at line 1201 of file epd.c.

1202 {
1203  return(IsInfDouble(epd->type.value));
1204 }
double value
Definition: epd.h:130
int IsInfDouble(double value)
Definition: epd.c:1276
union EpTypeUnion type
Definition: epd.h:136
int EpdIsNan ( EpDouble epd)

Function********************************************************************

Synopsis [Checks whether the value is NaN.]

Description [Checks whether the value is NaN.]

SideEffects []

SeeAlso []

Definition at line 1240 of file epd.c.

1241 {
1242  return(IsNanDouble(epd->type.value));
1243 }
int IsNanDouble(double value)
Definition: epd.c:1305
double value
Definition: epd.h:130
union EpTypeUnion type
Definition: epd.h:136
int EpdIsNanOrInf ( EpDouble epd)

Function********************************************************************

Synopsis [Checks whether the value is NaN or Inf.]

Description [Checks whether the value is NaN or Inf.]

SideEffects []

SeeAlso []

Definition at line 1258 of file epd.c.

1259 {
1260  return(IsNanOrInfDouble(epd->type.value));
1261 }
double value
Definition: epd.h:130
union EpTypeUnion type
Definition: epd.h:136
int IsNanOrInfDouble(double value)
Definition: epd.c:1333
int EpdIsZero ( EpDouble epd)

Function********************************************************************

Synopsis [Checks whether the value is Zero.]

Description [Checks whether the value is Zero.]

SideEffects []

SeeAlso []

Definition at line 1219 of file epd.c.

1220 {
1221  if (epd->type.value == 0.0)
1222  return(1);
1223  else
1224  return(0);
1225 }
double value
Definition: epd.h:130
union EpTypeUnion type
Definition: epd.h:136
void EpdMakeInf ( EpDouble epd,
int  sign 
)

Function********************************************************************

Synopsis [Makes EpDouble Inf.]

Description [Makes EpDouble Inf.]

SideEffects []

SeeAlso []

Definition at line 1115 of file epd.c.

1116 {
1117  epd->type.bits.mantissa1 = 0;
1118  epd->type.bits.mantissa0 = 0;
1119  epd->type.bits.exponent = EPD_EXP_INF;
1120  epd->type.bits.sign = sign;
1121  epd->exponent = 0;
1122 }
unsigned int sign
Definition: epd.h:89
unsigned int mantissa1
Definition: epd.h:86
bool sign(Lit p)
Definition: SolverTypes.h:61
unsigned int mantissa0
Definition: epd.h:87
#define EPD_EXP_INF
Definition: epd.h:62
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
int exponent
Definition: epd.h:137
void EpdMakeNan ( EpDouble epd)

Function********************************************************************

Synopsis [Makes EpDouble NaN.]

Description [Makes EpDouble NaN.]

SideEffects []

SeeAlso []

Definition at line 1159 of file epd.c.

1160 {
1161  epd->type.nan.mantissa1 = 0;
1162  epd->type.nan.mantissa0 = 0;
1163  epd->type.nan.quiet_bit = 1;
1164  epd->type.nan.exponent = EPD_EXP_INF;
1165  epd->type.nan.sign = 1;
1166  epd->exponent = 0;
1167 }
struct IeeeNanStruct nan
Definition: epd.h:132
#define EPD_EXP_INF
Definition: epd.h:62
unsigned int exponent
Definition: epd.h:115
union EpTypeUnion type
Definition: epd.h:136
unsigned int sign
Definition: epd.h:116
unsigned int mantissa0
Definition: epd.h:113
unsigned int quiet_bit
Definition: epd.h:114
unsigned int mantissa1
Definition: epd.h:112
int exponent
Definition: epd.h:137
void EpdMakeZero ( EpDouble epd,
int  sign 
)

Function********************************************************************

Synopsis [Makes EpDouble Zero.]

Description [Makes EpDouble Zero.]

SideEffects []

SeeAlso []

Definition at line 1137 of file epd.c.

1138 {
1139  epd->type.bits.mantissa1 = 0;
1140  epd->type.bits.mantissa0 = 0;
1141  epd->type.bits.exponent = 0;
1142  epd->type.bits.sign = sign;
1143  epd->exponent = 0;
1144 }
unsigned int sign
Definition: epd.h:89
unsigned int mantissa1
Definition: epd.h:86
bool sign(Lit p)
Definition: SolverTypes.h:61
unsigned int mantissa0
Definition: epd.h:87
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
int exponent
Definition: epd.h:137
void EpdMultiply ( EpDouble epd1,
double  value 
)

Function********************************************************************

Synopsis [Multiplies two arbitrary precision double values.]

Description [Multiplies two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 205 of file epd.c.

206 {
207  EpDouble epd2;
208  double tmp;
209  int exponent;
210 
211  if (EpdIsNan(epd1) || IsNanDouble(value)) {
212  EpdMakeNan(epd1);
213  return;
214  } else if (EpdIsInf(epd1) || IsInfDouble(value)) {
215  int sign;
216 
217  EpdConvert(value, &epd2);
218  sign = epd1->type.bits.sign ^ epd2.type.bits.sign;
219  EpdMakeInf(epd1, sign);
220  return;
221  }
222 
223  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
224 
225  EpdConvert(value, &epd2);
226  tmp = epd1->type.value * epd2.type.value;
227  exponent = epd1->exponent + epd2.exponent;
228  epd1->type.value = tmp;
229  epd1->exponent = exponent;
230  EpdNormalize(epd1);
231 }
int IsNanDouble(double value)
Definition: epd.c:1305
double value
Definition: epd.h:130
void EpdConvert(double value, EpDouble *epd)
Definition: epd.c:185
unsigned int sign
Definition: epd.h:89
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
int IsInfDouble(double value)
Definition: epd.c:1276
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
void EpdMakeInf(EpDouble *epd, int sign)
Definition: epd.c:1115
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdMultiply2 ( EpDouble epd1,
EpDouble epd2 
)

Function********************************************************************

Synopsis [Multiplies two arbitrary precision double values.]

Description [Multiplies two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 246 of file epd.c.

247 {
248  double value;
249  int exponent;
250 
251  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
252  EpdMakeNan(epd1);
253  return;
254  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
255  int sign;
256 
257  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
258  EpdMakeInf(epd1, sign);
259  return;
260  }
261 
262  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
263  assert(epd2->type.bits.exponent == EPD_MAX_BIN);
264 
265  value = epd1->type.value * epd2->type.value;
266  exponent = epd1->exponent + epd2->exponent;
267  epd1->type.value = value;
268  epd1->exponent = exponent;
269  EpdNormalize(epd1);
270 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
void EpdMakeInf(EpDouble *epd, int sign)
Definition: epd.c:1115
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdMultiply2Decimal ( EpDouble epd1,
EpDouble epd2 
)

Function********************************************************************

Synopsis [Multiplies two arbitrary precision double values.]

Description [Multiplies two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 285 of file epd.c.

286 {
287  double value;
288  int exponent;
289 
290  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
291  EpdMakeNan(epd1);
292  return;
293  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
294  int sign;
295 
296  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
297  EpdMakeInf(epd1, sign);
298  return;
299  }
300 
301  value = epd1->type.value * epd2->type.value;
302  exponent = epd1->exponent + epd2->exponent;
303  epd1->type.value = value;
304  epd1->exponent = exponent;
305  EpdNormalizeDecimal(epd1);
306 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalizeDecimal(EpDouble *epd)
Definition: epd.c:1007
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
void EpdMakeInf(EpDouble *epd, int sign)
Definition: epd.c:1115
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
void EpdMultiply3 ( EpDouble epd1,
EpDouble epd2,
EpDouble epd3 
)

Function********************************************************************

Synopsis [Multiplies two arbitrary precision double values.]

Description [Multiplies two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 321 of file epd.c.

322 {
323  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
324  EpdMakeNan(epd1);
325  return;
326  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
327  int sign;
328 
329  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
330  EpdMakeInf(epd3, sign);
331  return;
332  }
333 
334  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
335  assert(epd2->type.bits.exponent == EPD_MAX_BIN);
336 
337  epd3->type.value = epd1->type.value * epd2->type.value;
338  epd3->exponent = epd1->exponent + epd2->exponent;
339  EpdNormalize(epd3);
340 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
void EpdMakeInf(EpDouble *epd, int sign)
Definition: epd.c:1115
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdMultiply3Decimal ( EpDouble epd1,
EpDouble epd2,
EpDouble epd3 
)

Function********************************************************************

Synopsis [Multiplies two arbitrary precision double values.]

Description [Multiplies two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 355 of file epd.c.

356 {
357  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
358  EpdMakeNan(epd1);
359  return;
360  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
361  int sign;
362 
363  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
364  EpdMakeInf(epd3, sign);
365  return;
366  }
367 
368  epd3->type.value = epd1->type.value * epd2->type.value;
369  epd3->exponent = epd1->exponent + epd2->exponent;
370  EpdNormalizeDecimal(epd3);
371 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalizeDecimal(EpDouble *epd)
Definition: epd.c:1007
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
void EpdMakeInf(EpDouble *epd, int sign)
Definition: epd.c:1115
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
void EpdNormalize ( EpDouble epd)

Function********************************************************************

Synopsis [Normalize an arbitrary precision double value.]

Description [Normalize an arbitrary precision double value.]

SideEffects []

SeeAlso []

Definition at line 977 of file epd.c.

978 {
979  int exponent;
980 
981  if (IsNanOrInfDouble(epd->type.value)) {
982  epd->exponent = 0;
983  return;
984  }
985 
986  exponent = EpdGetExponent(epd->type.value);
987  if (exponent == EPD_MAX_BIN)
988  return;
989  exponent -= EPD_MAX_BIN;
990  epd->type.bits.exponent = EPD_MAX_BIN;
991  epd->exponent += exponent;
992 }
double value
Definition: epd.h:130
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
int IsNanOrInfDouble(double value)
Definition: epd.c:1333
int exponent
Definition: epd.h:137
#define EPD_MAX_BIN
Definition: epd.h:60
int EpdGetExponent(double value)
Definition: epd.c:1068
void EpdNormalizeDecimal ( EpDouble epd)

Function********************************************************************

Synopsis [Normalize an arbitrary precision double value.]

Description [Normalize an arbitrary precision double value.]

SideEffects []

SeeAlso []

Definition at line 1007 of file epd.c.

1008 {
1009  int exponent;
1010 
1011  if (IsNanOrInfDouble(epd->type.value)) {
1012  epd->exponent = 0;
1013  return;
1014  }
1015 
1016  exponent = EpdGetExponentDecimal(epd->type.value);
1017  epd->type.value /= pow((double)10.0, (double)exponent);
1018  epd->exponent += exponent;
1019 }
double value
Definition: epd.h:130
int EpdGetExponentDecimal(double value)
Definition: epd.c:1091
union EpTypeUnion type
Definition: epd.h:136
int IsNanOrInfDouble(double value)
Definition: epd.c:1333
int exponent
Definition: epd.h:137
void EpdPow2 ( int  n,
EpDouble epd 
)

Function********************************************************************

Synopsis [Computes arbitrary precision pow of base 2.]

Description [Computes arbitrary precision pow of base 2.]

SideEffects []

SeeAlso []

Definition at line 917 of file epd.c.

918 {
919  if (n <= EPD_MAX_BIN) {
920  EpdConvert(pow((double)2.0, (double)n), epd);
921  } else {
922  EpDouble epd1, epd2;
923  int n1, n2;
924 
925  n1 = n / 2;
926  n2 = n - n1;
927  EpdPow2(n1, &epd1);
928  EpdPow2(n2, &epd2);
929  EpdMultiply3(&epd1, &epd2, epd);
930  }
931 }
void EpdConvert(double value, EpDouble *epd)
Definition: epd.c:185
void EpdPow2(int n, EpDouble *epd)
Definition: epd.c:917
void EpdMultiply3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
Definition: epd.c:321
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdPow2Decimal ( int  n,
EpDouble epd 
)

Function********************************************************************

Synopsis [Computes arbitrary precision pow of base 2.]

Description [Computes arbitrary precision pow of base 2.]

SideEffects []

SeeAlso []

Definition at line 946 of file epd.c.

947 {
948  if (n <= EPD_MAX_BIN) {
949  epd->type.value = pow((double)2.0, (double)n);
950  epd->exponent = 0;
951  EpdNormalizeDecimal(epd);
952  } else {
953  EpDouble epd1, epd2;
954  int n1, n2;
955 
956  n1 = n / 2;
957  n2 = n - n1;
958  EpdPow2Decimal(n1, &epd1);
959  EpdPow2Decimal(n2, &epd2);
960  EpdMultiply3Decimal(&epd1, &epd2, epd);
961  }
962 }
double value
Definition: epd.h:130
void EpdNormalizeDecimal(EpDouble *epd)
Definition: epd.c:1007
union EpTypeUnion type
Definition: epd.h:136
void EpdPow2Decimal(int n, EpDouble *epd)
Definition: epd.c:946
void EpdMultiply3Decimal(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
Definition: epd.c:355
int exponent
Definition: epd.h:137
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdSubtract ( EpDouble epd1,
double  value 
)

Function********************************************************************

Synopsis [Subtracts two arbitrary precision double values.]

Description [Subtracts two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 726 of file epd.c.

727 {
728  EpDouble epd2;
729  double tmp;
730  int exponent, diff;
731 
732  if (EpdIsNan(epd1) || IsNanDouble(value)) {
733  EpdMakeNan(epd1);
734  return;
735  } else if (EpdIsInf(epd1) || IsInfDouble(value)) {
736  int sign;
737 
738  EpdConvert(value, &epd2);
739  if (EpdIsInf(epd1) && IsInfDouble(value)) {
740  sign = epd1->type.bits.sign ^ epd2.type.bits.sign;
741  if (sign == 0)
742  EpdMakeNan(epd1);
743  } else if (EpdIsInf(&epd2)) {
744  EpdCopy(&epd2, epd1);
745  }
746  return;
747  }
748 
749  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
750 
751  EpdConvert(value, &epd2);
752  if (epd1->exponent > epd2.exponent) {
753  diff = epd1->exponent - epd2.exponent;
754  if (diff <= EPD_MAX_BIN)
755  tmp = epd1->type.value - epd2.type.value / pow((double)2.0, (double)diff);
756  else
757  tmp = epd1->type.value;
758  exponent = epd1->exponent;
759  } else if (epd1->exponent < epd2.exponent) {
760  diff = epd2.exponent - epd1->exponent;
761  if (diff <= EPD_MAX_BIN)
762  tmp = epd1->type.value / pow((double)2.0, (double)diff) - epd2.type.value;
763  else
764  tmp = epd2.type.value * (double)(-1.0);
765  exponent = epd2.exponent;
766  } else {
767  tmp = epd1->type.value - epd2.type.value;
768  exponent = epd1->exponent;
769  }
770  epd1->type.value = tmp;
771  epd1->exponent = exponent;
772  EpdNormalize(epd1);
773 }
int IsNanDouble(double value)
Definition: epd.c:1305
double value
Definition: epd.h:130
void EpdConvert(double value, EpDouble *epd)
Definition: epd.c:185
unsigned int sign
Definition: epd.h:89
void EpdCopy(EpDouble *from, EpDouble *to)
Definition: epd.c:1182
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
int IsInfDouble(double value)
Definition: epd.c:1276
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdSubtract2 ( EpDouble epd1,
EpDouble epd2 
)

Function********************************************************************

Synopsis [Subtracts two arbitrary precision double values.]

Description [Subtracts two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 788 of file epd.c.

789 {
790  double value;
791  int exponent, diff;
792 
793  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
794  EpdMakeNan(epd1);
795  return;
796  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
797  int sign;
798 
799  if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
800  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
801  if (sign == 0)
802  EpdMakeNan(epd1);
803  } else if (EpdIsInf(epd2)) {
804  EpdCopy(epd2, epd1);
805  }
806  return;
807  }
808 
809  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
810  assert(epd2->type.bits.exponent == EPD_MAX_BIN);
811 
812  if (epd1->exponent > epd2->exponent) {
813  diff = epd1->exponent - epd2->exponent;
814  if (diff <= EPD_MAX_BIN) {
815  value = epd1->type.value -
816  epd2->type.value / pow((double)2.0, (double)diff);
817  } else
818  value = epd1->type.value;
819  exponent = epd1->exponent;
820  } else if (epd1->exponent < epd2->exponent) {
821  diff = epd2->exponent - epd1->exponent;
822  if (diff <= EPD_MAX_BIN) {
823  value = epd1->type.value / pow((double)2.0, (double)diff) -
824  epd2->type.value;
825  } else
826  value = epd2->type.value * (double)(-1.0);
827  exponent = epd2->exponent;
828  } else {
829  value = epd1->type.value - epd2->type.value;
830  exponent = epd1->exponent;
831  }
832  epd1->type.value = value;
833  epd1->exponent = exponent;
834  EpdNormalize(epd1);
835 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
void EpdCopy(EpDouble *from, EpDouble *to)
Definition: epd.c:1182
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
void EpdSubtract3 ( EpDouble epd1,
EpDouble epd2,
EpDouble epd3 
)

Function********************************************************************

Synopsis [Subtracts two arbitrary precision double values.]

Description [Subtracts two arbitrary precision double values.]

SideEffects []

SeeAlso []

Definition at line 850 of file epd.c.

851 {
852  double value;
853  int exponent, diff;
854 
855  if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
856  EpdMakeNan(epd3);
857  return;
858  } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
859  int sign;
860 
861  if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
862  sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
863  if (sign == 0)
864  EpdCopy(epd1, epd3);
865  else
866  EpdMakeNan(epd3);
867  } else if (EpdIsInf(epd1)) {
868  EpdCopy(epd1, epd1);
869  } else {
870  sign = epd2->type.bits.sign ^ 0x1;
871  EpdMakeInf(epd3, sign);
872  }
873  return;
874  }
875 
876  assert(epd1->type.bits.exponent == EPD_MAX_BIN);
877  assert(epd2->type.bits.exponent == EPD_MAX_BIN);
878 
879  if (epd1->exponent > epd2->exponent) {
880  diff = epd1->exponent - epd2->exponent;
881  if (diff <= EPD_MAX_BIN) {
882  value = epd1->type.value -
883  epd2->type.value / pow((double)2.0, (double)diff);
884  } else
885  value = epd1->type.value;
886  exponent = epd1->exponent;
887  } else if (epd1->exponent < epd2->exponent) {
888  diff = epd2->exponent - epd1->exponent;
889  if (diff <= EPD_MAX_BIN) {
890  value = epd1->type.value / pow((double)2.0, (double)diff) -
891  epd2->type.value;
892  } else
893  value = epd2->type.value * (double)(-1.0);
894  exponent = epd2->exponent;
895  } else {
896  value = epd1->type.value - epd2->type.value;
897  exponent = epd1->exponent;
898  }
899  epd3->type.value = value;
900  epd3->exponent = exponent;
901  EpdNormalize(epd3);
902 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
void EpdCopy(EpDouble *from, EpDouble *to)
Definition: epd.c:1182
bool sign(Lit p)
Definition: SolverTypes.h:61
int EpdIsNan(EpDouble *epd)
Definition: epd.c:1240
void EpdNormalize(EpDouble *epd)
Definition: epd.c:977
union EpTypeUnion type
Definition: epd.h:136
struct IeeeDoubleStruct bits
Definition: epd.h:131
void EpdMakeInf(EpDouble *epd, int sign)
Definition: epd.c:1115
unsigned int exponent
Definition: epd.h:88
void EpdMakeNan(EpDouble *epd)
Definition: epd.c:1159
int value
#define assert(ex)
Definition: util_old.h:213
int exponent
Definition: epd.h:137
int EpdIsInf(EpDouble *epd)
Definition: epd.c:1201
#define EPD_MAX_BIN
Definition: epd.h:60
int IsInfDouble ( double  value)

Function********************************************************************

Synopsis [Checks whether the value is Inf.]

Description [Checks whether the value is Inf.]

SideEffects []

SeeAlso []

Definition at line 1276 of file epd.c.

1277 {
1278  EpType val;
1279 
1280  val.value = value;
1281  if (val.bits.exponent == EPD_EXP_INF &&
1282  val.bits.mantissa0 == 0 &&
1283  val.bits.mantissa1 == 0) {
1284  if (val.bits.sign == 0)
1285  return(1);
1286  else
1287  return(-1);
1288  }
1289  return(0);
1290 }
double value
Definition: epd.h:130
unsigned int sign
Definition: epd.h:89
unsigned int mantissa1
Definition: epd.h:86
unsigned int mantissa0
Definition: epd.h:87
#define EPD_EXP_INF
Definition: epd.h:62
struct IeeeDoubleStruct bits
Definition: epd.h:131
unsigned int exponent
Definition: epd.h:88
int value
int IsNanDouble ( double  value)

Function********************************************************************

Synopsis [Checks whether the value is NaN.]

Description [Checks whether the value is NaN.]

SideEffects []

SeeAlso []

Definition at line 1305 of file epd.c.

1306 {
1307  EpType val;
1308 
1309  val.value = value;
1310  if (val.nan.exponent == EPD_EXP_INF &&
1311  val.nan.sign == 1 &&
1312  val.nan.quiet_bit == 1 &&
1313  val.nan.mantissa0 == 0 &&
1314  val.nan.mantissa1 == 0) {
1315  return(1);
1316  }
1317  return(0);
1318 }
double value
Definition: epd.h:130
struct IeeeNanStruct nan
Definition: epd.h:132
#define EPD_EXP_INF
Definition: epd.h:62
unsigned int exponent
Definition: epd.h:115
unsigned int sign
Definition: epd.h:116
unsigned int mantissa0
Definition: epd.h:113
unsigned int quiet_bit
Definition: epd.h:114
unsigned int mantissa1
Definition: epd.h:112
int value
int IsNanOrInfDouble ( double  value)

Function********************************************************************

Synopsis [Checks whether the value is NaN or Inf.]

Description [Checks whether the value is NaN or Inf.]

SideEffects []

SeeAlso []

Definition at line 1333 of file epd.c.

1334 {
1335  EpType val;
1336 
1337  val.value = value;
1338  if (val.nan.exponent == EPD_EXP_INF &&
1339  val.nan.mantissa0 == 0 &&
1340  val.nan.mantissa1 == 0 &&
1341  (val.nan.sign == 1 || val.nan.quiet_bit == 0)) {
1342  return(1);
1343  }
1344  return(0);
1345 }
double value
Definition: epd.h:130
struct IeeeNanStruct nan
Definition: epd.h:132
#define EPD_EXP_INF
Definition: epd.h:62
unsigned int exponent
Definition: epd.h:115
unsigned int sign
Definition: epd.h:116
unsigned int mantissa0
Definition: epd.h:113
unsigned int quiet_bit
Definition: epd.h:114
unsigned int mantissa1
Definition: epd.h:112
int value