Lines Matching defs:id
77 fun getIntBranch fin id h =
83 else let val ci = id-(sat_getint fin)
91 fun addBranch lfn cl sva fin tc id =
92 let val (br,brl) = getIntBranch fin id (id-(rshift tc))
96 ((*print "\nB ";print( (int_to_string id)^": ");
99 resolveChain lfn sva cl (br,brl) id; true) (* resolve *)
119 fun addClause lfn cl sva vc clauseth fin lit1 id =
122 (*val _ = (print "\nR ";print((int_to_string orc)^"~"^(int_to_string id)^": ");
125 [] => failwith ("addClause:Failed parsing clause "^(int_to_string id)^"\n")
126 | _ => prepareRootClause lfn orc clauseth cl id
132 fun readTrace lfn cl sva vc clauseth fin id =
134 then id
138 then let val _ = addClause lfn cl sva vc clauseth fin tmp id
139 in readTrace lfn cl sva vc clauseth fin (id+1) end
140 else (let val isch = addBranch lfn cl sva fin tmp id
142 then readTrace lfn cl sva vc clauseth fin (id+1) (* chain *)
143 else readTrace lfn cl sva vc clauseth fin id end) (* deletion *)
153 val id = readTrace lfn cl sva vc clauseth fin 0
155 in SOME id end
168 SOME id => SOME (Dynarray.sub(cl,id-1))