Portability	unportable
Stability	unstable
Maintainer	Martin Avanzini <martin.avanzini@uibk.ac.at>
Safe Haskell	None

Tct.Processor

Contents

Answers
Complexity Proofs
- Partial Proofs
Complexity Processors
Existentially Quantified Processors, Instances and Proofs
Any Processor
The Solver Monad

Description

This module defines basic interfaces and functionality concerning complexity processors. A parameterised complexity processor, a so called processor instance, constructs from a complexity problem a proof object.

Synopsis

Answers

data Answer

The datatype Answer reflects the answer type from the complexity competition.

Constructors

CertAnswer Certificate
MaybeAnswer
NoAnswer
TimeoutAnswer

Instances

Eq Answer
Ord Answer
Show Answer
PrettyPrintable Answer
Parsable Answer
ComplexityProof Answer

yesAnswer :: Answer

Abbreviation for 'CertAnswer $ certified (unknown, unknown)'.

Complexity Proofs

class ComplexityProof proof where

Complexity proofs should be instance of the ComplexityProof class.

Methods

answer :: proof -> Answer

Construct an Answer from the proof.

pprintProof :: proof -> PPMode -> Doc

Pretty printer of proof.

toXml :: proof -> XmlContent

Instances

ComplexityProof Answer
ComplexityProof SomeProof
ComplexityProof OpenProof
ComplexityProof TrivialProof
ComplexityProof PopStarOrder
ComplexityProof MpoOrder
ComplexityProof MatrixOrder
ComplexityProof ArcticOrder
ComplexityProof PolynomialOrder
ComplexityProof BoundsProof
ComplexityProof PredicateProof
ComplexityProof proof => ComplexityProof (PartialProof proof)
Processor proc => ComplexityProof (Proof proc)
ComplexityProof (ProofOf p) => ComplexityProof (TOProof p)
ComplexityProof o => ComplexityProof (OrientationProof o)
ComplexityProof proof => ComplexityProof (MaybeSubsumed proof)
Processor p => ComplexityProof (OneOfProof p)
Processor p => ComplexityProof (TimedProof p)
(Transformer t, Processor sub) => ComplexityProof (Proof t sub)
(Transformer g, Processor t, Processor e) => ComplexityProof (IteProgressProof g t e)
(Processor g, Processor t, Processor e, ComplexityProof (ProofOf g), ComplexityProof (ProofOf t), ComplexityProof (ProofOf e)) => ComplexityProof (IteProof g t e)

certificate :: ComplexityProof p => p -> Certificate

returns the Certificate associated with the proof.

succeeded :: ComplexityProof p => p -> Bool

The predicate succeeded p holds iff answer p is of shape CertAnswer _.

failed :: ComplexityProof p => p -> Bool

Negation of succeeded.

isTimeout :: ComplexityProof p => p -> Bool

The predicate isTimeout p holds iff answer p is of shape TimeoutAnswer _.

data Proof proc

Objects of type 'Proof proc' correspond to a proof node, collecting the applied processor, the input problem and the proof constructed by the processor

Constructors

Proof
Fields appliedProcessor :: InstanceOf proc inputProblem :: Problem result :: ProofOf proc

Instances

Processor proc => ComplexityProof (Proof proc)

Partial Proofs

data SelectorExpression

Defines a notion of selected rules, specified as monotone Boolean Formula. SelectorExpressions are used for instance in solvePartial to determine which rules should be oriented by a processor.

Constructors

SelectDP Rule
SelectTrs Rule
BigAnd [SelectorExpression]
BigOr [SelectorExpression]

Instances

Show SelectorExpression
Typeable SelectorExpression
AssocArgument (RuleSelector SelectorExpression)

data PartialProof proof

Objects of type 'ProofPartial proc' correspond to a proof node obtained by solvePartial.

Constructors

PartialProof
Fields ppInputProblem :: Problem The input problem ppResult :: proof The proof of the applied processor. `answer proof` must reflect number of applications from rules in `ppRemovableDPs` and `ppRemovableTrs` with respect to derivations of the input problem. ppRemovableDPs :: [Rule] Dependency pair rules that whose complexity has been estimated by the applied processor. ppRemovableTrs :: [Rule] Rules that whose complexity has been estimated by the applied processor.
PartialInapplicable	Returned if the processor does not support `solvePartial`
Fields ppInputProblem :: Problem The input problem

Instances

ComplexityProof proof => ComplexityProof (PartialProof proof)

progressed :: PartialProof proof -> Bool

Returns true iff ppRemovableTrs or ppRemovableDPs is not empty.

Complexity Processors

class ComplexityProof (ProofOf proc) => Processor proc where

A processor p is an object whose instances 'InstanceOf p' are equipped with a solving method, translating a complexity problem into a proof object of type 'ProofOf proc'.

Associated Types

data InstanceOf proc

The instance of the processor.

type ProofOf proc

The proof type of the processor.

Methods

name :: proc -> String

Each processor is supposed to have a unique name.

instanceName :: InstanceOf proc -> String

Each instance of the processor should have a name, used in proof output.

processorToXml :: InstanceOf proc -> XmlContent

solve_ :: SolverM m => InstanceOf proc -> Problem -> m (ProofOf proc)

The solve method. Given an instance and a problem, it constructs a proof object. This method should not be called directly, instead the method solve from the class SolverM should be called.

