User Documentation

Ctrl is invoked from the command-line. You run it by typing:

        ./ctrl <benchmark>

Here, the benchmark is a file with the extension .ctrs, following the examples in the examples/ directory.

Parts of a .ctrs file

THEORY
List here a single file in the theories/ directory, which describes the theory symbols and interpretation as described below.
LOGIC
The theory file provides a translation to SMT-LIB format, and similarly the logic provides an SMT-LIB logic, which is passed to the SMT-solver when rewriting terms. Be aware that the more advanced analyses sometimes introduce quantifiers, if the logic permits this (that is, if the name of the logic does not start with QF_). This is likely to make Ctrl stronger, so if possible, use as powerful a logic over the theory supplied as the SMT-solver can handle.
SOLVER
The path to the SMT-solver executable, seen from the location of the program. Alternatively, you can use internal to indicate that Ctrl should use its own basic solving optimisations before passing on the query to intsolver, an SMT-solver which is guaranteed to accept all integer queries. At the moment, internal is only supported for systems over the core and ints theories. When using the internal solver, Ctrl itself will derive a suitable logic. If no solver is supplied, then this will use smtsolver, the default SMT-solver in the top directory (which is Z3 unless you replace it by a different file). The smtsolver solver is also used by intsolver and arrsolver.
SIGNATURE
The term symbols (elements of Σterms). Supply all term symbols, seperated by commas or semi-colons, and including values you wish to accept as (part of) terms. Generally, terms containing non-term symbols are seen as intermediate terms in a calculation, whereas terms fully built from symbols in Σterms are the structures of interest. You may omit the type declarations, supplying a list such as sum, sum1, u, !INTEGER;, if types can be derived automatically; if not, just supply declarations for some or all symbols, e.g.:
    err : result ;
    return ;
    strlen ;
    u : IntArray * Int => result ;
    !ARRAY!Int ;
Note the inclusion of the values given by !ARRAY!Int. This is further explained in the documentation on theory files below. It is not necessary to include values in the term signature (when they have already been included in the theory signature), but it does no harm.
RULES
The rules, in a semi-colon separated list. Each rule has the from left -> right [constraint].
NON-STANDARD
A rule is non-standard if its left-hand side contains theory symbols other than values. This is typically not intended (since for instance f(x + y) does not match f(3)), so such rules will cause an error unless you specify, after the RULES section, the NON-STANDARD keyword.
IRREGULAR
Like NON-STANDARD, IRREGULAR is a single keyword. Specify this if your rules are not regular, that is, if some constraints contain variables which do not occur in the left-hand side of the rules.
QUERY
The problem you want Ctrl to solve. This should have one of the following forms:
  • normal form term
    reduces term to normal form in an innermost way, showing you all the intermediate steps (will likely hang if term admits an infinite reduction)
  • reduce constrained term [constraint]
    reduces the given constrained term as far as we can
  • confluence
    tries to decide whether the system is confluent, and answers YES, NO or MAYBE (together with a reasoning)
  • termination
    tries to decide whether the system is terminating, and answers YES, NO or MAYBE (together with a reasoning)
  • equivalence term1 -><- term2 [constraint]
    tries to decide whether term1 and term2 can be reduced to each other, using (→ ∪ ←)*. Warning: this may well take a while.
  • user-equivalence term1 -><- term2 [constraint]
    launches an interactive editor where you can use standard commands to prove equivalence of the given two terms; this is essentially a user interface to equivalence.
  • print-simplification [list] or simplification [list]
    prints a variation of the given LCTRS where rules are combined where possible and sometimes arguments are removed; list
    • is a sequence of space-separated symbols whose declaration must not be modified
  • do_simplify [list] and action
    derives simplification [list] and then continues as though QUERY action was requested for the resulting LCTRS
END OF FILE
If you put this tag in, then everything following the tag will be ignored, enabling for instance an explanation of the purpose of the benchmark.

Writing a theory file

Aside from the systems describing the LCTRS term signatures and rules, the theory signature Σtheory and the interpretation mappings 𝓘 and 𝓙 must be provided. Now, the interpretation is given by SMT-LIB; we support only theories for which SMT-solvers exists (although in the case of arrays with size, such a solver is supplied by us, along with Ctrl). The signature is specified in the theory files, which are included in all lctrs files. All theory files reside in the theories/ directory. For a good example, look at core.thr and ints.thr, which should be included in any release. Such files specify:

INCLUDE
Includes all symbols and settings from the given theory file; used for instance in ints.thr to include also the core theory.
DECLARE
The symbols in Σtheory, complete with their sort declaration (infix association and priority may also be provided, for easier use of symbols in constraints. For example, in the core file,     /\ : Bool * Bool => Bool (l-infix 50) ;
indicates that /\ is a binary infix symbol which takes two arguments of sort Bool and returns an argument of sort Bool, and that a /\ b /\ c should be read as (a /\ b) /\ c. Additionally,
    xor : Bool * Bool => Bool (l-infix 47) ;
defines another infix symbol of lower priority, so a /\ b xor c is read as (a /\ b) xor c.
Polymorphism is allowed here, indicating a theory symbol of which versions exists for all sorts. For example,
    = : <?A> => Bool (infix 60) ;
declares a symbol =, which can take as many arguments as you want (this is indicated by the <...> brackets), as long as they are all of the same sort, which may be an arbitrary sort (?A is a polymorphic variable, which may be instantiated by anything). Writing for instance 1 = 1 = 2 creates the term =Int(1,1,2).

Ctrl will automatically assume that any symbol declared with a non-functional type is a value. There are three ways to declare an infinite number of values at once:
  • !INTEGER includes all integer symbols, i.e. 0, 1, -37 and so on, as values of the declared sort
  • !ARRAY!<sort> includes all expressions of the form {x1:...:xn} where all xi are values of sort <sort> as values of the declared sort; spaces are not allowed to occur (for example, !ARRAY!Int : Column would include {0:1:-37} as a value of sort Column, and, having this, !ARRAY!Column : Matrix would include {{0:1}:{-37}:{}} as a value of sort Matrix.
  • !MIXED!<open>!<close> includes all strings starting with the string <open> and ending with the string <close> as values of the declared sort; for example, !MIXED!"!" : String would include "hello" and "3.14" as values of sort String. Importantly, these values are passed to the SMT-solver without the bracketing.
WELL-FOUNDED
Lists symbols which are guaranteed to define well-founded relations, i.e. binary symbols R such that no infinite sequence x1, x2, ... exists where each xi R xi+1. It is not compulsary to include all well-founded relations in the theory here, but is is recommended, since this makes the termination prover significantly more powerful.
CHAIN
The CHAIN keyword gives another layer of syntactical sugar, allowing for instance x > y >= a to be translated to x > y /\ y >= a.
SMT-RENAMINGS
A list of entries fancy name -> name according to SMT-LIB. If a function is not in the list, then its interpretation is simply the SMT-LIB function of the same name.
SMT-TRANSLATIONS
A list of entries symbol(x1, ..., xn) -> term where all xi are distinct variables, and term is a term over these variables. This gives a more powerful form of SMT-RENAMINGS, allowing the theory designer to specify exactly how a term headed by a given symbol should be passed to the SMT-solver. This makes it possible to define custom symbols; for example, to strengthen termination proving, we can define a custom symbol >! which is well-founded; its lack of support by common SMT-solvers is solved by automatically translating it to the relation λx y.x > y /\ x >= 0.

Further notes

Three default SMT-solvers are supplied with the program, all of which can be replaced by other SMT-solvers which have similar functionality: