Hets - the Heterogeneous Tool Set

Copyright(c) Rainer Grabbe
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

SoftFOL.MathServMapping

Description

Maps a MathServResponse into a GenericConfig structure.

Synopsis

Documentation

brokerName :: String

Name of the prover if MathServ was called via Broker.

mapMathServResponse

Arguments

:: [String]

all axiom names

-> Either String MathServResponse

SOAP faultstring or Parsed MathServ data

-> GenericConfig ProofTree

configuration to use

-> Named SPTerm

goal to prove

-> String

prover name

-> (ATPRetval, GenericConfig ProofTree)

(retval, configuration with proof status and complete output)

Maps a MathServResponse record into a GenericConfig with ProofStatus. If an error occured, an ATPError with error message instead of result output will be returned.

mapProverResult

Arguments

:: [String]

all axiom names

-> MWFoAtpResult

parsed FoATPResult data

-> MWTimeResource

global time spent

-> GenericConfig ProofTree

configuration to use

-> Named SPTerm

goal to prove

-> String

prover name

-> (ATPRetval, GenericConfig ProofTree)

(retval, configuration with proof status, complete output)

Maps a FoAtpResult record into a GenericConfig with ProofStatus. Result output contains all important informations in a list of Strings. The function should only be called if there is a FoAtpResult available.

mapToGoalStatus

Arguments

:: MWStatus

goal status

-> GoalStatus

final parsed goal status

Maps the status message from MathServ results to GoalStatus.

usedProverName

Arguments

:: String

Prover name from MathServResponse

-> String

name without version number or unknown

Gets the prover name from MathServResponse and extracts the name only (without version number). If the name's empty, prover name is "unknown".

defaultProofStatus

Arguments

:: Named SPTerm

goal to prove

-> String

prover name

-> Int

time limit

-> [String]

list of used options

-> String

proof tree (simple text)

-> ProofStatus ProofTree 

Default proof status. Contains the goal name, prover name and the time limit option used by MathServ.

proofStat

Arguments

:: [String]

all axiom names

-> Named SPTerm

goal to prove

-> GoalStatus

Nothing stands for prove error

-> [String]

Used axioms in the proof

-> Bool

Timeout status

-> ProofStatus ProofTree

default proof status

-> (ATPRetval, ProofStatus ProofTree)

General return value of a prover run, used in GUI. Detailed proof status if information is available.

Returns the value of a prover run used in GUI (Success or TLimitExceeded), and the proofStatus containing all prove information available.