Confluence Competition


The format for logically constrained TRSs extends the MSTRS format, according to the following grammar:

      LCTRS ::= ( format LCTRS (:smtlib standard)? )
                    theory+ smt-def* sort-decl* fun-decl* rule*
   standard ::= identifier
     theory ::= ( theory smt-theory )
  sort-decl ::= ( sort identifier )
       sort ::= identifier | theory-sort
theory-sort ::= ( _ identifier+ )
    smt-def ::= ( define-fun identifier ( vars ) theory-sort formula )
   fun-decl ::= ( fun identifier type )
       type ::= sort | ( -> sort+ sort )
       rule ::= ( rule term term (:guard term)? (:var ( vars ))? )
       vars ::= (( identifier sort ))*
The option :smtlib standard in the format declaration specifies an SMT standard, e.g., 2.6 (SMT-LIB 2.6) as defined in this document. Supported versions and theories will be added over time. The smt-theory in the theory declaration specifies the theory symbols and types of the LCTRS theory part by importing an SMT theory smt-theory, defined in the specified SMT standard. This theory should be supported in an off-the-shelf SMT solver. Sensible examples can be found on the SMT-LIB site. In an LCTRS file, at least one theory is required.

The theory-sort in the sort declaration is used to declare sorts in an imported SMT theory such as (_ BitVec 32) that cannot be specified using an identifier. Furthermore, smt-def must adhere to the define-fun command of SMT-LIB, and formula must be an SMT-LIB formula (possibly a term) of the corresponding imported SMT theories. A formula is assumed to be an object consisting of theory symbols, variables and quantifiers. Note that logical connectives are considered theory symbols. Further note that identifier in formula does not have to be an ARI identifier. Theory symbols declared by define-fun must not conflict with other built-in theory symbols that can be used for the imported SMT theories even if they are not declared in the file.

The optional (local) variable declaration :var (vars) is mandatory in the case that sorts of variables cannot be inferred. For example, assuming the theory Ints, the variables x and y in (rule a b :guard (not (= x y))) can be of sort Bool or Int. In addition, identifier of theory symbols defined by define-fun and vars has to be an identifier in the specified SMT standard.

LCTRSs in the ARI Database

LCTRSs in the ARI database are assumed to adhere to the definition in the literature. For example, the left- and right-hand side of a constrained rule must have the same type. Below we specify further restrictions on the grammar constructs in the above format.

SMT-LIB versions declared by :smtlib standard

The declaration is mandatory for LCTRSs in the ARI database. Currently we support SMT-LIB 2.6:

   standard ::= 2.6

SMT-LIB theories declared by smt-theory

We disallow redundant declarations of theories: A theory can be declared at most once in a file, and if a theory T is declared then no subtheory of T can be declared. For 2.6 we allow

   smt-theory ::= Core | Ints | FixedSizeBitVectors | Reals | Reals_Ints
Theory Core is implicitly included by means of other theories, but when no (other) theory is declared, (theory Core) has to be specified. In addition, Reals and Ints cannot be used simultaneously (because of a conflict on the use of strings for integers). Instead, Reals_Ints is used. Note that both Reals and Ints are subtheories of Reals_Ints.

Theory sorts generated by theory-sort

For 2.6 we admit (_ BitVec n) with n > 0:

  theory-sort ::= Bool | Int | (_ BitVec posnumeral) | Real
   posnumeral ::= [1-9][0-9]*
The following theory sorts in the specified theories can be used:
theory theory sorts
Core Bool
Ints Bool,   Int
FixedSizeBitVectors Bool,   (_ BitVec n) with n > 0
Reals Bool,   Real
Reals_Ints Bool,   Real,   Int
Sorts declared by sort-decl should exclude these.


The specified theories admit the following values:

theory sort values grammar
Core Bool Boolean values valueBool ::= true | false
Ints Int integers valueInt ::= integer
FixedSizeBitVectors (_ BitVec n) n-bits bitvectors valueBitVec ::= #b[0-1]+ | #x[0-9 a-f A-F]+
Reals Real reals (and integers) valueRealInt ::= valueReal
Reals_Ints Real reals valueReal ::= decimal
Int integers valueInt ::= integer
Unlike the SMT-LIB 2.6 standard, we allow the direct specification of negative numbers:
  negnumeral ::= -[1-9][0-9]*
     numeral ::= 0 | posnumeral
     integer ::= numeral | negnumeral
     decimal ::= -?numeral.0*numeral 

Theory symbols

The specified theories admit the following theory symbols:

true,   false,   not,   =>,   and,   or,   xor,   =,   distinct,   ite
-,   +,   *,   div,   mod,   abs,   <=,   <,   >=,   >,   (_ divisible n) for n > 0,   and the values of valueInt
concat,   (_ extract i j) with ij ≥ 0,   bvnot,   bvneg,   bvand,   bvor,   bvadd,   bvmul,   bvudiv,   bvurem,   bvshl,   bvlshr,   bvult,   and the values of valueBitVec
-,   +,   *,   /,   <=,   <,   >=,   >,   and the values of valueRealInt
-,   +,   *,   div,   mod,   abs,   <=,   <,   >=,   >,   (_ divisible n) with n > 0,   /, to_real,   to_int,   is_int,   and the values of valueReal and valueInt
In addition, the theories Ints, FixedSizeBitVectors, Reals and Reals_Ints contain all theory symbols of Core.

