1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
/*======================================================================
t <- ESPCADDOPFSUFF(P,D)
Do the projection factors suffice?
inputs
P : Projection factor set data structure.
K : A list of ESPCAD cells, all in a CAD defined by P, and
all with the same signiture.
outputs
t : NIL if no solution formula exists using the pols in P.
Otherwise, TRUE, FALSE, or UNDET.
TRUE (FALSE) if all cells in substrees rooted at cells K which
have truth values have truth value TRUE (FALSE). Otherwise
UNDET.
======================================================================*/
#include "qepcad.h"
#include "espcad.h"
static Word comp(Word A, Word B) __pure;
#define BDCOMP(a,b) ((a) > (b) ? 1 : ((a) < (b) ? -1 : 0))
Word ESPCADDOPFSUFF(Word P, Word K)
{
Word t,L,Kp,Lp,T,F,Lpp,tp,C;
Step1: /* Initialize. */
if (LELTI(FIRST(K),LEVEL) == 0 && LELTI(FIRST(K),CHILD) == NIL) {
t = LELTI(FIRST(K),TRUTH);
goto Return; }
else
t = NIL;
Step3: /* List cells of level r, sorted by signiture. */
L = NIL;
for(Kp = K; Kp != NIL; Kp = RED(Kp)) {
C = LELTI(FIRST(Kp),SC_CDTV);
L = CCONC(ISATOM(C) ? NIL : C,L); }
L = GISL(L,comp);
Step4: /* Loop over each block of cells with same signiture. */
while (L != NIL) {
Lp = NIL;
do {
Lp = COMP(FIRST(L),Lp);
L = RED(L);
} while (L != NIL && comp(FIRST(Lp),FIRST(L)) == 0);
Step5: /* Get the number of TRUE leaf cells and FALSE leaf cells. */
T = 0; F = 0;
for(Lpp = Lp; Lpp != NIL; Lpp = RED(Lpp)) {
switch( LELTI(FIRST(Lpp),TRUTH) ) {
case TRUE : T++; break;
case FALSE: F++; break; } }
Step6: /* Case: All cells are leaf cells. */
if (T + F == LENGTH(Lp)) {
if ( T > 0 && F == 0 ) { tp = TRUE; goto Step8; }
if ( F > 0 && T == 0 ) { tp = FALSE; goto Step8; }
t = NIL; goto Return; }
Step7: /* Case: Not all cells are leaf cells. */
tp = ESPCADDOPFSUFF(P,Lp);
if ( ( F == 0 && T == 0 && tp != NIL) ||
( F == 0 && T > 0 && tp == TRUE ) ||
( F > 0 && T == 0 && tp == FALSE ) )
goto Step8;
t = NIL; goto Return;
Step8: /* Set t to the proper value. t = NIL at this step only if
it is the first time through the loop. */
if (t == NIL)
t = tp;
else
if (t != tp) t = UNDET; }
Return: /* Prepare to return. */
return (t);
}
/*-- Comparison of signitures of cells. Both cells
-- are assumed to be of the same level, and both cells are
-- assumed to have the same signiture on all projection factors
-- of level lower than the cells themselves. */
static Word comp(Word A, Word B)
{
Word s_a,s_b,t;
Step1: /* Initialization. */
s_a = LELTI(A,SC_SIGN);
s_b = LELTI(B,SC_SIGN);
t = 0;
Step2: /* Compare siginitures. */
while ( t == 0 && s_a != NIL) {
t = BDCOMP(FIRST(s_a),FIRST(s_b));
s_a = RED(s_a); s_b = RED(s_b); }
Return: /* Return. */
return (t);
}
|
