Format
The format for logically constrained TRSs extends the MSTRS format, according to the following grammar:
LCTRS ::= ( format LCTRS (:smtlib standard)? ) theory+ smtdef* sortdecl* fundecl* rule* standard ::= identifier theory ::= ( theory smttheory ) sortdecl ::= ( sort identifier ) sort ::= identifier  theorysort theorysort ::= ( _ identifier+ ) smtdef ::= ( definefun identifier ( vars ) theorysort formula ) fundecl ::= ( 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
(SMTLIB 2.6) as defined in this
document.
Supported versions and theories will be added over time.
The smttheory
in the theory
declaration specifies the theory symbols and types of the LCTRS theory part
by importing an SMT theory smttheory
, defined in
the specified SMT standard. This theory should be supported in an
offtheshelf SMT solver. Sensible examples can be found on the
SMTLIB
site. In an LCTRS file, at least one theory is required.
The theorysort
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, smtdef
must adhere to the
definefun
command of SMTLIB, and
formula
must be an SMTLIB 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 definefun
must not conflict with other builtin 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
definefun
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 righthand side of a constrained rule must have the same type. Below we specify further restrictions on the grammar constructs in the above format.
SMTLIB versions declared by
:smtlib standard
The declaration is mandatory for LCTRSs in the ARI database. Currently we support SMTLIB 2.6:
standard ::= 2.6
SMTLIB theories declared by smttheory
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
smttheory ::= Core  Ints  FixedSizeBitVectors  Reals  Reals_IntsTheory
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 theorysort
For 2.6
we admit (_ BitVec n)
with
n > 0:
theorysort ::= Bool  Int  (_ BitVec posnumeral)  Real posnumeral ::= [19][09]*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 
Values
The specified theories admit the following values:
theory  sort  values  grammar 

Core 
Bool 
Boolean values  value_{Bool} ::=
true  false 
Ints 
Int 
integers  value_{Int} ::=
integer 
FixedSizeBitVectors 
(_ BitVec n) 
nbits bitvectors  value_{BitVec} ::=
#b[01]+ 
#x[09 af
AF]+ 
Reals 
Real 
reals (and integers)  value_{RealInt} ::=
value_{Real}

Reals_Ints 
Real 
reals  value_{Real} ::=
decimal


Int 
integers  value_{Int} ::=
integer

negnumeral ::= [19][09]* 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}
Ints
,
FixedSizeBitVectors
, Reals
and
Reals_Ints
contain all theory symbols of Core
.
Some theory symbols are (adhoc) polymorphic. For SMTLIB 2.6

=
,distinct
andite
are polymorphic, 

,+
,*
,<=
,<
,>=
and>
are adhoc polymorphic in the theoryReals_Ints
, 
concat
,(_ extract i j)
with i ≥ j ≥ 0,bvnot
,bvneg
,bvand
,bvor
,bvadd
,bvmul
,bvudiv
,bvurem
,bvshl
,bvlshr
andbvult
are adhoc polynormphic in theoryFixedSizeBitVectors
.

=
forBool
and=
forInt
are considered to be different, 
unary minus

and binary minus
are different symbols, 
bvadd
of type(> (_ BitVec 8) (_ BitVec 8) (_ BitVec 8))
andbvadd
of type(> (_ BitVec 32) (_ BitVec 32) (_ BitVec 32))
are different.
We consider nonsimple symbols such as
(_ divisible n)
as theory symbols, but they cannot
be used in rewrite rules. To use a nonsimple symbol it must be declared
by definefun
. For example, to use
(_ divisible 2)
in a rewrite rule, we can
use (definefun 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 userdefined 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 smtdef declaration, including bound variables, and

variables in
:guard term
.
(definefun f (vars)
theorysort formula)
, any userdefined 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 SMTLIB language.
For this reason we allow only simple symbol
as identifiers. Furthermore, theory variables and userdefined theory
symbol cannot be reserved words of the SMTLIB language specified by
:smtlib version
.
For SMTLIB 2.6 the reserved words recognized in the ARI database
are
in addition to the values and theory symbols listed above. Values and theory symbols of unsupported theories are also reserved words.as
let
forall
exists
match
!
_
Associativity, chainability, and pairwise property of theory symbols
Some theory symbols in SMTLIB are leftassociative, rightassociative
chainable, or have the pairwise property. For example, and
is
leftassociative,
=
is chainable, and distinct
has the pairwise
property, i.e., we can write
(and t_{1} t_{2}
t_{3} ...)
,
(= t_{1} t_{2}
t_{3} ...)
, and
(distinct t_{1} t_{2}
t_{3} ...)
.
These properties make the corresponding symbols variadic, which
is considered as syntactic sugar.
The arity of function symbols in the left and righthand 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 righthand sides of rewrite rules is two. However, for
convenience, we allow theory symbols with the leftassociative,
rightassociative, chainable, or pairwise properties to be variadic in
formulas and guard terms. In SMTLIB 2.6 the theory symbols
are leftassociative,and
or
xor
bvand
bvor
bvadd
bvmul

(binary)+
*
div
/
=>
is rightassociativity,
are chainable, and=
<=
<
>=
>
distinct
has the pairwise property.
Formulas for formula
The ARI database restricts formula
to
variables, (possibly userdefined) theory symbols, and quantifiers:
formula ::= identifier  theorysymbol  ((identifier  theorysymbol) 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 adhoc) 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) (definefun 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 nontheory 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 bitvector version of the above LCTRS:
(format LCTRS :smtlib 2.6) (theory FixedSizeBitVectors) (definefun 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))))