redlog/ofsf/ofsfcad.red

474    begin scalar basecell;
475       basecell := acell_mk(0, nil, nil, nil, nil);  % the only cell of R^0
476       return ofsf_ftoc(basecell, hh, varl)
479 asserted procedure ofsf_ftoc(basecell: Acell, hh: Atom, varl: List): Atree;
480    % Full CAD tree over cell. [basecell] is a cell in R^{j-1}, [hh] is a vector
482    % (x_1, ..., x_r). Returns an Atree over the basecell. Intuition: Recursively
487       sp := acell_getsp basecell;
493       % (1) Non-recursion Case: j = r + 1. [basecell] is a leaf.
497       	 return atree_mk basecell
508       res := atree_mk basecell;
514    begin scalar basecell;
515       % basecell := acell_mk(0, nil, nil, 'true, nil);  % the only cell of R^0
516       basecell := acell_mk(0, nil, nil, nil, nil);  % the only cell of R^0
517       return ofsf_ptoc(basecell, cl_nnf caddata_psi cd, cd)
520 asserted procedure ofsf_ptoc(basecell: Acell, psi: QfFormula, cd: CadData): Atree;
521    % Partial CAD tree over cell. [basecell] is a cell in R^{j-1}. Returns a
522    % partial tree over [basecell]. Intuition: Recursively find for a cell C in
528       sp := acell_getsp basecell;
534       % (1) Non-recursion Case: j = r + 1. [basecell] is a leaf.
536 	 acell_puttv(basecell, ofsf_evalqff(psi, sp, varl));
539       	 return atree_mk basecell
546 	    acell_puttv(basecell, psi);
549 	    return atree_mk basecell
568       	 res := atree_mk basecell;
584       acell_puttv(basecell, tv);
585       res := atree_mk basecell;
591 	 ofsf_addanswers(basecell, treel, j, cd);
648 asserted procedure ofsf_addanswers(basecell: Acell, treel: List, j: Integer, cd: CadData): Any;
661       	 % 	 acell_addtagip(basecell,
1242       % Print basecell: