The idea here is to come up with some format for formulas that
will allow me to do all the manipulations I want. Here is the
definition of a formula in this format.
Let D be a CAD and P be its projection factor set:
- (TRUE) and (FALSE) are both formulas.
- ((i,j),op) is a formula, where 0 < i <= |P| and 0 < j <=
|P_i|, and op is in {LTOP,EQOP,GTOP,GEOP,NEOP,LEOP}.
- (ANDOP,F_1,...,F_i) is a formula, where i > 1 and
F_1,...,F_i are formulas.
- (OROP,F_1,...,F_i) is a formula, where i > 1 and F_1,...,F_i
are formulas.
- ((i,j),(op,k)) is a formula,where 0 < i <= |P| and 0 < j <
|P_i|, and op
is in {LTOP,EQOP,GTOP,GEOP,NEOP,LEOP} and k is a non-zero int.
The list (i,j) will refer to a polynomial in the following way:
The signiture vector for a given cell assumes an ordering on the
polynomials of a given level in P. So, (i,j) refers to the jth
polynomial in the ordering of the elements of P_i.
The interpretation of 5. is probably deserving of some
explanation. Let us give a name to the polynomial (i,j), call
it q(x_1, ...,x_i).
Then ((i,j),(op,k)) is interpreted as
- if k > 0
- x_i op "the kth root of
q(x_1, ..., x_{i-1}, X)", where X is a purely symbolic
variable. This atomic formula is true if and only
if q(x_1, ..., x_{i-1}, X) has at least k roots, and x_i bears
relation op to the kth of these, ordered smallest to largest.
- if 0 > k
- x_i op "the |k|th root of
q(x_1, ..., x_{i-1}, X)", where X is a purely symbolic
variable. This atomic formula is true if and only
if q(x_1, ..., x_{i-1}, X) has at least |k| roots, and x_i bears
relation op to the |k|th of these, ordered largest to smallest.
Last modified: Tue Jul 30 15:25:05 EDT 2002