Some theory symbols are (ad-hoc) polymorphic. For SMT-LIB 2.6

We distinguish (ad-hoc) polymorphic symbols depending on their sorts. For example,

We consider non-simple symbols such as (_ divisible n) as theory symbols, but they cannot be used in rewrite rules. To use a non-simple symbol it must be declared by define-fun. For example, to use (_ divisible 2) in a rewrite rule, we can use (define-fun divisible2 ((x Int)) Bool ((_ divisible 2) x)).

Theory symbols introduced by a theory extension are not allowed. For example, bvsub cannot be used because it is defined in QF_BV rather than FixedSizeBitVectors.

Theory variables and user-defined theory symbols

A theory variable is a variable appearing in a formula or in a term (which may be sent to an SMT solver), i.e.,

A user-defined theory symbol is a function symbol defined in a smt-def declaration. User-defined theory symbols cannot be values and thus must take at least one argument. For (define-fun f (vars) theory-sort formula), any user-defined theory symbol in formula must be defined before f. A guard term is a term t appearing in :guard t.

Formulas sent to an SMT solver have to be consistent with the allowed identifiers of the SMT-LIB language. For this reason we allow only simple symbol as identifiers. Furthermore, theory variables and user-defined theory symbol cannot be reserved words of the SMT-LIB language specified by :smtlib version. For SMT-LIB 2.6 the reserved words recognized in the ARI database are

as   let   forall   exists   match   !   _
in addition to the values and theory symbols listed above. Values and theory symbols of unsupported theories are also reserved words.

Associativity, chainability, and pairwise property of theory symbols

Some theory symbols in SMT-LIB are left-associative, right-associative chainable, or have the pairwise property. For example, and is left-associative, = is chainable, and distinct has the pairwise property, i.e., we can write (and t1 t2 t3 ...), (= t1 t2 t3 ...), and (distinct t1 t2 t3 ...). These properties make the corresponding symbols variadic, which is considered as syntactic sugar.

The arity of function symbols in the left- and right-hand sides of rewrite rules have to be consistent, i.e., we do not allow variadic function symbols. For example, the number of arguments of and in the left- and right-hand sides of rewrite rules is two. However, for convenience, we allow theory symbols with the left-associative, right-associative, chainable, or pairwise properties to be variadic in formulas and guard terms. In SMT-LIB 2.6 the theory symbols

and   or   xor   bvand   bvor   bvadd   bvmul   - (binary)   +   *   div   /
are left-associative,
is right-associativity,
=   <=   <   >=   >
are chainable, and
has the pairwise property.

Formulas for formula

The ARI database restricts formula to variables, (possibly user-defined) theory symbols, and quantifiers:

   formula ::= identifier | theory-symbol | ((identifier | theory-symbol) formula+ )
             | ( (forall | exists) ( vars ) formula )
Note that formula may be a term.

Local variables declared in :var (vars)

Variables can be declared only once in the variable sequence vars in :var (vars). A variable occurring in a constrained rewrite rule must be declared if it occurs as a direct argument of a (possibly ad-hoc) polymorphic predicate. For example, assuming the theory Ints, the types of the variables x, y and z in

(rule (f (= x y) x) z :guard (= z (+ x 1)) :var ((x Int) (y Int) (z Int)))
must be (and are) declared.


(format LCTRS :smtlib 2.6)
(theory Ints)
(define-fun isEven ((x Int)) Bool (= (mod x 2) 0))
(sort NList)
(fun build (-> Int NList NList)) 
(fun nats NList)
(fun cons (-> Int NList NList)) 
(fun nil NList)
(rule nats (build 0 nil))
(rule (build n xs) (build (+ n 1) (cons n xs)) :guard (and (isEven n) (>= n 0)))
(rule (build n xs) (build (+ n 1) xs) :guard (and (not (isEven n)) (>= n 0)))
This example specifies an LCTRS with Bool and Int as theory sorts, NList as non-theory sort, and integers as values. The theory signature consists of the values, the theory symbols of Core and Ints, and isEven. The term signature consists of build, nats, cons and nil.

The following LCTRS is a bit-vector version of the above LCTRS:

(format LCTRS :smtlib 2.6)
(theory FixedSizeBitVectors)
(define-fun isEven ((x (_ BitVec 32))) Bool (= (bvurem x #x00000002) #x00000000))
(sort BVList)
(fun build (-> (_ BitVec 32) BVList BVList))
(fun bvs BVList)
(fun cons (-> (_ BitVec 32) BVList BVList))
(fun nil BVList)
(rule bvs (build #x00000000 nil))
(rule (build n xs) (build (bvadd n #x00000001) (cons n xs)) 
    :guard (and (isEven n) (not (bvult n #x00000000))) :var ((n (_ BitVec 32))))
(rule (build n xs) (build (bvadd n #x00000001) xs) 
    :guard (and (not (isEven n)) (not (bvult n #x00000000))) :var ((n (_ BitVec 32))))