Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-08-14 00:50:26 -0700 (Tue, 14 Aug 2001)
Revision: 3370
Log message:

      Everything that I had before should be state aware now. :)
      Fir_test now has a few test cases, and more will be needed
      to make sure everything is working properly.
      
      The complex1 test case blows up horribly right now.
      It evaluates perfectly well, but takes an amazingly
      large amount of resources.  The .prlb file (not included) for that
      one proof is 8.4 MB and MetaPRL ~64MB of RAM and 2 minutes on a
      1 GHz Pentium III system.
      After the proof, the "counts" were [2, ~34000] for that proof
      (took me 2 steps).  After restarting MetaPRL and reloading the proof,
      the counts were [2,290483].  Needless to say, something needs
      to be done concerning efficiency.  As far as I can tell, things
      are not being reduced in an optimal order. I'll be looking more
      into this.
      

Changes  Path
+0 -4 metaprl/theories/mc/Makefile
+40 -18 metaprl/theories/mc/fir_exp.ml
+15 -5 metaprl/theories/mc/fir_exp.mli
+12 -12 metaprl/theories/mc/fir_int.ml
+4 -4 metaprl/theories/mc/fir_int_set.ml
+1 -1 metaprl/theories/mc/fir_int_set.mli
Deleted metaprl/theories/mc/fir_itt_state.ml
Deleted metaprl/theories/mc/fir_itt_state.mli
Deleted metaprl/theories/mc/fir_sos.ml
Deleted metaprl/theories/mc/fir_sos.mli
+127 -43 metaprl/theories/mc/fir_state.ml
+47 -27 metaprl/theories/mc/fir_state.mli
+51 -26 metaprl/theories/mc/fir_test.ml
+1 -0 metaprl/theories/mc/fir_test.mli
+0 -5 metaprl/theories/mc/fir_ty.ml
+0 -5 metaprl/theories/mc/fir_ty.mli