AProVE Help: Complexity Integer Term Rewrite System

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:

• The declaration (GOAL COMPLEXITY), specifying that the goal of this file is complexity analysis.
• The list of start states (STARTTERM (FUNCTIONSYMBOLS start)). Currently, only one state (e.g., start) may be specified as a start state.
• The declaration of all variables that are used in the remaining program. This includes not only the variables representing the state of the program, but also all variables that are only used to define constraints. The list of variables is space-separated. Hence, the line (VAR A B C D) declares the variables A, B, C, and D.
• Finally, the list of transitions, given in the statement (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 f(X1,...,Xn) where Xi is the ith variable of the program (for 1 <= i <= n). Each of the end states is given as f(t1,...,tn) where ti is 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.