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

Tct.Interactive

Contents

Loading Problems
- Loading Problems with Respect to a Complexity Category
The Proof State
History Functionality
Changing the behaviour of TcTi
Help and Documentation
Miscellaneous Utilities
Accessing to the Configuration
Silent Versions
Misc

Description

This section describes the interactive interface of TcT (TcT-i for short), for usage information on the command line interface, please refer to Tct. Since TcT-i relies on the Interpreter ghci from the Glasgow Haskell Compiler (http://www.haskell.org/ghc/), the interactive interface is only available if ghci is present on your system. As explained in Tct.Configuration, TcT can be easily customized. TcT-i makes use of this by loading the configuration file, usually located in ${HOME}/.tct/tct.hs.

The interactive interface is invoked from the command line as follows:

>>> tct -i
GHCi, version 7.4.1: http://www.haskell.org/ghc/  :? for help
...
Loading package tct-2.0 ... linking ... done.
[1 of 1] Compiling Main             ( tct.hs, interpreted )
Ok, modules loaded: Main.
.
  Welcome to the TcT
  ------------------
.  
  This is version 2.0 of the Tyrolean Complexity Tool.
.  
  (c) Martin Avanzini <martin.avanzini@uibk.ac.at>,
      Georg Moser <georg.moser@uibk.ac.at>, and
      Andreas Schnabl <andreas.schnabl@uibk.ac.at>.
.  
  This software is licensed under the GNU Lesser General Public
  License, see <http://www.gnu.org/licenses/>.
.  
  Don't know how to start? Type 'help'.
TcT>

As can be readily seen from the output, this command starts a customized version of ghci. In particular all the functionality of ghci is available, cf. http://www.haskell.org/ghc/docs/latest/html/users_guide/ghci.html on general usage information of ghci.

Synopsis

Loading Problems

A complexity problem can be loaded into TcT-i by invoking the load action. This action accepts a file path refering to either a file in the old tpdb-format (cf. http://www.lri.fr/~marche/tpdb/format.html) or in the new xml-based format (cf. http://dev.aspsimon.org/xtc.xsd). Examples are available in the directory examples in the software distribution, or the current termination problem database (http://termcomp.uibk.ac.at/status/downloads/tpdb-current-exported.tar.gz).

load :: FilePath -> IO ()

Loads a complexity problem from the given file.

>>> load "examples/quot.trs"
--------------------------------------------------------------------
Selected Open Problems:
-----------------------
Strict Trs:
  {  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
   , quot(0(), s(y)) -> 0()
   , minus(s(x), s(y)) -> minus(x, y)
   , minus(x, 0()) -> x}
StartTerms: basic terms
Strategy: none

Loading Problems with Respect to a Complexity Category

For convenience, TcT-i provides the following modifications of load, matching the categories of the complexity division of the internation termination competition http://termination-portal.org/wiki/Complexity.

loadRC :: FilePath -> IO ()

Same as load, but overwrites strategy and start-terms in order to match a runtime-complexity problem.

loadIRC :: FilePath -> IO ()

Same as load, but overwrites strategy and start-terms in order to match a innermost runtime-complexity problem.

loadDC :: FilePath -> IO ()

Same as load, but overwrites strategy and start-terms in order to match a derivational-complexity problem.

loadIDC :: FilePath -> IO ()

Same as load, but overwrites strategy and start-terms in order to match a innermost derivational-complexity problem.

The Proof State

During the interactive session, TcT-i maintains a so called proof state, which is basically a list of open complexity problems together with some information on how this state was obtained. In order to prove upper bounds on complexity problem, this proof state needs to be reduced to the empty list.

To see the list of open problems, use the action state. To obtain a proof, use the action proof. To simplify the state use the action apply as described below.

Applying Complexity Techniques

The proof state is modified by applying instance of processors. A processor is the TcT representation of a complexity technique. Processors are separated for historical reasons into standard-processors and transformers.

Processors are usually parameterised by some arguments, for instance the dependency pair processor dependencyPairs accepts a flag usetuples that defines whether dependency tuples should be employed. Processors with instantiated arguments are called instances of processors. When applying a processor, TcT-i will prompt the user for any necessary arguments so it can construct the corresponding instance.

Predefined processors are available in module Tct.Processors. Instances can be constructed also directly, using the functionality provided in Tct.Instances. This module defines also a wealth of combinators and is considered the preferred way for dealing with processors.

apply :: Apply p => p -> IO ()

Type apply m for some technique m to simplify the list of selected open problems using m. The proof state is updated by replacing each open problem with the result of applying m. TcT-i displays the proof fragment resulting from applying m to each selected open problem, and finally redisplays the new proof state.

The following example demonstrates the application of dependency pairs. Note that when a processor from Tct.Processors is applied, TcT-i might ask for further flags.

>>> apply Processor.dependencyPairs
Input arguments for dp
* 'usetuples'
  This argument specifies whether dependency tuples instead of pairs
  should be used.
  Synopsis: On|Off
  Use the default value 'Off'? Enter 'yes' or 'no', default is 'yes':
  > 
  Problem 1:
  ----------
1) Dependency Pairs [OPEN]:
  ---------------------------
.  
    We consider the following problem:
      Strict Trs:
        {  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
         , quot(0(), s(y)) -> 0()
         , minus(s(x), s(y)) -> minus(x, y)
         , minus(x, 0()) -> x}
      StartTerms: basic terms
      Strategy: none
.
    We have computed the following dependency pairs
.
      Strict DPs:
        {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
         , quot^#(0(), s(y)) -> c_2()
         , minus^#(s(x), s(y)) -> minus^#(x, y)
         , minus^#(x, 0()) -> x}
.
    Generated New Problems:
    -----------------------
.
      * Problem 1.1)
          Strict DPs:
            {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
             , quot^#(0(), s(y)) -> c_2()
             , minus^#(s(x), s(y)) -> minus^#(x, y)
             , minus^#(x, 0()) -> x}
          Strict Trs:
            {  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
             , quot(0(), s(y)) -> 0()
             , minus(s(x), s(y)) -> minus(x, y)
             , minus(x, 0()) -> x}
          StartTerms: basic terms
          Strategy: none
.      
      1.1) Open Problem [OPEN]:
      -------------------------
        We consider the following problem:
          Strict DPs:
            {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
             , quot^#(0(), s(y)) -> c_2()
             , minus^#(s(x), s(y)) -> minus^#(x, y)
             , minus^#(x, 0()) -> x}
          Strict Trs:
            {  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
             , quot(0(), s(y)) -> 0()
             , minus(s(x), s(y)) -> minus(x, y)
             , minus(x, 0()) -> x}
          StartTerms: basic terms
          Strategy: none
.
  ----------------------------------------------------------------------
  Selected Open Problems:
  -----------------------
    Strict DPs:
      {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
       , quot^#(0(), s(y)) -> c_2()
       , minus^#(s(x), s(y)) -> minus^#(x, y)
       , minus^#(x, 0()) -> x}
    Strict Trs:
      {  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
       , quot(0(), s(y)) -> 0()
       , minus(s(x), s(y)) -> minus(x, y)
       , minus(x, 0()) -> x}
    StartTerms: basic terms
    Strategy: none
  ----------------------------------------------------------------------

The next example shows the application of instances, in combination with the combinators from Tct.Instances.

>>> :module +Tct.Instances
>>> apply $ try removeWeakSuffix >>> try usableRules
...
----------------------------------------------------------------------
Selected Open Problems:
-----------------------
  Strict DPs:
    {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
     , quot^#(0(), s(y)) -> c_2()
     , minus^#(s(x), s(y)) -> minus^#(x, y)
     , minus^#(x, 0()) -> x}
  Strict Trs:
    {  minus(s(x), s(y)) -> minus(x, y)
     , minus(x, 0()) -> x}
  StartTerms: basic terms
  Strategy: none
----------------------------------------------------------------------

class Apply p

Instances

Processor p => Apply (InstanceOf p)
(ParsableArguments (ArgumentsOf p), Processor p) => Apply (StdProcessor p)
Transformer t => Apply (TheTransformer t)
(ParsableArguments (ArgumentsOf t), Transformer t) => Apply (Transformation t sub)

Instance of the class apply can be used to modify the list of (selected) open problems using the action apply.

Values of type StdProcessor p and Transformation t sub can be found in module Tct.Processors. Values of type InstanceOf p and TheTransformer t for (standard) processors p and transformations t, i.e., instances of processors, are collected in Tct.Instances.

Inspecting the State

As explained above, TcT-i retains a list of open problems and proof information. These are accessible anytime using the actions state and proof.

state :: IO ()

This action prints the current proof state.

>>> state
----------------------------------------------------------------------
Selected Open Problems:
-----------------------
  Strict DPs:
    {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
     , quot^#(0(), s(y)) -> c_2()
     , minus^#(s(x), s(y)) -> minus^#(x, y)
     , minus^#(x, 0()) -> x}
  Strict Trs:
    {  minus(s(x), s(y)) -> minus(x, y)
     , minus(x, 0()) -> x}
  StartTerms: basic terms
  Strategy: none
----------------------------------------------------------------------

The output shows the example from load, already simplified using weak dependency pairs, and further processed by try removeTails >>> try usableRules

proof :: IO ()

This action prints the current proof tree.

>>> proof
1) Dependency Pairs [OPEN]:
  ---------------------------
.  
    We consider the following problem:
      Strict Trs:
        {  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
         , quot(0(), s(y)) -> 0()
         , minus(s(x), s(y)) -> minus(x, y)
         , minus(x, 0()) -> x}
      StartTerms: basic terms
      Strategy: none
.
    We have computed the following dependency pairs
.
      Strict DPs:
        {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
         , quot^#(0(), s(y)) -> c_2()
         , minus^#(s(x), s(y)) -> minus^#(x, y)
         , minus^#(x, 0()) -> x}
.
    Generated New Problems:
    -----------------------
.
      * Problem 1.1)
          Strict DPs:
            {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
             , quot^#(0(), s(y)) -> c_2()
             , minus^#(s(x), s(y)) -> minus^#(x, y)
             , minus^#(x, 0()) -> x}
          Strict Trs:
            {  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
             , quot(0(), s(y)) -> 0()
             , minus(s(x), s(y)) -> minus(x, y)
             , minus(x, 0()) -> x}
          StartTerms: basic terms
          Strategy: none
.
    1.1) removetails >>> ... [OPEN]:
    --------------------------------
.
      We consider the following problem:
        Strict DPs:
          {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
           , quot^#(0(), s(y)) -> c_2()
           , minus^#(s(x), s(y)) -> minus^#(x, y)
           , minus^#(x, 0()) -> x}
        Strict Trs:
          {  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
           , quot(0(), s(y)) -> 0()
           , minus(s(x), s(y)) -> minus(x, y)
           , minus(x, 0()) -> x}
        StartTerms: basic terms
        Strategy: none
.
      The processor is inapplicable since the strict component of the
      input problem is not empty
.
      We apply the transformation 'usablerules' on the resulting sub-problem(s):
.
        We consider the problem
.
        Strict DPs:
          {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
           , quot^#(0(), s(y)) -> c_2()
           , minus^#(s(x), s(y)) -> minus^#(x, y)
           , minus^#(x, 0()) -> x}
        Strict Trs:
          {  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
           , quot(0(), s(y)) -> 0()
           , minus(s(x), s(y)) -> minus(x, y)
           , minus(x, 0()) -> x}
        StartTerms: basic terms
        Strategy: none
.
        We replace strict/weak-rules by the corresponding usable rules:
.
          Strict Usable Rules:
            {  minus(s(x), s(y)) -> minus(x, y)
             , minus(x, 0()) -> x}
.
        The consider problem is replaced by
.
        1) Strict DPs:
             {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
              , quot^#(0(), s(y)) -> c_2()
              , minus^#(s(x), s(y)) -> minus^#(x, y)
              , minus^#(x, 0()) -> x}
           Strict Trs:
             {  minus(s(x), s(y)) -> minus(x, y)
              , minus(x, 0()) -> x}
           StartTerms: basic terms
           Strategy: none
. 
      Generated New Problems:
      -----------------------
.
        * Problem 1.1.1)
            Strict DPs:
              {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
               , quot^#(0(), s(y)) -> c_2()
               , minus^#(s(x), s(y)) -> minus^#(x, y)
               , minus^#(x, 0()) -> x}
            Strict Trs:
              {  minus(s(x), s(y)) -> minus(x, y)
               , minus(x, 0()) -> x}
            StartTerms: basic terms
            Strategy: none
.
      1.1.1) Open Problem [OPEN]:
      ---------------------------
.
        We consider the following problem:
          Strict DPs:
            {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
             , quot^#(0(), s(y)) -> c_2()
             , minus^#(s(x), s(y)) -> minus^#(x, y)
             , minus^#(x, 0()) -> x}
          Strict Trs:
            {  minus(s(x), s(y)) -> minus(x, y)
             , minus(x, 0()) -> x}
          StartTerms: basic terms
          Strategy: none

The output precisely reflects how the current proof state was obtained from the initial state. Since state contains still open problems, the proof also open subproblems, in this case subproblem 1.1.1). From the output we can also see that removeTails is inapplicable. The reason is that removeTails is unsound if the strict trs from the problem is not empty. TcT will never apply processors in an unsound setting!

as proof, but output to given file

writeProof :: FilePath -> IO ()

Extracting the State

Beside showing the current state and the proof constructed so far, TcT-i also defines actions for extractions.

problems :: IO [Problem]

Displays and returns the list of selected open problems.

>>> problems
Problem 1:
. 
  Strict DPs:
  {  quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
  , quot^#(0(), s(y)) -> c_2()
  , minus^#(s(x), s(y)) -> minus^#(x, y)
   , minus^#(x, 0()) -> x}
Strict Trs:
  {  minus(s(x), s(y)) -> minus(x, y)
   , minus(x, 0()) -> x}
StartTerms: basic terms
Strategy: none
.
[Problem { startTerms = ...
         , strategy   = ...
         , variables  = ...
         , signature  = ...
         , strictDPs  = Trs {rules = ...} 
         , strictTrs  = Trs {rules = ...} 
         , weakDPs    = Trs {rules = ...} 
         , weakTrs    = Trs {rules = ...}}
]

Problems are defined in the accompanying term rewriting library (cf. http://cl-informatik.uibk.ac.at/software/tct/projects/termlib/). The module Repl, collecting most of the functionality of the term rewriting library, is imported qualified as module TR. Cf. http://cl-informatik.uibk.ac.at/software/tct/projects/termlib/docs/Termlib-Repl.html for documentation of the module Repl.

wdgs :: IO [DG]

This action displays the weak dependency graphs of all selected problems. If dot from the GraphViz project (c.f. http://www.graphviz.org/) is installed, then a SVG-picture is rendered in 'dg.svg' of the current working directory.

cwdgs :: IO [CDG]

This action displays the weak congruence dependency graphs of all selected problems. To produce an SVG-picture, use the procedure wdgs that draws weak dependency graphs, but also shows congruence classes.

uargs :: IO [UsablePositions]

This action displays the usable argument positions of the selected problems.

selectedRules :: ExpressionSelector -> IO [SelectorExpression]

This action displays the application of a rule-selector.

Selecting and Unselecting Problems

Sometimes it is convenient to consider a sublist of the list of open Problems. To restrict the list of problems considered by apply, use the procedures select and unselect, in combination with a Selector.

class Selector i

Instances

Selector SelectAll
Integral n => Selector [n]
Selector s => Selector (SelectInv s)
Selector (Problem -> Bool)

Instances of this class can be used in combination with select. Note that Selector [Int] selects according to the problem number as recorded in the state (c.f. procedure state).

select :: Selector sel => sel -> IO ()

Select problems from the proof state according to the given Selector.

Consider the following state that is obtained from the running example, after applying pathAnalysis.

>>> state
--------------------------------------------------------------------
Selected Open Problems:
-----------------------
  1) Strict DPs: {minus^#(s(x), s(y)) -> minus^#(x, y)}
     Strict Trs:
       {  minus(s(x), s(y)) -> minus(x, y)
        , minus(x, 0()) -> x}
     StartTerms: basic terms
     Strategy: none
.
  2) Strict DPs: {minus^#(x, 0()) -> x}
     Strict Trs:
       {  minus(s(x), s(y)) -> minus(x, y)
        , minus(x, 0()) -> x}
     Weak DPs: {minus^#(s(x), s(y)) -> minus^#(x, y)}
     StartTerms: basic terms
     Strategy: none
.
  3) Strict DPs: {quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))}
     Strict Trs:
       {  minus(s(x), s(y)) -> minus(x, y)
        , minus(x, 0()) -> x}
     StartTerms: basic terms
     Strategy: none
.
  4) Strict DPs: {quot^#(0(), s(y)) -> c_2()}
     Strict Trs:
       {  minus(s(x), s(y)) -> minus(x, y)
        , minus(x, 0()) -> x}
     Weak DPs: {quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))}
     StartTerms: basic terms
     Strategy: none
.
>>> select [1,3]
--------------------------------------------------------------------
Unselected Open Problems:
-------------------------
  2) Strict DPs: {minus^#(x, 0()) -> x}
     Strict Trs:
       {  minus(s(x), s(y)) -> minus(x, y)
        , minus(x, 0()) -> x}
     Weak DPs: {minus^#(s(x), s(y)) -> minus^#(x, y)}
     StartTerms: basic terms
     Strategy: none
.
  4) Strict DPs: {quot^#(0(), s(y)) -> c_2()}
     Strict Trs:
       {  minus(s(x), s(y)) -> minus(x, y)
        , minus(x, 0()) -> x}
     Weak DPs: {quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))}
     StartTerms: basic terms
     Strategy: none
.
Selected Open Problems:
-----------------------
  1) Strict DPs: {minus^#(s(x), s(y)) -> minus^#(x, y)}
     Strict Trs:
       {  minus(s(x), s(y)) -> minus(x, y)
        , minus(x, 0()) -> x}
     StartTerms: basic terms
     Strategy: none
.
  3) Strict DPs: {quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))}
     Strict Trs:
       {  minus(s(x), s(y)) -> minus(x, y)
        , minus(x, 0()) -> x}
     StartTerms: basic terms
     Strategy: none

