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
