Interface TheoremProverFactory

All Known Implementing Classes:
MultiProverFactory, RobustCVCTheoremProverFactory, RobustWhy3ProvePlatformFactory, RobustZ3TheoremProverFactory

public interface TheoremProverFactory
A factory for producing instances of TheoremProver. Each instance of TheoremProver contains a specific, fixed "context". The context is a boolean symbolic expression. It is the assumption that is used for all queries asked of that theorem prover. In symbolic execution, the context is typically the "path condition". Hence a distinct theorem prover is generated for each path condition.
  • Method Details