unselect :: Selector sel => sel -> IO ()

Inverse of select. The example of select can also be obtained by typing

>>> unselect [2,4]

data SelectAll

Instances

Selector SelectAll

Special selector to select all open problems.

data SelectInv s

Instances

Selector s => Selector (SelectInv s)

Special selector to inverse a selection.

Changing the Initial Problem

The following procedures change the initial problem. Note that in order to guarantee soundness, any progress will undone. However the procedure undo allows to revert a change to the initial problem.

setRC :: IO ()

This action overwrites strategy and start-terms in order to match a runtime-complexity problem.

setIRC :: IO ()

This action overwrites strategy and start-terms in order to match a innermost runtime-complexity problem.

setDC :: IO ()

This action overwrites strategy and start-terms in order to match a derivational-complexity problem.

setIDC :: IO ()

This action overwrites strategy and start-terms in order to match a innermost derivational-complexity problem.

addRuleFromString :: String -> IO ()

This action adds the given rule to the input problem. Terms are parsed using the simple grammar

```
RULE -> TERM SEP TERM
```
TERM -> SYM([TERM]*) | SYM.

Here SEP is either -> or ->=. In the former case, the parsed rule is considered a strict rule, in the latter case a weak rule. SYM is either the special name COM, or any character not matchin (),"-=. If the root of the left hand side has ^ as suffix, then the rule is considered a dependency pair (these dependency pair suffixes are stripped off by the parser). The special symbol COM is replaced by a fresh compound symbol.