solvePartial_ :: SolverM m => InstanceOf proc -> SelectorExpression -> Problem -> m (PartialProof (ProofOf proc))

Similar to solve_, but constructs a PartialProof. At least all rules in the additional paramter of type SelectorExpression should be removed. Per default, this method returns PartialInapplicable.

Instances

Processor AnyProcessor
Processor SomeProcessor
(Processor proc, Arguments (ArgumentsOf proc)) => Processor (StdProcessor proc)
Processor proc => Processor (Subsumed proc)
(Arguments arg, ComplexityProof res) => Processor (Custom arg res)

apply :: (SolverM m, Processor proc) => InstanceOf proc -> Problem -> m (Proof proc)

Similar to solve but wraps the result into a Proof object.

class Processor a => ParsableProcessor a where

Parsable processors provide additional information for parsing.

Methods

description :: a -> [String]

synString :: a -> SynString

posArgs :: a -> [(Int, ArgDescr)]

optArgs :: a -> [ArgDescr]

parseProcessor_ :: a -> ProcessorParser (InstanceOf a)

parseFromArgsInteractive :: a -> AnyProcessor -> IO (InstanceOf a)

Instances

ParsableProcessor AnyProcessor
ParsableProcessor SomeProcessor
(Processor a, ParsableArguments (ArgumentsOf a)) => ParsableProcessor (StdProcessor a)
(Arguments arg, ComplexityProof res, ParsableArguments arg) => ParsableProcessor (Custom arg res)

Existentially Quantified Processors, Instances and Proofs

data SomeProcessor

Existential quantification of ParsableProcessor.

Constructors

forall p . ParsableProcessor p => SomeProcessor p

Instances

Typeable SomeProcessor
PrettyPrintable SomeProcessor
ParsableProcessor SomeProcessor
Processor SomeProcessor
Show (InstanceOf SomeProcessor)
Typeable (InstanceOf SomeProcessor)
Processor p => EQuantified (InstanceOf p) (InstanceOf SomeProcessor)

someProcessor :: (ComplexityProof (ProofOf p), ParsableProcessor p) => p -> SomeProcessor

Constructor for SomeProcessor.

data SomeInstance

Existential quantification of Processor p => InstanceOf p.

Constructors

forall p . Processor p => SomeInstance (InstanceOf p)

someInstance :: forall p. (ComplexityProof (ProofOf p), Processor p) => InstanceOf p -> InstanceOf SomeProcessor

Constructor for InstanceOf SomeProcessor.

data SomeProof

Existential quantification of ComplexityProof.

Constructors

forall p . ComplexityProof p => SomeProof p

Instances

ComplexityProof SomeProof

someProof :: ComplexityProof p => p -> SomeProof

Constructor for SomeProof

someProofNode :: Processor p => InstanceOf p -> Problem -> ProofOf p -> Proof SomeProcessor

Constructor for a proof node of SomeProcessor

solveBy :: (Processor a, SolverM m) => Problem -> InstanceOf a -> m SomeProof

Same as solve but wraps the resulting proof into SomeProof.

Any Processor

data AnyProcessor

AnyProcessor implements a choice of processors, i.e., a list of processors. AnyProcessors are mainly used for parsing. The InstanceOf an any procesessor is an instance of one of its elements.

toProcessorList :: AnyProcessor -> [SomeProcessor]

Extract the list of processors from an AnyProcessor.

fromProcessorList :: [SomeProcessor] -> AnyProcessor

Construct an AnyProcessor from a list of processors.

none :: AnyProcessor

The empty AnyProcessor.

(<|>) :: (ComplexityProof (ProofOf p), ParsableProcessor p) => p -> AnyProcessor -> AnyProcessor

Add a processor to an AnyProcessor.

(<++>) :: AnyProcessor -> AnyProcessor -> AnyProcessor

Append operation on AnyProcessors.

The Solver Monad

class MonadIO m => SolverM m where

The interface for a solver monad, i.e., the monad under within an instance of a processor tries to solve the complexity problem. Minimal definition is: runSolver, mkIO and satSolver.

Associated Types

type St m

some state

Methods

runSolver :: St m -> m a -> IO a

construct an IO monad from a solver monad, when given initial state

mkIO :: m a -> m (IO a)

construct a IO monad from the given solver monad. This is require mainly for concurrent execution

satSolver :: m SatSolver

return the SatSolver

solve :: Processor proc => InstanceOf proc -> Problem -> m (ProofOf proc)

This method can be used to wrap method solve_ from Processor

solvePartial :: Processor proc => InstanceOf proc -> SelectorExpression -> Problem -> m (PartialProof (ProofOf proc))

This method can be used to wrap method solvePartial_ from Processor

Instances

SolverM StdSolverM	Standard Implementation for solver monad
SolverM m => SolverM (LoggingSolverM m)

data SatSolver

Representation of a SAT-solver. Currently, only minisat (cf. http://minisat.se) is supported.

Constructors

MiniSat FilePath

Show AnyProcessor
Typeable AnyProcessor
ParsableProcessor AnyProcessor
Processor AnyProcessor
ParsableArgument Processor
Show (InstanceOf AnyProcessor)
Typeable (InstanceOf AnyProcessor)
(Transformer t, ParsableArguments (ArgumentsOf t)) => Describe (Transformation t AnyProcessor)