Lines Matching defs:cl
91 fun addBranch lfn cl sva fin tc id =
99 resolveChain lfn sva cl (br,brl) id; true) (* resolve *)
119 fun addClause lfn cl sva vc clauseth fin lit1 id =
126 | _ => prepareRootClause lfn orc clauseth cl id
132 fun readTrace lfn cl sva vc clauseth fin 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 *)
149 fun parseTrace cl sva nr fname solver vc clauseth lfn proof =
153 val id = readTrace lfn cl sva vc clauseth fin 0
166 val cl = Dynarray.array((Array.length clauseth) * 2,TRUTH)
167 in case parseTrace cl sva nr fname solver vc clauseth lfn proof of
168 SOME id => SOME (Dynarray.sub(cl,id-1))