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 Source #

stores each node to be considered along with some further infomation

Constructors

FNode 

Fields

Instances

Eq FNode Source # 

Methods

(==) :: FNode -> FNode -> Bool

(/=) :: FNode -> FNode -> Bool

Ord FNode Source #

for comparison, the goal status of each node is considered. only with equal goal status, nodes are sorted by name.

Methods

compare :: FNode -> FNode -> Ordering

(<) :: FNode -> FNode -> Bool

(<=) :: FNode -> FNode -> Bool

(>) :: FNode -> FNode -> Bool

(>=) :: FNode -> FNode -> Bool

max :: FNode -> FNode -> FNode

min :: FNode -> FNode -> FNode

Show FNode Source #

Get a markup string containing name and color

Methods

showsPrec :: Int -> FNode -> ShowS

show :: FNode -> String

showList :: [FNode] -> ShowS

toGtkGoals :: FNode -> [Goal] Source #

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 Source #

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

showStatus :: FNode -> String Source #

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

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

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 Source #

returns True if a node has not been proved jet

timedout :: FNode -> Bool Source #

returns True if at least one goal has been timed out

allProved :: FNode -> Bool Source #

returns True only if every goal has been proved