I'm currently working on a static analysis work in which I need to check whether a given formula is met or not. I hope the following example clarifies my requirement.
Suppose we have a list of three-addressed expressions whose operators are simple arithmetic and bit-wise operators (such as
xor). Each expression could have constant literals or variable symbols. For example, consider the following list:
a = b + 1 c = d c = c xor d a = a + c a = a + 4
What I need is that to see whether a given formula is established or not. For example, the following formulas:
a == b + <some_constants> # In this example: Yes, because a == b + 5 a == d + <some_constants> # In this example: No
So can a SMT solver (Z3 for example) help me in this situation? If not, could you please point me out if there is a suitable tool applicable for this requirement?