[impl:prover] Subclass ProverResult and make it abstract

team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)

BSD 3-Clause "New" or "Revised" License

5 stars 3 forks source link

[impl:prover] Subclass ProverResult and make it abstract #2

Closed bafain closed 12 years ago

bafain commented 12 years ago

Encapsulate check result information (satisfiability, model, errors) extraction in ProverResult subclasses and let StdProver#getResult implementations decide which extractor to instantiate. For example will Z3Prover instantiate Z3ProverResult which knows how to interpret Z3 outputs.