Complexity Integer Term Rewrite Systems are a special form of integer term rewrite systems that is used for complexity analysis. For further details, we refer to our paper at TACAS 2014. Each cint file consists of four parts:
(GOAL COMPLEXITY), specifying that the goal of this file is complexity analysis.
(STARTTERM (FUNCTIONSYMBOLS start)). Currently, only one state (e.g., start) may be specified as a start state.
(VAR A B C D)declares the variables
(RULES ...). Each transition consists of a start state, an arrow (
->), a list of end states (wrapped in
Com_k(...), where k is the number of end states), and an optional constraint separated by
:|:from the rest of the state. The start state is given in the form
ith variable of the program (for
1 <= i <= n). Each of the end states is given as
tiis the value of the
ith variable after evaluating the transition (for
1 <= i <= n). All values and constraints have to be given as polynomials over the variables in the
(VAR ...)section. Variables occurring in an end state, but not in the start state are interpreted as an arbitrary integer.