deleteRuleFromString :: String -> IO ()

This action deletes the given rule from the input problem. See addRuleFromString for grammar.

modifyInitialWith :: (Problem -> Problem) -> IO ()

This action modifies the initial problem according to given function.

History Functionality

TcT provides basic history functionality, in order to undo previous actions. This functionality covers all actions that modify the state.

reset :: IO ()

This action resets the proof state to the initially loaded system.

undo :: IO ()

Undos the last modification of the proof state

Changing the behaviour of TcTi

When set to True, interactive mode will print proofs after execution of commands. This can be globally configured in your configuration by modifying interactiveShowProofs.

setShowProofs :: Bool -> IO ()

Help and Documentation

help :: IO ()

Displays a help message.

welcome :: IO ()

Displays a help message.

Prints a description of the given technique. In particular, describe accepts processors as defined in Processors.

>>> describe Processor.lmpo
.
Processor "lmpo":
-----------------
  This processor implements orientation of the input problem using
  'light multiset path orders',
  a technique applicable for innermost runtime-complexity analysis.
  Light multiset path orders are a miniaturisation of 'multiset path
  orders', restricted so that compatibility assesses polytime computability 
  of the functions defined.
  Further, it induces exponentially bounded innermost runtime-complexity.
.   
  Usage:
   lmpo [:ps [On|Off]] [:wsc [On|Off]]
