Hi Khaza, If you don't care about the output, you could try
val _ = time defCNF.DEF_CNF_VECTOR_CONV ``<my BIG input>``; That should just print the time for the conversion and throw away the result. Cheers, Joe On Fri, Dec 11, 2009 at 6:14 AM, Khaza Anuarul Hoque <[email protected]> wrote: > I have a big file of DNF which has 500 clause, each clause has upto 50 > literals. now i > was trying to do the cnf conversion using HOL4 Kan4 release. > > load "tautLib"; > open tautLib; > load "defCNF"; > open defCNF; > > time defCNF.DEF_CNF_VECTOR_CONV ``<my BIG input>``; > > Whenever i do this it returns me an exception "Ptetty Printer: out_of_memory". > Seems like this is a problem because HOL is running out of memory > while printing the output on screen. So is there any way to do the > computation in background rather in printing on screen ?? All i need > is the time of that cnf computation, i dont need to see the output. I > am sure there is a way to do this... can anyone help me ?? Its more > than urgent.... > > regards > -- > Khaza Anuarul Hoque, B.Sc Engr > M.A.Sc Student, Dept. of ECE > Concordia University, Montreal, Canada > Web: http://users.encs.concordia.ca/~k_hoque > > > > > > > ------------------------------------------------------------------------------ > Return on Information: > Google Enterprise Search pays you back > Get the facts. > http://p.sf.net/sfu/google-dev2dev > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ Return on Information: Google Enterprise Search pays you back Get the facts. http://p.sf.net/sfu/google-dev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
