Hets - the Heterogeneous Tool Set

Copyright(c) Klaus Luettich, Rainer Grabbe 2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Prover)
Safe HaskellNone

Proofs.BatchProcessing

Description

Functions for batch processing. Used by SoftFOL provers.

Synopsis

Documentation

batchTimeLimit :: Int

Time limit used by the batch mode prover.

isTimeLimitExceeded :: ATPRetval -> Bool

Checks whether an ATPRetval indicates that the time limit was exceeded.

adjustOrSetConfig

Arguments

:: Ord proof_tree 
=> (GenericConfig proof_tree -> GenericConfig proof_tree)

function to be applied against the current configuration or a new emptyConfig

-> String

name of the prover

-> ATPIdentifier

name of the goal

-> proof_tree

initial empty proof_tree

-> GenericConfigsMap proof_tree

current GenericConfigsMap

-> GenericConfigsMap proof_tree

resulting GenericConfigsMap with the changes applied

Adjusts the configuration associated to a goal by applying the supplied function or inserts a new emptyConfig with the function applied if there's no configuration associated yet.

Uses Map.member, Map.adjust, and Map.insert for the corresponding tasks internally.

checkGoal :: GenericConfigsMap proof_tree -> ATPIdentifier -> Bool

Checks whether a goal in the results map is marked as proved.

goalProcessed

Arguments

:: Ord proof_tree 
=> MVar (GenericState sentence proof_tree pst)

IORef pointing to the backing State data structure

-> Int

batch time limit

-> [String]

extra options

-> Int 
-> String

name of the prover

-> Int

number of goals processed so far

-> Named sentence

goal that has just been processed

-> Bool

wether to be verbose: print goal status (CMDL mode)

-> (ATPRetval, GenericConfig proof_tree) 
-> IO Bool 

Called every time a goal has been processed in the batch mode.

genericProveBatch

Arguments

:: (Ord sentence, Ord proof_tree) 
=> Bool

True means use tLimit/options from GenericState

-> Int

batch time limit

-> [String]

extra options passed

-> Bool

True means include proved theorems

-> Bool 
-> (Int -> Named sentence -> Maybe (Named sentence) -> (ATPRetval, GenericConfig proof_tree) -> IO Bool)

called after every prover run. return True if you want the prover to continue.

-> (pst -> Named sentence -> pst)

inserts a Namend sentence into a logicalPart

-> RunProver sentence proof_tree pst 
-> String

prover name

-> String

theory name

-> GenericState sentence proof_tree pst 
-> Maybe (MVar (Result [ProofStatus proof_tree]))

empty MVar to be filled after each proof attempt

-> IO [ProofStatus proof_tree]

proof status for each goal

A non-GUI batch mode prover. The list of goals is processed sequentially. Proved goals are inserted as axioms.

genericCMDLautomaticBatch

Arguments

:: (Ord proof_tree, Ord sentence) 
=> ATPFunctions sign sentence mor proof_tree pst

prover specific functions

-> Bool

True means include proved theorems

-> Bool

True means save problem file

-> MVar (Result [ProofStatus proof_tree])

used to store the result of each attempt in the batch run

-> String

prover name

-> String

theory name

-> ATPTacticScript

default prover specific tactic script

-> Theory sign sentence proof_tree

theory consisting of a signature and a list of Named sentence

-> [FreeDefMorphism sentence mor]

freeness constraints

-> proof_tree

initial empty proof_tree

-> IO (ThreadId, MVar ())

fst: identifier of the batch thread for killing it snd: MVar to wait for the end of the thread

Automatic command line prover using batch mode.