Complete Prover Refactor

[AdityaSenthilvel]

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] ImmutableADTs
• [x] Iterators
• [ ] Output
  • [x] Metrics
  • [ ] PerVCProverModel
• [x] PExp hierarchy
  • [x] abysn
    • [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 #7

[rhit-fosswe]

Out of scope for our team (at least for now). Original ticket is from June 17, 2018. It has been updated since then, but this is not really part of our project (currently).