AUFLIA

(logic AUFLIA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-04-30"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "

 :theories (Ints ArraysEx)

 :language 
 "Closed formulas built over arbitrary expansions of the Ints and ArraysEx
  signatures with free sort and function symbols, but with the following 
  restrictions:
  - all terms of sort Int are linear, that is, have no occurrences of the
    function symbols *, /, div, mod, and abs, except as specified in the 
    :extensions attributes;
  - all array terms have sort (Array Int Int).
 "

 :extensions
 "As in the logic QF_AUFLIA."

:notes
 "This logic properly extends the logic QF_AUFLIA by allowing quantifiers."
)


(
raw file)

AUFLIRA

(logic AUFLIRA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli and Clark Barrett"
 :date "2010-05-05"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
  2011-06-03 Replaced "(* c x), or (* x c)" with "c, (* c x), or (* x c)" 
             in :extensions.
             (The missing case was had been left out unintentionally.)
 "

 :theories (Reals_Ints ArraysEx)

:language
 "Closed formulas built over arbitrary expansions of the Reals_Ints and
  ArraysEx signatures with free sort and function symbols, but with the
  following restrictions:
  - all terms of sort Int are linear, that is, have no occurrences of the
    function symbols *, /, div, mod, and abs, except as specified in the 
    :extensions attributes;
  - all terms of sort Real are linear, that is, have no occurrences of the
    function symbols * and /, except as specified in the 
    :extensions attribute;
  - all array terms have sort 
    (Array Int Real) or 
    (Array Int (Array Int Real)).
 "

:extensions
 "For every operator op with declaration (op Real Real s) for some sort s,
  and every term t1, t2 of sort Int and t of sort Real, the expression 
  - (op t1 t) is syntactic sugar for (op (to_real t1) t)
  - (op t t1) is syntactic sugar for (op t (to_real t1))
  - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2))
 "

 :extensions
 "Real or Int terms with _concrete_ coefficients are also allowed, that is,
  terms of the form c, (* c x), or (* x c) where
  x is a free constant of sort Int or Real and 
  c is an integer or rational coefficient, respectively. 
  - An integer coefficient is a term of the form m or (- m) for some
    numeral m.
  - A rational coefficient is a term of the form d, (- d) or (/ c n) 
    for some decimal d, integer coefficient c and numeral n other than 0.
 "
)
(
raw file)

AUFNIRA

(logic AUFNIRA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli and Clark Barrett"
 :date "2010-05-12"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
  2012-09-26 Clarified in :notes in what way AUFNIRA extendes AUFLIRA.
 "

 :theories (Reals_Ints ArraysEx)

 :language
 "Closed formulas built over arbitrary expansions of the Reals_Ints and
  ArraysEx signatures with free sort and function symbols.
 "

 :extensions
 "For every operator op with declaration (op Real Real s) for some sort s,
  and every term t1, t2 of sort Int and t of sort Real, the expression 
  - (op t1 t) is syntactic sugar for (op (to_real t1) t)
  - (op t t1) is syntactic sugar for (op t (to_real t1))
  - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2))
 "

 :notes
 "This logic properly extends the logic AUFLIRA by allowing 
  - non-linear (integer/real) operators such as  *, /, div, mod, and abs, and
  - allowing terms with an arbitrary array sort (as opposed to just
    (Array Int Real) and (Array Int (Array Int Real)) ).
 "
)
(
raw file)

LIA

(logic LIA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2016-02-07"
 
 :theories (Ints)

 :language 
 "Closed formulas built over an arbitrary expansion of the
  Ints signature with free constant symbols, but whose terms of sort Int 
  are all linear, that is, have no occurrences of the function symbols
  *, /, div, mod, and abs, except as specified the :extensions attribute.
 "

 :extensions
 "Terms with _concrete_ coefficients are also allowed, that is, terms
  of the form c, (* c x), or (* x c)  where x is a free constant and 
  c is a term of the form n or (- n) for some numeral n.
 "
)


(
raw file)

LRA

