Format

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.

Values

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:

Core

true,   false,   not,   =>,   and,   or,   xor,   =,   distinct,   ite

Ints

-,   +,   *,   div,   mod,   abs,   <=,   <,   >=,   >,   (_ divisible n) for n > 0,   and the values of value_Int

FixedSizeBitVectors

concat,   (_ extract i j) with i ≥ j ≥ 0,   bvnot,   bvneg,   bvand,   bvor,   bvadd,   bvmul,   bvudiv,   bvurem,   bvshl,   bvlshr,   bvult,   and the values of value_BitVec

Reals

-,   +,   *,   /,   <=,   <,   >=,   >,   and the values of value_RealInt

Reals_Ints

-,   +,   *,   div,   mod,   abs,   <=,   <,   >=,   >,   (_ divisible n) with n > 0,   /, to_real,   to_int,   is_int,   and the values of value_Real and value_Int

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

• =, distinct and ite are polymorphic,
• -, +, *, <=, <, >= and > are ad-hoc polymorphic in the theory Reals_Ints,
• concat, (_ extract i j) with i ≥ j ≥ 0, bvnot, bvneg, bvand, bvor, bvadd, bvmul, bvudiv, bvurem, bvshl, bvlshr and bvult are ad-hoc polynormphic in theory FixedSizeBitVectors.

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

• = for Bool and = for Int are considered to be different,
• unary minus - and binary minus - are different symbols,
• bvadd of type (-> (_ BitVec 8) (_ BitVec 8) (_ BitVec 8)) and bvadd of type (-> (_ BitVec 32) (_ BitVec 32) (_ BitVec 32)) are different.

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.,

• variables used in an smt-def declaration, including bound variables, and
• variables in :guard term.

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

distinct

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.

Examples

(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))))