Complete Prover Refactor

[yushan87]

Summary

With the VCGenerator refactor almost complete, it is time to integrate the Congruence Class Prover. Below is a check list of things that will need to happen before we can run tests on the new compiler. Currently, the list is incomplete and new items will be added when we encounter them during the refactoring process.

Refactor Check List

• [ ] CongruenceClassProver
• [x] Immutable ADTs
• [x] Iterators
• [ ] Output
  • [x] Metrics
  • [ ] PerVCProverModel
• [x] PExp hierarchy
  • [x] absyn
    • [x] PExp
    • [x] PSymbol
    • [x] PLambda
    • [x] PAlternative
  • [x] iterators
    • [x] PExpSubexpressionIterator
    • [x] PSymbolArgumentIterator
    • [x] PLambdaBodyIterator
    • [x] PAlternativesIterator
  • [x] visitors
    • [x] PExpVisitor
    • [x] NestedPExpVisitors
    • [x] PExpTextRenderingVisitor
• [x] Utilities classes
  • [x] expressions
    • [x] ConjunctionOfNormalizedAtomicExpressions
    • [x] NormalizedAtomicExpressions
  • [x] theorems
    • [x] Theorem (Originally TheoremCongruenceClosureImpl)
    • [x] TheoremPrioritizer
    • [x] TheoremWithScore
  • [x] ImmutableVC (Combined Hampton's VC and Mike's VerificationConditionCongruenceClosureImpl)
  • [x] Registry

New Changes Check List

• [ ] FileOutputListener method for displaying prover results

Issues to Address

• [ ] Issue #205