(logic LRA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-05-11"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
  2011-06-03 Replaced ''(* c x), or (* x c)'' with ''c, (* c x), or (* x c)'' 
  in :extensions.
  (The missing case was had been left out unintentionally.)
 "

 :theories (Reals)

 :language 
 "Closed formulas built over arbitrary expansions of the Reals signature
  with free constant symbols, but containing only linear atoms, that is, 
  atoms with no occurrences of the function symbols * and /, except as 
  specified the :extensions attribute.
 "

 :extensions
 "Terms with _concrete_ coefficients are also allowed, that is, terms
  of the form c, (* c x), or (* x c)  where x is a free constant and 
  c is an integer or rational coefficient. 
  - An integer coefficient is a term of the form m or (- m) for some
    numeral m.
  - A rational coefficient is a term of the form d, (- d) or (/ c n) 
    for some decimal d, integer coefficient c and numeral n other than 0.
 "

:notes
 "This logic properly extends the logic QF_LRA by allowing quantifiers."
)

(
raw file)

QF_ABV

(logic QF_ABV

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli and Clark Barrett"
 :date "2010-07-05"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
  2013-06-24 Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors.
 "

 :theories (FixedSizeBitVectors ArraysEx)

 :language 
 "Closed quantifier-free formulas built over the FixedSizeBitVectors and
  ArraysEx signatures, with the restriction that all array terms have sort of
  the form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.
 "

 :extensions "As in the logic QF_BV."
)


(
raw file)

QF_AUFBV

(logic QF_AUFBV

:smt-lib-version 2.5
:written-by "Cesare Tinelli and Clark Barrett"
:date "2010-05-11"
:last-updated "2015-04-25"
:update-history 
 "2015-04-25 Updated to Version 2.5.
  2013-06-24 Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors.
"

:theories (FixedSizeBitVectors ArraysEx)

:language 
 "Closed quantifier-free formulas built over an arbitrary expansion of the
  FixedSizeBitVectors and ArraysEx signatures with free sort and function
  symbols, but with the restriction that all array terms have sort of the 
  form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.
 "

:extensions "As in the logic QF_BV."
)


(
raw file)

QF_AUFLIA

