RCAD

RCell : a new data structure, a refined CAD

An RCAD is a list (LEVEL, CHILD, ASSIGNED, TRUTH, SAMPLE, INDX, SIGNPF, HOWTV, DEGSUB, MULSUB, INCELL), with the following meanings:

  1. LEVEL - the level of the cell.
  2. CHILD - a list of RCell data structures, the children.
  3. ASSIGNED - Assignment flag (for parallel execution only).
  4. TRUTH - the truth value of the cell: TRUE, FALSE, or UNDET.
  5. SAMPLE - a sample point data structure.
  6. INDX - the index of the cell as a list.
  7. SIGNPF - a list (S_1,...,S_k), where k is the LEVEL of the cell. S_i is a list (s_1,...,s_n) where n is the number of k-i+1 level projection factors, and s_j is the sign of ... well here I change things. The n projection factors at some level m are (P_m,i_1, P_m,i_2, ... , P_m,i_n), where i_1 < i_2 < ... < i_n. So s_j is the sign of P_i,i_{k-i+1} in the cell.
  8. HOWTV - how the truth value was assigned, the possibilities are BYTEV = trial evaluation, BYPRP = propogation, BYEQC = equational constraint, and NOTDET = not determined.
  9. DEGSUB - List of degrees of substituted projection factors.
  10. MULSUB - List of multiplicities of substituted projection factors.
  11. INCELL - the cell in the qepcad CAD which contains this RCELL.
  12. OSPFLAG - a flag that equals 1 if this cell's sample point was a sample point from the original CAD.

Last modified: Tue Jan 19 10:33:19 EST 1999