Package edu.udel.cis.vsl.sarl.prove.IF

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 Summary

Modifier and Type	Method	Description
TheoremProver	newProver(BooleanExpression context)	Returns a new instance of TheoremProver with the given context.
TheoremProver	newProver(BooleanExpression context, ProverFunctionInterpretation[] logicFunctions)	Returns a new instance of TheoremProver with the given context.

Method Details

newProver

TheoremProver newProver(BooleanExpression context)

Returns a new instance of TheoremProver with the given context.

Parameters:

context - boolean expression assumed to hold

Returns:

a theorem prover operating under the given context

newProver

TheoremProver newProver(BooleanExpression context,
 ProverFunctionInterpretation[] logicFunctions)

Returns a new instance of TheoremProver with the given context.

Parameters:

context - boolean expression assumed to hold

logicFunctions - A list of ProverFunctionInterpretations. Some provers support factoring the common and complex parts into logic functions (e.g. z3, cvc4, why3)

Returns:

a theorem prover operating under the given context