.      
  Arguments:
   ps:
             If enabled then the scheme of parameter substitution is admitted,
             cf. http://cl-informatik.uibk.ac.at/~zini/publications/WST09.pdf
             how this is done for polynomial path orders.
             The default is set to 'On'.
. 
   wsc:
             If enabled then composition is restricted to weak safe composition.
.
For documentation concerning creation of instances, consult:
  http://cl-informatik.uibk.ac.at/software/tct/projects/tct/docs/Tct-Instances.html#v:lmpo

class Describe p where

Methods

describe :: p -> IO ()

Instances

(Processor p, ParsableArguments (ArgumentsOf p)) => Describe (ProcessorInstance p)
(Processor p, ParsableArguments (ArgumentsOf p)) => Describe (StdProcessor p)
(Transformer t, ParsableArguments (ArgumentsOf t)) => Describe (TheTransformer t)
(Transformer t, ParsableArguments (ArgumentsOf t)) => Describe (Transformation t AnyProcessor)

Instances of this class can be handled by the action describe.

Miscellaneous Utilities

pprint :: PrettyPrintable a => a -> IO ()

pretty-print objects.

processor :: (ParsableArguments (ArgumentsOf p), Processor p) => p -> IO (InstanceOf (StdProcessor p))

given a processor, construct an instance

termFromString :: String -> Problem -> IO (Term, Problem)

Parses a term from a string, with respect to the signature and variables from the given problem. See addRuleFromString for grammar.

ruleFromString :: String -> Problem -> IO (Rule, Problem)

Parses a rule from a string, with respect to the signature and variables from the given problem. See addRuleFromString for grammar.

Accessing to the Configuration

The TcT configuration file, usually residing in ${HOME}/.tct/tct.hs contains a definition config :: Config. In particular, TcT-i employs the field processors when it requires the list of available processors, for instance when parsing arguments. The configuration is accessible throught the following actions. Note that the configuration can be modified while running TcT-i.

getConfig :: IO Config

Returns the current configuration.

setConfig :: Config -> IO ()

Set the configuration.

modifyConfig :: (Config -> Config) -> IO ()

Modify the configuration according to the given function.

Silent Versions

wdgs' :: IO [DG]

problems' :: IO [Problem]

Misc

runTct :: StdSolverM a -> IO a