(logic QF_AUFLIA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-04-30"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
  2011-06-03 Allowed x to be more than a free constants in terms of the form 
             (* c x) or (*x c)   in :extensions.
 "

 :theories (Ints ArraysEx)

 :language 
 "Closed quantifier-free formulas built over arbitrary expansions of the
  Ints and ArraysEx signatures with free sort and function symbols, but
  with the following restrictions:
  - all terms of sort Int are linear, that is, have no occurrences of the
    function symbols *, /, div, mod, and abs, except as specified in the 
    :extensions attributes;
  - all array terms have sort (Array Int Int).
 "

 :extensions
 "Terms with _concrete_ integer coefficients are also allowed, that is, terms
  of the form c, (* c x), or (* x c)  where 
  - x is a free constant or a term with top symbol not in Ints, and 
  - c is a term of the form n or (- n) for some numeral n.
 ")

(
raw file)

QF_AX

(logic QF_AX

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-04-30"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "

 :theories (ArraysEx)
 
 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of
  the ArraysEx signature with free sort and constant symbols.
 "

 :notes
 "Formulas can contain variables as long as they are bound by a let binder."
)


(
raw file)

QF_BV

(logic QF_BV

 :smt-lib-version 2.6
 :written-by "Silvio Ranise, Cesare Tinelli, and Clark Barrett"
 :date "2010-05-02"
 :last-updated "2017-06-13"
 :update-history 
 "2017-06-13 Added that bvxor and bvxnor are left associative
  2017-05-03 Updated to Version 2.6.  Division and remainder operations are no
             longer undefiend when the second operand is 0.  See
             the FixedSizeBitVectors theory definition for details.
  2015-04-25 Updated to Version 2.5.
  2013-06-24 Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors.
  2011-06-15 Fixed bug in definition of bvsmod.  Previously, it gave an incorrect
             answer when the divisor is negative and goes into the dividend evenly.
 "

:theories (FixedSizeBitVectors)

:language
 "Closed quantifier-free formulas built over an arbitrary expansion of the
  FixedSizeBitVectors signature with free constant symbols over the sorts
  (_ BitVec m) for 0 < m.  Formulas in ite terms must satisfy the same
  restriction as well, with the exception that they need not be closed 
  (because they may be in the scope of a let binder).
 "

:notes
 "For quick reference, the following is a brief and informal summary of the
  legal symbols in this logic and their meaning (formal definitions are found
  either in the FixedSizeBitvectors theory, or in the extensions below).

  Defined in theory FixedSizeBitvectors:

    Bitvector constants:

      - #bX where X is a binary numeral of length m defines the
        bitvector constant with value X and size m.
      - #xX where X is a hexadecimal numeral of length m defines the
        bitvector constant with value X and size 4*m.
 
   Functions:
 
    (concat (_ BitVec i) (_ BitVec j) (_ BitVec m))
      - concatenation of bitvectors of size i and j to get a new bitvector of
        size m, where m = i + j
    ((_ extract i j) (_ BitVec m) (_ BitVec n))
      - extraction of bits i down to j from a bitvector of size m to yield a
        new bitvector of size n, where n = i - j + 1
    (bvnot (_ BitVec m) (_ BitVec m))
      - bitwise negation
    (bvand (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - bitwise and
    (bvor (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - bitwise or
    (bvneg (_ BitVec m) (_ BitVec m))
      - 2's complement unary minus
    (bvadd (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - addition modulo 2^m
    (bvmul (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - multiplication modulo 2^m
    (bvudiv (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - unsigned division, truncating towards 0
    (bvurem (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - unsigned remainder from truncating division
    (bvshl (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - shift left (equivalent to multiplication by 2^x where x is the value of
        the second argument)
    (bvlshr (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - logical shift right (equivalent to unsigned division by 2^x where x is
        the value of the second argument)
    (bvult (_ BitVec m) (_ BitVec m) Bool)
      - binary predicate for unsigned less-than

  Defined below:

    Functions:

    (bvnand (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - bitwise nand (negation of and)
    (bvnor (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - bitwise nor (negation of or)
    (bvxor (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - bitwise exclusive or
    (bvxnor (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - bitwise equivalence (equivalently, negation of bitwise exclusive or)
    (bvcomp (_ BitVec m) (_ BitVec m) (_ BitVec 1))
      - bit comparator: equals #b1 iff all bits are equal
    (bvsub (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - 2's complement subtraction modulo 2^m
    (bvsdiv (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - 2's complement signed division
    (bvsrem (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - 2's complement signed remainder (sign follows dividend)
    (bvsmod (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - 2's complement signed remainder (sign follows divisor)
    (bvashr (_ BitVec m) (_ BitVec m) (_ BitVec m))
      - Arithmetic shift right, like logical shift right except that the most
        significant bits of the result always copy the most significant
        bit of the first argument.

    The following symbols are parameterized by the numeral i, where i >= 1.

    ((_ repeat i) (_ BitVec m) (_ BitVec i*m))
      - ((_ repeat i) x) means concatenate i copies of x

    The following symbols are parameterized by the numeral i, where i >= 0.

    ((_ zero_extend i) (_ BitVec m) (_ BitVec m+i))
      - ((_ zero_extend i) x) means extend x with zeroes to the (unsigned)
        equivalent bitvector of size m+i
    ((_ sign_extend i) (_ BitVec m) (_ BitVec m+i))
      - ((_ sign_extend i) x) means extend x to the (signed) equivalent bitvector
        of size m+i
    ((_ rotate_left i) (_ BitVec m) (_ BitVec m))
      - ((_ rotate_left i) x) means rotate bits of x to the left i times
    ((_ rotate_right i) (_ BitVec m) (_ BitVec m))
      - ((_ rotate_right i) x) means rotate bits of x to the right i times

    (bvule (_ BitVec m) (_ BitVec m) Bool)
      - binary predicate for unsigned less than or equal
    (bvugt (_ BitVec m) (_ BitVec m) Bool)
      - binary predicate for unsigned greater than
    (bvuge (_ BitVec m) (_ BitVec m) Bool)
      - binary predicate for unsigned greater than or equal
    (bvslt (_ BitVec m) (_ BitVec m) Bool)
      - binary predicate for signed less than
    (bvsle (_ BitVec m) (_ BitVec m) Bool)
      - binary predicate for signed less than or equal
    (bvsgt (_ BitVec m) (_ BitVec m) Bool)
      - binary predicate for signed greater than
    (bvsge (_ BitVec m) (_ BitVec m) Bool)
      - binary predicate for signed greater than or equal
 "

:extensions
 "Below, let |exp| denote the integer resulting from the evaluation
  of the arithmetic expression exp.

  - Bitvector Constants:
    (_ bvX n) where X and n are numerals, i.e. (_ bv13 32),
    abbreviates the term #bY of sort (_ BitVec n) such that

    [[#bY]] = nat2bv[n](X) for X=0, ..., 2^n - 1.

    See the specification of the theory's semantics for a definition
    of the functions [[_]] and nat2bv.  Note that this convention implicitly
    considers the numeral X as a number written in base 10.

  - Bitwise operators

    For all terms s,t of sort (_ BitVec m), where 0 < m,

    (bvnand s t) abbreviates (bvnot (bvand s t))
    (bvnor s t) abbreviates (bvnot (bvor s t))
    (bvxor s t) abbreviates (bvor (bvand s (bvnot t)) (bvand (bvnot s) t))
    (bvxnor s t) abbreviates (bvor (bvand s t) (bvand (bvnot s) (bvnot t)))
    (bvcomp s t) abbreviates (bvxnor s t) if m = 1, and
       (bvand (bvxnor ((_ extract |m-1| |m-1|) s) ((_ extract |m-1| |m-1|) t))
              (bvcomp ((_ extract |m-2| 0) s) ((_ extract |m-2| 0) t))) otherwise.

    Additionally, bvxor and bvxnor are left associative, so:

    (bvxor s_1 s_2 ... s_n) abbreviates (bvxor (bvxor s_1 s_2 ...) s_n), and
    (bvxnor s_1 s_2 ... s_n) abbreviates (bvxnor (bvxnor s_1 s_2 ...) s_n).

  - Arithmetic operators

    For all terms s,t of sort (_ BitVec m), where 0 < m,

    (bvsub s t) abbreviates (bvadd s (bvneg t))
    (bvsdiv s t) abbreviates
      (let ((?msb_s ((_ extract |m-1| |m-1|) s))
            (?msb_t ((_ extract |m-1| |m-1|) t)))
        (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
             (bvudiv s t)
        (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
             (bvneg (bvudiv (bvneg s) t))
        (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
             (bvneg (bvudiv s (bvneg t)))
             (bvudiv (bvneg s) (bvneg t))))))
    (bvsrem s t) abbreviates
      (let ((?msb_s ((_ extract |m-1| |m-1|) s))
            (?msb_t ((_ extract |m-1| |m-1|) t)))
        (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
             (bvurem s t)
        (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
             (bvneg (bvurem (bvneg s) t))
        (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
             (bvurem s (bvneg t)))
             (bvneg (bvurem (bvneg s) (bvneg t))))))
    (bvsmod s t) abbreviates
      (let ((?msb_s ((_ extract |m-1| |m-1|) s))
            (?msb_t ((_ extract |m-1| |m-1|) t)))
        (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
              (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
          (let ((u (bvurem abs_s abs_t)))
            (ite (= u (_ bv0 m))
                 u
            (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
                 u
            (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
                 (bvadd (bvneg u) t)
            (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
                 (bvadd u t)
                 (bvneg u))))))))
    (bvule s t) abbreviates (or (bvult s t) (= s t))
    (bvugt s t) abbreviates (bvult t s)
    (bvuge s t) abbreviates (or (bvult t s) (= s t))
    (bvslt s t) abbreviates:
      (or (and (= ((_ extract |m-1| |m-1|) s) #b1)
               (= ((_ extract |m-1| |m-1|) t) #b0))
          (and (= ((_ extract |m-1| |m-1|) s) ((_ extract |m-1| |m-1|) t))
               (bvult s t)))
    (bvsle s t) abbreviates:
      (or (and (= ((_ extract |m-1| |m-1|) s) #b1)
               (= ((_ extract |m-1| |m-1|) t) #b0))
          (and (= ((_ extract |m-1| |m-1|) s) ((_ extract |m-1| |m-1|) t))
               (bvule s t)))
    (bvsgt s t) abbreviates (bvslt t s)
    (bvsge s t) abbreviates (bvsle t s)

  - Other operations

    For all numerals i > 0, j > 1 and 0 < m, and all terms s and t of
    sort (_ BitVec m),

    (bvashr s t) abbreviates 
      (ite (= ((_ extract |m-1| |m-1|) s) #b0)
           (bvlshr s t)
           (bvnot (bvlshr (bvnot s) t)))

    ((_ repeat 1) t) stands for t
    ((_ repeat j) t) abbreviates (concat t ((_ repeat |j-1|) t))

    ((_ zero_extend 0) t) stands for t
    ((_ zero_extend i) t) abbreviates (concat ((_ repeat i) #b0) t)

    ((_ sign_extend 0) t) stands for t
    ((_ sign_extend i) t) abbreviates
      (concat ((_ repeat i) ((_ extract |m-1| |m-1|) t)) t)

    ((_ rotate_left 0) t) stands for t
    ((_ rotate_left i) t) abbreviates t if m = 1, and
      ((_ rotate_left |i-1|)
        (concat ((_ extract |m-2| 0) t) ((_ extract |m-1| |m-1|) t))
      otherwise

    ((_ rotate_right 0) t) stands for t
    ((_ rotate_right i) t) abbreviates t if m = 1, and
      ((_ rotate_right |i-1|)
        (concat ((_ extract 0 0) t) ((_ extract |m-1| 1) t)))
      otherwise
 "
)

(
raw file)

QF_IDL

(logic QF_IDL

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-04-30"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "

 :theories ( Ints )

 :language
 "Closed quantifier-free formulas with atoms of the form:
  - q
  - (op (- x y) n),
  - (op (- x y) (- n)), or
  - (op x y)
  where
    - q is a variable or free constant symbol of sort Bool,
    - op is <, <=, >, >=, =, or distinct,
    - x, y are free constant symbols of sort Int, 
    - n is a numeral. 
 "
)


(
raw file)

QF_LIA

(logic QF_LIA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-04-30"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "

 :theories (Ints)

 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of the
  Ints signature with free constant symbols, but whose terms of sort Int 
  are all linear, that is, have no occurrences of the function symbols
  *, /, div, mod, and abs, except as specified the :extensions attribute.
 "

 :extensions
 "Terms with _concrete_ coefficients are also allowed, that is, terms
  of the form c, (* c x), or (* x c)  where x is a free constant and 
  c is a term of the form n or (- n) for some numeral n.
 "
)


(
raw file)

QF_NIA

(logic QF_NIA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-05-12"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "

 :theories ( Ints )

 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of the
  Ints signature with free constant symbols.
 "
)
(
raw file)

QF_NRA

(logic QF_NRA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2011-06-11"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "
 
 :theories ( Reals )

 :language 
 "Closed quantifier-free formulas built over arbitrary expansions of 
  the Reals signature with free constant symbols."
)


(
raw file)

QF_RDL

(logic QF_RDL

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-04-30"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
  2010-12-16 Replaced erroneous ''n > 0'' with ''n > 1'' in language attribute.
 "

 :theories (Reals)

 :language 
 "Closed quantifier-free formulas with atoms of the form:
  - p
  - (op (- x y) c),
  - (op x y),
  - (op (- (+ x ... x) (+ y ... y)) c) with n > 1 occurrences of x and of y,
  where
    - p is a variable or free constant symbol of sort Bool,
    - c is an expression of the form m or (- m) for some numeral m,
    - op is <, <=, >, >=, =, or distinct,
    - x, y are free constant symbols of sort Real. 
  "

 :extensions
 "The expression (op (- x y) (/ c n)) where n is a numeral other than 0 and
  c is an expression of the form m or (- m) for some numeral m, 
  abbreviates the expression
  (op (- (+ x ... x) (+ y ... y)) c) with n occurrences of x and y.
 "
)


(
raw file)

QF_UF

(logic QF_UF

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-04-14"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "
 
 :theories ()  ; includes just Core theory

 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of
  the Core signature with free sort and function symbols.
 "
 :values
 "For each sort other than Bool the set of values is abstract.
  For Bool it is defined as in the Core theory declaration.
 "
 :notes
 "Formulas can contain variables as long as they are bound by a let binder.
 "
 :notes
 "All the free symbols used in scripts for this logic must be declared in
  the scripts themselves.
 "
)


(
raw file)

QF_UFBV

(logic QF_UFBV

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2011-06-11"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
  2013-06-24 Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors.
 "

:theories ( FixedSizeBitVectors )

:language
 "Closed quantifier-free formulas built over arbitrary expansions of
  the FixedSizeBitVectors signature with free sort and function
  symbols.
 "

:extensions "As in the logic QF_BV."
)
(
raw file)

QF_UFIDL

(logic QF_UFIDL

 :smt-lib-version 2.5
 :written-by "Clark Barrett, Cesare Tinelli"
 :date "2010-05-12"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
  2011-06-03 Added :note field."

 :theories (Ints)

 :language
 "Closed quantifier-free formulas built over an arbitrary expansion with 
  free sort and function symbols of the signature consisting of 
  - all the sort and function symbols of Core and
  - the following symbols of Int:

    :sorts ((Int 0))
    :funs ((NUMERAL Int) 
           (- Int Int Int)
           (+ Int Int Int) 
           (<= Int Int Bool)
           (< Int Int Bool)
           (>= Int Int Bool)
           (> Int Int Bool)
          )

  Additionally, for every term of the form (op t1 t2) with op in {+, -}, 
  at least one of t1 and t2 is a numeral. 
 "

 :note 
 "For historical reasons, the syntax of this logic is *not* an extension 
  of QF_IDL's syntax. However, any formula in this logic with no free sorts 
  and no free function symbol of arity > 0 can be converted into an 
  equisatisfiable formula in QF_IDL.
 "
)


(
raw file)

QF_UFLIA

(logic QF_UFLIA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2011-06-11"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "

 :theories ( Ints )

 :language 
 "Closed quantifier-free formulas built over arbitrary expansions of the
  Ints signatures with free sort and function symbols, but with the 
  following restrictions:
  - all terms of sort Int are linear, that is, have no occurrences of the
    function symbols *, /, div, mod, and abs, except as specified in the 
    :extensions attributes;
 "

 :extensions
 "As in the logic QF_LIA."
)

(
raw file)

QF_UFLRA

(logic QF_UFLRA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2011-06-11"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "
 
 :theories ( Reals )

 :language 
 "Closed quantifier-free formulas built over arbitrary expansions of the 
  Reals signature with free sort and function symbols, but containing 
  only linear atoms, that is, atoms with no occurrences of the function
  symbols * and /, except as specified the :extensions attribute.
 "

 :extensions
 "Terms with _concrete_ coefficients are also allowed, that is, terms
  of the form c, (* c x), or (* x c)  where x is a free constant and 
  c is an integer or rational coefficient. 
  - An integer coefficient is a term of the form m or (- m) for some
    numeral m.
  - A rational coefficient is a term of the form d, (- d) or (/ c n) 
    for some decimal d, integer coefficient c and numeral n other than 0.
 "
)


(
raw file)

QF_LRA

(logic QF_LRA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2010-04-14"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5. 
  2011-06-03 Replaced ''(* c x), or (* x c)'' with ''c, (* c x), or (* x c)'' 
             in :extensions. (The missing case had been left out unintentionally.)
 "

 :theories (Reals)

 :language 
 "Closed quantifier-free formulas built over arbitrary expansions of 
  the Reals signature with free constant symbols, but containing only
  linear atoms, that is, atoms with no occurrences of the function
  symbols * and /, except as specified the :extensions attribute.
 "

 :extensions
 "Terms with _concrete_ coefficients are also allowed, that is, terms
  of the form c, (* c x), or (* x c)  where x is a free constant and 
  c is an integer or rational coefficient. 
  - An integer coefficient is a term of the form m or (- m) for some
    numeral m.
  - A rational coefficient is a term of the form d, (- d) or (/ c n) 
    for some decimal d, integer coefficient c and numeral n other than 0.
 "
)


(
raw file)

QF_UFNRA

(logic QF_UFNRA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2011-06-11"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "
 
 :theories ( Reals )

 :language 
 "Closed quantifier-free formulas built over arbitrary expansions of 
  the Reals signature with free sort and function symbols.
 "
)


(
raw file)

UFLRA

(logic UFLRA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2011-06-11"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "
 
 :theories ( Reals )

 :language 
 "Closed formulas built over arbitrary expansions of the Reals signature 
  with free sort and function symbols, but containing only linear atoms, 
  that is, atoms with no occurrences of the function symbols * and /,
  except as specified the :extensions attribute.
 "

 :extensions
 "Terms with _concrete_ coefficients are also allowed, that is, terms
  of the form c, (* c x), or (* x c)  where x is a free constant and 
  c is an integer or rational coefficient. 
  - An integer coefficient is a term of the form m or (- m) for some
    numeral m.
  - A rational coefficient is a term of the form d, (- d) or (/ c n) 
    for some decimal d, integer coefficient c and numeral n other than 0.
 "
)


(
raw file)

UFNIA

(logic UFNIA

 :smt-lib-version 2.5
 :written-by "Cesare Tinelli"
 :date "2011-06-11"
 :last-updated "2015-04-25"
 :update-history 
 "2015-04-25 Updated to Version 2.5.
 "

 :theories ( Ints )

 :language 
 "Closed formulas built over an arbitrary expansion of the Ints signature
  with free sort and function symbols."
)
(
raw file)