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 |

Functions for batch processing. Used by SoftFOL provers.

- 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 :: (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 :: (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

Time limit used by the batch mode prover.

isTimeLimitExceeded :: ATPRetval -> Bool

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

:: 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

checkGoal :: GenericConfigsMap proof_tree -> ATPIdentifier -> Bool

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

:: 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.

:: (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.

:: (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.