Use a function that computes the result as an intermediate value, but throws
it away. The ML interpreter does not optimise this out and still does the
computation.
So:
time
(fn tm =>
let val _ = defCNF.DEF_CNF_VECTOR_CONV tm
in () end)
``<my BIG input>``;
Mark
Mark Adams,
Proof Technologies Ltd.
on 12/12/09 3:05 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
