ClemsonRSRG/RESOLVE — pull request #136 by yushan87 (2014-10-31 04:01:46+00:00)
Title: Cpsc372fixes

1) Decreasing clauses for loops are not optional. The VC generator expects a decreasing clause and it is not one that we can generate. (We really don't know what is decreasing at the compiler level... The user should provide that to us) Maintaining clauses and Changing clauses remain optional, because if not supplied all variables are changing and we "maintain" true!

2) Replace is such a pain. For some reason CharExp and StringExp did not implement the replace method! I went ahead and implemented it, but can't help to feel that Dan is right and we should use substitute...

3) The PExp builder doesn't deal with CharExp and StringExp... (No idea why they wouldn't! Hampton wrote one for IntegerExp) I followed the same logic to write one for CharExp and StringExp.