SMT-LIB2 Input Language Reference

This page contains a short description for the SMT-LIB version 2 input language that STP can parse. For more information related to SMT-LIB, please refer to this page.

Declarations

Bitvector expressions (or terms) are constructed out of bitvector constants, bitvector variables and the functions listed below. In STP all variables have to declared before the point of use. An example declaration of a bitvector variable of length, say 32, is as follows:

(declare-fun x () (_ BitVec 32))

An example of an array declaration with 32 bit indices, and 7 bit results is:

(declare-fun a () (Array (_ BitVec 32) (_ BitVec 7)))

Functions and Terms

Bitvector variables (or terms) of length 0 are not allowed. Bitvector constants can be represented in binary or hexadecimal format. The rightmost bit is called the least significant bit (LSB), and the leftmost bit is the most significant bit (MSB). The index of the LSB is 0, and the index of the MSB is n-1 for an n-bit constant. This convention naturally extends to all bitvector expressions.

Following are some examples of bitvector constants in binary and hexadecimal:

#b0000111101010000
#x0f50

The bitvector implementation in STP supports a very large number of functions and predicates. The functions are categorized into word-level functions, bitwise functions, and arithmetic functions.

Word-level functions

Name Symbol Example
Concatenation concat (concat (_ bv0 16) x)
Extraction extract ((_ extract 7 0) o277135888)
Left Shift bvlshl (bvlshl x y)
Light Shift bvlshr (bvlshr x y)
Sign Extension sign_extend ((_ sign_extend 24) x)
Array READ select (select e829 v817)
Array WRITE store (store a x y)

Notes:

  • For extraction terms, say ((_extract i j) t), n > i >= j >= 0, where n is the length of t.
  • For left shift terms, t << k is equal to k 0’s appended to t. The length of t << k is n.
  • For right shift terms, say t >> k, the term is equal to the bitvector obtained by k 0’s followed by t[n-1:k]. The length of t >> k is n.

Bitwise functions

Name Symbol Example
Bitwise AND bvand (bvand o1 o6)
Bitwise OR bvor (bvor var29 var30)
Bitwise NOT bvnot (bvnot (_ bv0 2000))
Bitwise XOR bvxor (bvxor e7015 e7019)

The arguments of bitwise functions have the same length.

Examples

There are many SMT-LIB2 format examples in STP’s source code repository. Look for files with a .smt2 extension here. Signed division of -1/-2 = 0, should be satisfiable:

(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(set-info :status sat)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(check-sat)
(exit)