Copyright	(c) Simon Ulbricht, Uni Bremen 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	tekknix@informatik.uni-bremen.de
Stability	provisional
Portability	portable
Safe Haskell	None

Common.AutoProofUtils

Description

This module provides sturctures and methods for the automatic proofs module.

Synopsis

Documentation

data FNode

stores each node to be considered along with some further infomation

Constructors

FNode
Fields name :: String node :: LNode DGNodeLab sublogic :: G_sublogics goals :: [String] results :: G_theory

Instances

Eq FNode
Ord FNode	for comparison, the goal status of each node is considered. only with equal goal status, nodes are sorted by name.
Show FNode	Get a markup string containing name and color

toGtkGoals :: FNode -> [Goal]

mostly for the purpose of proper display, the resulting G_theory of each FNode can be converted into a list of Goals.

goalsToPrefix :: [Goal] -> String

as a Prefix for display purpose, the ratio of proven and total goals is shown

showStatus :: FNode -> String

Displays every goal of a Node with a prefix showing the status and the goal name.

initFNodes :: [LNode DGNodeLab] -> [FNode]

gets all Nodes from the DGraph as input and creates a list of FNodes only containing Nodes to be considered. The results status field is initialised with the nodes local theory

unchecked :: FNode -> Bool

returns True if a node has not been proved jet

timedout :: FNode -> Bool

returns True if at least one goal has been timed out

allProved :: FNode -> Bool

returns True only if every goal has been proved