Commit 9697fd3b authored by Martin Jonas's avatar Martin Jonas
Browse files

Polishing

parent bcd1e724
......@@ -65,13 +65,15 @@ be replaced by a simpler term regardless the parity of the value
$k$. In particular, if $i$ is the largest number for which $2^i$
divides the constant $k$ and the unconstrained variable $x$ has
bit-width $n$, the term $k \times x$ can be rewritten to
$extract_0^{n-i}(x) \cdot 0^i$. This approach can be also extended to
the multiplication of two variables from which one is unconstrained. I
plan to investigate further extensions to the terms containing
division and remainder operations and to publish a paper concerning
propagation of unconstrained variables in quantified formulas and
extensions of unconstrained variable simplification to multiplication
and division. I will also experimentally evaluate the effect of such
$extract_0^{n-i}(x) \cdot 0^i$. Intuitively, the term $k \times x$ can
have every possible bit-vector value that has the last significant $i$
bits zero. This approach can be also extended to the multiplication of
two variables from which one is unconstrained. I plan to investigate
further extensions to the terms containing division and remainder
operations and to publish a paper concerning propagation of
unconstrained variables in quantified formulas and extensions of
unconstrained variable simplification to multiplication and
division. I will also experimentally evaluate the effect of such
simplifications on our solver Q3B and on state-of the art solvers such
as Boolector, CVC4, and Z3.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment