Hets - the Heterogeneous Tool Set

Copyright(c) Simon Ulbricht, Uni Bremen 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertekknix@informatik.uni-bremen.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

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 

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