Module dev.civl.sarl
Package dev.civl.sarl.prove.IF

Interface TheoremProverFactory

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

    • workingDirectory

      Path workingDirectory()
      The directory that can be used for files generated by the theory provers created by this factory.
      Returns:
      the directory

    • 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)
      Returns:
      a theorem prover operating under the given context