aboutsummaryrefslogtreecommitdiff
path: root/ic-reals-6.3/base/boolUtil.c
diff options
context:
space:
mode:
Diffstat (limited to 'ic-reals-6.3/base/boolUtil.c')
-rw-r--r--ic-reals-6.3/base/boolUtil.c405
1 files changed, 405 insertions, 0 deletions
diff --git a/ic-reals-6.3/base/boolUtil.c b/ic-reals-6.3/base/boolUtil.c
new file mode 100644
index 0000000..f768a46
--- /dev/null
+++ b/ic-reals-6.3/base/boolUtil.c
@@ -0,0 +1,405 @@
+/*
+ * Copyright (C) 2000, Imperial College
+ *
+ * This file is part of the Imperial College Exact Real Arithmetic Library.
+ * See the copyright notice included in the distribution for conditions
+ * of use.
+ */
+
+#include <stdio.h>
+#include "real.h"
+#include "real-impl.h"
+
+/*
+ * Various utilities used by predicates and boolean operators.
+ */
+void
+force_To_Bool_From_The_Abyss()
+{
+ Bool b;
+ b = (Bool) POP;
+
+ Error(FATAL, E_INT, "force_To_Bool_From_The_Abyss",
+ "trying to force a boolean which is already known");
+}
+
+void
+force_To_PredX_From_The_Abyss()
+{
+ PredX *predX;
+ predX = (PredX *) POP;
+
+ Error(FATAL, E_INT, "force_To_PredX_From_The_Abyss",
+ "trying to force a predicate which is already known");
+}
+
+
+void
+absorbDigsXIntoPredX(PredX *predX)
+{
+ DigsX *digsX;
+
+ digsX = (DigsX *) predX->x;
+ predX->x = digsX->x;
+
+#ifdef DAVINCI
+ beginGraphUpdate();
+ deleteOnlyEdge(predX, digsX);
+ newEdgeToOnlyChild(predX, digsX->x);
+ endGraphUpdate();
+#endif
+}
+
+void
+absorbSignXIntoPredX(PredX *predX)
+{
+ SignX *signX;
+
+ signX = (SignX *) predX->x;
+ predX->x = signX->x;
+
+#ifdef DAVINCI
+ beginGraphUpdate();
+ deleteOnlyEdge(predX, signX);
+ newEdgeToOnlyChild(predX, signX->x);
+ endGraphUpdate();
+#endif
+}
+
+void
+setBoolXY(BoolXY *boolXY, BoolVal v)
+{
+ boolXY->tag.value = v;
+
+ switch (v) {
+ case LAZY_TRUE :
+ case LAZY_FALSE :
+#ifdef DAVINCI
+ beginGraphUpdate();
+ deleteEdgeToXChild(boolXY, boolXY->x);
+ deleteEdgeToYChild(boolXY, boolXY->y);
+ endGraphUpdate();
+#endif
+ boolXY->force = force_To_Bool_From_The_Abyss;
+ boolXY->x = NULL;
+ boolXY->y = NULL;
+ break;
+ case LAZY_UNKNOWN :
+ break;
+ default :
+ Error(FATAL, E_INT, "setBoolXY", "bad boolean value");
+ }
+}
+
+void
+setPredX(PredX *predX, BoolVal v)
+{
+ predX->tag.value = v;
+
+ switch (v) {
+ case LAZY_TRUE :
+ case LAZY_FALSE :
+#ifdef DAVINCI
+ beginGraphUpdate();
+ deleteOnlyEdge(predX, predX->x);
+ endGraphUpdate();
+#endif
+ predX->force = force_To_Bool_From_The_Abyss;
+ predX->x = NULL;
+ break;
+ case LAZY_UNKNOWN :
+ break;
+ default :
+ Error(FATAL, E_INT, "setPredX", "bad boolean value");
+ }
+}
+
+void
+setBoolX(BoolX *boolX, BoolVal v)
+{
+ boolX->tag.value = v;
+
+ switch (v) {
+ case LAZY_TRUE :
+ case LAZY_FALSE :
+#ifdef DAVINCI
+ beginGraphUpdate();
+ deleteOnlyEdge(boolX, boolX->x);
+ endGraphUpdate();
+#endif
+ boolX->force = force_To_Bool_From_The_Abyss;
+ boolX->x = NULL;
+ break;
+ case LAZY_UNKNOWN :
+ break;
+ default :
+ Error(FATAL, E_INT, "setBoolX", "bad boolean value");
+ }
+}
+
+PredX *
+allocPredX(Real x)
+{
+ PredX *predX;
+
+ if ((predX = (PredX *) malloc(sizeof(PredX))) == NULL)
+ Error(FATAL, E_INT, "allocPredX", "malloc failed");
+
+#ifdef DAVINCI
+ newNodeId(predX);
+#else
+#ifdef TRACE
+ newNodeId(predX);
+#endif
+#endif
+
+ predX->tag.type = PREDX;
+ predX->tag.value = LAZY_UNKNOWN;
+ predX->tag.dumped = FALSE;
+ predX->x = x;
+
+#ifdef DAVINCI
+ beginGraphUpdate();
+ newNode(predX, PREDX);
+ newEdgeToOnlyChild(predX, x);
+ endGraphUpdate();
+#endif
+
+ return predX;
+}
+
+/*
+ * This consumes a stream of characteristic pairs. If a pair (c,n) has the
+ * property that c = 2n-1, then the boolean is LAZY_UNKNOWN, otherwise
+ * it gets set to LAZY_TRUE and we advance to the next pair.
+ */
+void
+force_To_PredX_From_DigsX_2n_minus_1_True_Entry()
+{
+ PredX *predX;
+ DigsX *digsX;
+ void force_To_PredX_From_DigsX_2n_minus_1_True_Cont();
+
+ predX = (PredX *) POP;
+ digsX = (DigsX *) predX->x;
+
+ PUSH_2(force_To_PredX_From_DigsX_2n_minus_1_True_Cont, predX);
+ if (digsX->count == 0)
+ PUSH_3(digsX->force, digsX, defaultForceCount);
+}
+
+/*
+ * At this point we know we have some digits available, ie a characteristic
+ * pair (c,n) with n > 0. The predicate is set LAZY_TRUE if c != 2n-1.
+ * Otherwise we just arrange to consume more digits.
+ */
+void
+force_To_PredX_From_DigsX_2n_minus_1_True_Cont()
+{
+ PredX *predX;
+ DigsX *digsX;
+ void force_To_Bool_From_The_Abyss();
+
+ predX = (PredX *) POP;
+ digsX = (DigsX *) predX->x;
+
+#ifdef PACK_DIGITS
+ if (digsX->count <= DIGITS_PER_WORD) {
+ if (digsX->word.small == (1 << digsX->count) - 1)
+ absorbDigsXIntoPredX(predX);
+ else
+ setPredX(predX, LAZY_TRUE);
+ }
+ else {
+#endif
+ /*
+ * This is comparing a big word with +(2^n - 1). It would be faster
+ * to compare each word with 0xffffffff but this may have to
+ * wait. ####
+ */
+ if (mpz_sgn(digsX->word.big) > 0 &&
+ mpz_popcount(digsX->word.big) == digsX->count)
+ absorbDigsXIntoPredX(predX);
+ else
+ setPredX(predX, LAZY_TRUE);
+#ifdef PACK_DIGITS
+ }
+#endif
+}
+
+/*
+ * This consumes a stream of characteristic pairs. If a pair (c,n) has the
+ * property that c = 2n-1, then the boolean is LAZY_UNKNOWN, otherwise
+ * it gets set to LAZY_FALSE and we advance to the next pair.
+ */
+void
+force_To_PredX_From_DigsX_2n_minus_1_False_Entry()
+{
+ PredX *predX;
+ DigsX *digsX;
+ void force_To_PredX_From_DigsX_2n_minus_1_False_Cont();
+
+ predX = (PredX *) POP;
+ digsX = (DigsX *) predX->x;
+
+ PUSH_2(force_To_PredX_From_DigsX_2n_minus_1_False_Cont, predX);
+ if (digsX->count == 0)
+ PUSH_3(digsX->force, digsX, defaultForceCount);
+}
+
+/*
+ * At this point we know we have some digits available, ie a characteristic
+ * pair (c,n) with n > 0. The predicate is set LAZY_FALSE if c != 2n-1.
+ * Otherwise we just arrange to consume more digits.
+ */
+void
+force_To_PredX_From_DigsX_2n_minus_1_False_Cont()
+{
+ PredX *predX;
+ DigsX *digsX;
+ void force_To_Bool_From_The_Abyss();
+
+ predX = (PredX *) POP;
+ digsX = (DigsX *) predX->x;
+
+#ifdef PACK_DIGITS
+ if (digsX->count <= DIGITS_PER_WORD) {
+ if (digsX->word.small == (1 << digsX->count) - 1)
+ absorbDigsXIntoPredX(predX);
+ else
+ setPredX(predX, LAZY_FALSE);
+ }
+ else {
+#endif
+ /*
+ * This is comparing a big word with +(2^n - 1). It would be faster
+ * to compare each word with 0xffffffff but this may have to
+ * wait. ####
+ */
+ if (mpz_sgn(digsX->word.big) > 0 &&
+ mpz_popcount(digsX->word.big) == digsX->count)
+ absorbDigsXIntoPredX(predX);
+ else
+ setPredX(predX, LAZY_FALSE);
+#ifdef PACK_DIGITS
+ }
+#endif
+}
+
+/*
+ * This consumes a stream of characteristic pairs. If a pair (c,n) has the
+ * property that -c = 2n-1, then the boolean is LAZY_UNKNOWN, otherwise
+ * it gets set to LAZY_FALSE and we advance to the next pair.
+ */
+void
+force_To_PredX_From_DigsX_minus_2n_minus_1_False_Entry()
+{
+ PredX *predX;
+ DigsX *digsX;
+ void force_To_PredX_From_DigsX_minus_2n_minus_1_False_Cont();
+
+ predX = (PredX *) POP;
+ digsX = (DigsX *) predX->x;
+
+ PUSH_2(force_To_PredX_From_DigsX_minus_2n_minus_1_False_Cont, predX);
+ if (digsX->count == 0)
+ PUSH_3(digsX->force, digsX, defaultForceCount);
+}
+
+/*
+ * At this point we know we have some digits available, ie a characteristic
+ * pair (c,n) with n > 0. The predicate is set LAZY_FALSE if -c != 2n-1.
+ * Otherwise we just arrange to consume more digits.
+ */
+void
+force_To_PredX_From_DigsX_minus_2n_minus_1_False_Cont()
+{
+ PredX *predX;
+ DigsX *digsX;
+ void force_To_Bool_From_The_Abyss();
+
+ predX = (PredX *) POP;
+ digsX = (DigsX *) predX->x;
+
+#ifdef PACK_DIGITS
+ if (digsX->count <= DIGITS_PER_WORD) {
+ if (digsX->word.small == -((1 << digsX->count) - 1))
+ absorbDigsXIntoPredX(predX);
+ else
+ setPredX(predX, LAZY_FALSE);
+ }
+ else {
+#endif
+ /*
+ * This is comparing a big word with -(2^n - 1).
+ *
+ * THIS RELIES ON GMP USING SIGN/MAGNITUDE REPRESENTATION.
+ */
+ if (mpz_sgn(digsX->word.big) < 0 &&
+ mpz_popcount(digsX->word.big) == digsX->count)
+ absorbDigsXIntoPredX(predX);
+ else
+ setPredX(predX, LAZY_FALSE);
+#ifdef PACK_DIGITS
+ }
+#endif
+}
+
+/*
+ * This consumes a stream of characteristic pairs. If a pair (c,n) has the
+ * property that -c = 2n-1, then the boolean is LAZY_UNKNOWN, otherwise
+ * it gets set to LAZY_TRUE and we advance to the next pair.
+ */
+void
+force_To_PredX_From_DigsX_minus_2n_minus_1_True_Entry()
+{
+ PredX *predX;
+ DigsX *digsX;
+ void force_To_PredX_From_DigsX_minus_2n_minus_1_True_Cont();
+
+ predX = (PredX *) POP;
+ digsX = (DigsX *) predX->x;
+
+ PUSH_2(force_To_PredX_From_DigsX_minus_2n_minus_1_True_Cont, predX);
+ if (digsX->count == 0)
+ PUSH_3(digsX->force, digsX, defaultForceCount);
+}
+
+/*
+ * At this point we know we have some digits available, ie a characteristic
+ * pair (c,n) with n > 0. The predicate is set LAZY_TRUE if -c != 2n-1.
+ * Otherwise we just arrange to consume more digits.
+ */
+void
+force_To_PredX_From_DigsX_minus_2n_minus_1_True_Cont()
+{
+ PredX *predX;
+ DigsX *digsX;
+ void force_To_Bool_From_The_Abyss();
+
+ predX = (PredX *) POP;
+ digsX = (DigsX *) predX->x;
+
+#ifdef PACK_DIGITS
+ if (digsX->count <= DIGITS_PER_WORD) {
+ if (digsX->word.small == -((1 << digsX->count) - 1))
+ absorbDigsXIntoPredX(predX);
+ else
+ setPredX(predX, LAZY_TRUE);
+ }
+ else {
+#endif
+ /*
+ * This is comparing a big word with -(2^n - 1).
+ *
+ * THIS RELIES ON GMP USING SIGN/MAGNITUDE REPRESENTATION.
+ */
+ if (mpz_sgn(digsX->word.big) < 0 &&
+ mpz_popcount(digsX->word.big) == digsX->count)
+ absorbDigsXIntoPredX(predX);
+ else
+ setPredX(predX, LAZY_TRUE);
+#ifdef PACK_DIGITS
+ }
+#endif
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-19 16:35:48 +0000