| Copyright | (c) Klaus Luettich Rainer Grabbe 2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | luecke@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | non-portable (imports Logic.Prover) |
| Safe Haskell | None |
Proofs.BatchProcessing
Description
Functions for batch processing. Used by SoftFOL provers.
Synopsis
- batchTimeLimit :: Int
- isTimeLimitExceeded :: ATPRetval -> Bool
- adjustOrSetConfig :: Ord proof_tree => (GenericConfig proof_tree -> GenericConfig proof_tree) -> String -> ATPIdentifier -> proof_tree -> GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
- filterOpenGoals :: GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
- checkGoal :: GenericConfigsMap proof_tree -> ATPIdentifier -> Bool
- goalProcessed :: Ord proof_tree => MVar (GenericState sentence proof_tree pst) -> Int -> [String] -> Int -> String -> Int -> Named sentence -> Bool -> (ATPRetval, GenericConfig proof_tree) -> IO Bool
- genericProveBatch :: (Show sentence, Ord sentence, Ord proof_tree) => Bool -> Int -> [String] -> Bool -> Bool -> (Int -> Named sentence -> Maybe (Named sentence) -> (ATPRetval, GenericConfig proof_tree) -> IO Bool) -> (pst -> Named sentence -> pst) -> RunProver sentence proof_tree pst -> String -> String -> GenericState sentence proof_tree pst -> Maybe (MVar (Result [ProofStatus proof_tree])) -> IO [ProofStatus proof_tree]
- genericCMDLautomaticBatch :: (Show sentence, Ord proof_tree, Ord sentence) => ATPFunctions sign sentence mor proof_tree pst -> Bool -> Bool -> MVar (Result [ProofStatus proof_tree]) -> String -> String -> ATPTacticScript -> Theory sign sentence proof_tree -> [FreeDefMorphism sentence mor] -> proof_tree -> IO (ThreadId, MVar ())
Documentation
batchTimeLimit :: Int Source #
Time limit used by the batch mode prover.
isTimeLimitExceeded :: ATPRetval -> Bool Source #
Checks whether an ATPRetval indicates that the time limit was exceeded.
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.
filterOpenGoals :: GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree Source #
checkGoal :: GenericConfigsMap proof_tree -> ATPIdentifier -> Bool Source #
Checks whether a goal in the results map is marked as proved.
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.
Arguments
| :: (Show sentence, 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 Source #
Arguments
| :: (Show sentence, 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.