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.