tct-trs

This package is part of the Tyrolean Complexity Tool (TcT) and provides automatic complexity analysis of Term Rewrite Systems (TRSs).

This repository provides the tct-trs library as well as the tct-trs executable.

Requirements

Executables:

• Glasgow Haskell Compiler, version 7.10
• minismt, version 0.6 or z3, version 4.3
  • We recommend using minismt. If you want to use z3, see how to set up z3.

Other packages:

• slogic
• tct-core
• tct-common
• term-rewriting-xml

The tool is only tested under GNU/Linux.

Installation

Using Stack

We recommend using stack with the accompanied stack-XXX.yaml file. To build and install the package run following command:

stack install tct-trs

Using Cabal

For building via cabal/cabal-install, make sure that you have ghc and cabal. To build and install the package run following commands:

mkdir tct-bundle
cd tct-bundle
git clone https://github.com/ComputationWithBoundedResources/slogic
git clone https://github.com/ComputationWithBoundedResources/tct-core
git clone https://github.com/ComputationWithBoundedResources/tct-common
git clone https://github.com/ComputationWithBoundedResources/tct-trs
git clone https://github.com/ComputationWithBoundedResources/term-rewriting-xml
cabal install **/*.cabal tct-trs

Example Usage

The installation provides an executable tct-trs.

tct-trs --complexity rci examples/RaML/minsort.raml.trs

For full options, run tct-trs --help.

FAQ

Q:How to set up z3?

To use z3, you have to update the default configuration and re-install the executable.

module Main (main) where

import Tct.Trs.Config

main :: IO ()
main = trs $ trsConfig `setSolver` ("z3",[])