IntroductionSTP is an efficient decision procedure for the validity (or
satisfiability) of formulas from a quantifierfree manysorted theory
of fixedwidth bitvectors and (nonextensional) onedimensional arrays.
The functions in STP's input language include concatenation,
extraction, left/right shift, signextension, unary minus, addition,
multiplication, (signed) modulo/division, bitwise Boolean operations,
ifthenelse terms, and array reads and writes. The predicates in the
language include equality and (signed) comparators between bitvector
terms. The file based input formats that STP reads are the: CVC, SMTLIB1, and SMTLIB2 formats. The SMTLIB2 format is the recommended file format, because it is parsed by all modern bitvector solvers. STP implements a subset of the SMTLIB2 language; not all SMTLIB2 features are implemented. Input Formats accepted by STPSTP uses the file extension to select the appropriate parser, but this can be overridden by command line options (use h to see the command line options). Files with a cvc extension automatically cause STP to use the CVC parser, the smt extension triggers the SMTLIB1 parser, and the smt2 extension triggers the SMTLIB2 parser. SMTLIB2 languageSTP supports the SMTLIB1 and SMTLIB2 formats. See the SMTLIB website
for a formal description of the languages. We give some of the SMTLIB2 bitvector operations below. The bitvector operations and all of their semantics are given at the SMTLIB2 website here HeaderThe SMTLIB2 format uses a header to tell the solver which type of problem is coming, the header needed is: (setlogic QF_ABV) QF_BV is for bitvector problems, QF_ABV is for bitvector and array problems. Declarations

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) 
 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.
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:
(checksat)
(exit)
Examples
There are many SMTLIB2 format examples in STP's source code repository. Look for files with a .smt2 extension
here .
(setlogic QF_BV)
(setinfo :smtlibversion 2.0)
(setinfo :status sat)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(checksat)
(exit)
The CVC language
In this section we describe the input language that STP expects by default.
Declarations
x : BITVECTOR(32);
An example of an array declaration is as follows:
x_arr : ARRAY BITVECTOR(32) OF BITVECTOR(5000);
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:
0bin0000111101010000, and the corresponding hex representation is 0hex0f50.
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.
The word level functions are:
Name 
Symbol 
Example 
Concatenation 
@ 
t1@t2@...@tm 
Extraction 
[i:j] 
x[31:26] 
left shift 
<< 
0bin0011 << 3 =
0bin0011000 
right shift 
>> 
x[24:17] >> 5, another example: 0bin1000 >> 3 = 0bin0001 
sign extension 
BVSX(bv,n) 
BVSX(0bin100, 5) = 0bin11100 
Array READ 
[index] 
x_arr[t1] 
Array WRITE 
WITH 
x_arr WITH [index] := value 
 For extraction terms, say t[i:j], 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+k.
 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.
Name 
Symbol 
Example 
Bitwise AND 
& 
t1 & t2 & ...
& tm 
Bitwise OR   
t1  t2  t3  ...  tm 
Bitwise NOT 
~ 
~t1 
Bitwise XOR 
BVXOR 
BVXOR(t1,t2) 
Bitwise NAND 
BVNAND 
BVNAND(t1,t2) 
Bitwise NOR 
BVNOR 
BVNOR(t1,t2) 
Bitwise XNOR 
BVXNOR 
BVXNOR(t1,t2) 
 It is required that all the arguments of bitwise functions have the same length
Name 
Symbol 
Example 
Bitvector Add 
BVPLUS 
BVPLUS(n,t1,t2,...,tm) 
Bitvector Mult 
BVMULT 
BVMULT(n,t1,t2) 
Bitvector subtract 
BVSUB 
BVSUB(n,t1,t2) 
Bitvector Unary Minus 
BVUMINUS 
BVUMINUS(t1) 
Bitvector Div 
BVDIV 
BVDIV(n,t1,t2), where t1
is the
dividend and t2 is the divisor 
Signed Bitvector Div 
SBVDIV 
SBVDIV(n,t1,t2), where t1 is the dividend and t2 is the divisor 
Bitvector Modulo 
BVMOD 
BVMOD(n,t1,t2), where t1 is the dividend and t2 is the divisor 
Signed Bitvector Modulo 
SBVMOD 
SBVMOD(n,t1,t2), where t1 is the dividend and t2 is the divisor 
 the number of output bits has to specified (except unary minus).
 Inputs t1,t2 ...,tm must be of the same length
 BVUMINUS(t) is a shorthand for BVPLUS(n,~t,0bin1), where n is the length of t.
 Bitvector subtraction (BVSUB(n,t1,t2)) is a shorthand for BVPLUS(n,t1,BVUMINUS(t2))
STP also supports conditional terms (IF cond THEN t1 ELSE t2 ENDIF), where cond is boolean term, t1 and t2 can be bitvector terms. This allows us to simulate multiplexors. An example is:
x,y : BITVECTOR(1);
QUERY(x = IF 0bin0=x THEN y ELSE BVUMINUS(y));
Predicates
Name 
Symbol 
Example 
Equality 
= 
t1=t2 
Less Than 
BVLT 
BVLT(t1,t2) 
Greater Than 
BVGT 
BVGT(t1,t2) 
Less Than Or Equal To 
BVLE 
BVLE(t1,t2) 
Greater Than Or Equal To 
BVGE 
BVGE(t1,t2) 
Signed Less Than 
SBVLT 
SBVLT(t1,t2) 
Signed Greater Than 
SBVGT 
SBVGT(t1,t2) 
Signed Less Than Or Equal
To 
SBVLE 
SBVLE(t1,t2) 
Signed Greater Than Or
Equal To 
SBVGE 
SBVGE(t1,t2) 
 STP requires that in atomic formulas such as x=y, x and y are expressions of the same length. STP accepts Boolean combination of atomic formulas.
Some Examples
Example 1 illustrates the use of arithmetic, wordlevel and bitwise NOT operations:
x : BITVECTOR(5);
y : BITVECTOR(4);
yy : BITVECTOR(3);
QUERY(
BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, 0bin000@~(y[3:2]))
);
Example 2 illustrates the use of arithmetic, wordlevel and multiplexor terms:
bv : BITVECTOR(10);
a : BOOLEAN;
QUERY(
0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2]
AND
0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF)=(IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0]
);
Example 3 illustrates the use of bitwise operations:
x, y, z, t, q : BITVECTOR(1024);
ASSERT(x=~x);
ASSERT(x&y&t&z&q = x);
ASSERT(xy = t);
ASSERT(BVXOR(x,~x)=t);
QUERY(FALSE);
Example 4 illustrates the use of predicates and all the arithmetic operations:
x, y : BITVECTOR(8);
ASSERT(x=0hex05);
ASSERT(y = 0bin00000101);
QUERY(
BVMULT(8,x,y)=BVMULT(8,y,x)
AND
NOT(BVLT(x,y))
AND
BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x)))
AND
x = BVSUB(8, BVUMINUS(x), BVPLUS(8, x,0hex01))
);
Example 5 illustrates the use of shift functions
x, y : BITVECTOR(8);
z, t : BITVECTOR(12);
ASSERT(x=0hexff);
ASSERT(z=0hexff0);
QUERY(z = x << 4);
For invalid inputs, the COUNTEREXAMPLE command can be used to generate appropriate counterexamples. The generated counter example is essentially a bitwise assignment to the variables in the input.