More simplifications to the KCFG class

[ehildenb]

This brings in what should be most of the rest of the refactorings to the KCFG class, including:

• Removing data from the KCFG class:
  • The notion of target is removed (tracked in classes like APRProof where it has semantic meaning).
  • The notion of init is broadened to any node not having predecessors.
  • The notion of frontier is removed (in favor of leaves).
  • The notion of expanded is removed, in favor of direct storage of stuck attribute for given nodes.
  • The notion of init in renamed to root.
• Move the path_length method to a staticmethod of the KCFG class intead of being direct in kcfg module.
• sort_ac_collections is changed to hardcode how it searches for AC collections, rather than using a KDefinition. This is potentially a problem down the road, if the user names a sort quite specifically, but allows not threading through a KDefinition into KCFGShow and such.
• Refactors to KCFGShow:
  • Move KCFGShow.to_module to KCFG.to_module. Do any post-processing needed in KCFGShow instead, which may require a definition or extra CLI arguments.
  • Remove all handling of target nodes from KCFGShow.
• Refactors to the APRProof and APRBMCProof classes, how they compute their node subsets:
  • The predicates APR*Proof.is_... are prioritized for defining the sets rather than the other way around.
  • New predicate APR*Proof.is_failing and set APR*Proof.failing is added, to determine if there are failing nodes.
  • APRProof.status is updated to cehck the failing set directly, and then the exact same status can be used in subclass APRBMCProof.status instead of duplicating that check.
  • Logic for checking sbuproof status is simplified.
• Add class APRProofShow for printing out information about APRProof. It:
  • Holds a KCFGShow for printing out the KCFG portion.
  • Extends the functionality to include the extra information about target nodes.