Use of rewriting term in decision-making procedures for bit vector arithmetic

Question

I am working on a project whose purpose is to use rewriting of terms to solve / simplify arithmetic problems of a fixed size bit vector, which is useful as a preliminary step to some decision-making procedure, for example, based on the-blasting bit. The term “rewriting” can generally solve the problem or otherwise produce a much simpler equivalent problem, so a combination of both can lead to significant speedup.

I know that many SMT solvers implement this strategy (e.g. Boolector, Beaver, Alt-Ergo or Z3), but it is difficult to find documents / technical reports / etc in which these rewriting steps are described in detail. In general, I only found articles in which the authors describe such simplification steps in a few paragraphs. I would like to find some document that explains in detail the use of rewriting terms: providing example rules, discussing the convenience of rewriting AC and / or other equational axioms, using rewriting strategies, etc.

Currently, I just found a technical report Decision Procedure for Fixed Width Bit Vectors that describes the normalization / simplification steps performed by CVC Lite, and I would like to find more technical reports like this! I also found a poster about Term rewriting in STP , but this is just a short summary.

I have already visited the websites of these SMT solvers, and I have looked at their publication pages ...

I would appreciate any reference or any explanation of how term rewriting is used in current versions of well-known SMT solvers. I'm especially interested in the Z3 because it looks like one of the smartest phases of simplification. For example, Z3 3. * introduced a new decision procedure for the bit vector, but, unfortunately, I could not find a single paper describing it.

Answer 1

I agree with you. It is difficult to find documents describing the preprocessing steps used in modern SMT solvers. Most SMT solver developers agree that these preprocessing steps are very important for bit vector theory. I believe that these methods are not published for several reasons: most of them are small tricks, which in themselves are not a significant scientific contribution; most methods work only in the context of a specific system; a method that may seem to work very well on solver A does not work on solver B I believe that having open SMT solvers is the only way to solve this problem. Even if we publish the methods used in a specific solver A , it would be very difficult to reproduce the actual behavior of solver A without seeing its source code.

In any case, here is a summary of the preprocessing performed by Z3, and important details.

• A few simplification rules can reduce this size locally, but increase it globally. Simplification should avoid memory bloat caused by such simplification. Examples can be found at: http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf

• The first simplification step performs only local simplifications that preserve equivalence. Examples:

 2*x - x -> xx and x -> x 

• Next, Z3 performs continuous distribution. Given the equality t = v , where v is the value. It replaces t everywhere with v .

 t = 0 and F[t] -> t = 0 and F[0] 

• Further, it performs a Gaussian exception for bit vectors. However, only variables that occur no more than two times in arithmetic expressions are excluded. This restriction is used to prevent an increase in the number of adders and multipliers in your formula. For example, suppose that x = y+z+w and x occurs at p(x+z) , p(x+2*z) , p(x+3*z) and p(x+4*z) . Then, after eliminating x , we would have p(y+2*z+w) , p(y+3*z+w) , p(y+4*z+w) and p(y+5*z+w) . Although we excluded x , we have more adders than the original formula.

• Then it excludes unlimited variables. This approach is described in a doctoral dissertation by Robert Brammeyer and Roberto Brutomeso.

• Then another round of simplification is performed. This time, local contextual simplifications are performed. These simplifications are potentially very expensive. Thus, a threshold value is used for the maximum number of nodes that need to be visited (the default value is 10 million). Simplifying the local context contains rules such as

 (x != 0 or y = x+1) -> (x != 0 or y = 1) 

• He then tries to minimize the number of multipliers using distributivity. Example:

ab + ac → (b + c) * a

• Then he tries to minimize the number of adders and multipliers, using associativity and commutativity. Assume that the formula contains the terms a + (b + c) and a + (b + d) . Then Z3 will rewrite them in: (a+b)+c and (a+b)+d . Before the Z3 conversion, 4 adders would have to be encoded. After that, only three adders should be encoded, since Z3 uses fully shared expressions.

• If the formula contains only equality, concatenation, extraction, and similar operators. Then Z3 uses a specialized solver based on union-finding and congruence.

• Otherwise, it destroys everything, uses AIG to minimize the Boolean formula, and calls its SAT solver.

Answer 2

Z3 uses rewriting for many simplifications performed during preprocessing. Many rewrite rules used for the UFBV strategy (with quantifiers) are described in the following article:

Wintersteiger, Hamadi, de Moura: An Effective Solution to Quantitative Bit-Vector Formulas, FMCAD, 2010