Module dev.civl.sarl
Package dev.civl.sarl.reason.IF

Interface ReasonerFactory

public interface ReasonerFactory

A factory for producing instances of Reasoner. Each BooleanExpression has an associated Reasoner. The boolean expression is called the context for that reasoner. The context is the fixed, underlying assumption used by that reasoner whenever it is called to check validity or to simplify a formula.

A ReasonerFactory may cache the Reasoners it produces, so that if called twice on the same (or just "equal") boolean expression, the same instance of Reasoner will be returned.

  • Method Details

    • workingDirectory

      Path workingDirectory()
      Returns the working directory for the theorem provers created by this factory. This is the directory where temporary files are stored, such as query files.
      Returns:
      working directory

    • getReasoner

      Reasoner getReasoner(BooleanExpression context, boolean useBackwardSubstitution, ProverFunctionInterpretation[] proverPredicates)
      Gets a Reasoner for the given context. If this method is called twice with two contexts that are equal (according to method SymbolicObject.equals(Object)), the second call may return the same instance as the first call (i.e., the factory may cache the results).
      Parameters:
      context - a non-null boolean expression to be used as the context for the Reasoner
      useBackwardSubstitution - shall the reasoner use backwards substitution to solve for certain numeric expressions in terms of others when simplifying?
      proverPredicates - ProverFunctionInterpretations which factor out common boolean expressions from complex prover contexts and queries
      simplifyWithTrivialProver - should the reasoner's
      invalid reference 
      Simplifier
      use a TrivialProver or the one constructed by the factory returned by
      invalid reference 
      getTheoremProverFactory
      ?
      Returns:
      a Reasoner based on the given context

    • getReasoner

      Reasoner getReasoner(List<BooleanExpression> contextStack, boolean useBackwardSubstitution, ProverFunctionInterpretation[] proverPredicates)