You could use Globals.max_print_depth := 10;
(try: help "max_print_depth"). You could also do val _ = time defCNF.DEF_CNF_VECTOR_CONV ``<my BIG input>``; which will perform the computation, giving you the time, but then throw away the result. Anthony. On 11 Dec 2009, at 14:14, Khaza Anuarul Hoque 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
