The SMT Language
This page contains a short description for the SMTLibv2 input language that STP can parse. For a longer description please read this PDF.
Header
The SMTLIB2 format uses a header to tell the solver which type of problem is coming, the header needed is:
1 2 

QF_BV is for bitvector problems, QF_ABV is for bitvector and array problems.
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:
1


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


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 n1 for an nbit constant. This convention naturally extends to all bitvector expressions. Following are some examples of bitvector constants:
1


The Bitvector implementation in STP supports a very large number of functions and predicates. The functions are categorized into wordlevel functions, bitwise functions, and arithmetic functions. Let t1,t2,…,tm denote some arbitrary bitvector terms.
Word level functions
Name  Symbol  Example 

Concatenation  concat  (concat (_ bv0 16) x) 
Extraction  extract  ((_ extract 7 0) o277135888) 
left shift  bvlshl  (bvlshl x y) 
right 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[n1: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.
Footer
After defining the problem, tell STP what to do. Usually this is to check the satisfiability, then to exit:
1 2 

Examples
There are many SMTLIB2 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:
1 2 3 4 5 6 
