Hi, I played a little bit with computeLib in order to see its capabilities and got stuck with efficiency problems when dealing with "case ... of". My problem is that all branches are necessarily evaluated thus yielding huge efficiency wastes. The standard way to control the evaluation order for parameters would be lazyfy_thm. However, it is of no use here since the argument which allows to decide on which branch to follow is the last one. For instance ``case x of T => 1 | F => 2`` is actually a shortcut for ``bool_case 1 2 x``: x is in the end so lazyfy_thm cannot do anything.
Did I misunderstand something or is there a standard workaround? Regards, -- Vincent Aravantinos Postdoctoral Fellow, Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent ------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
