Search code examples
z3smtmodel-checkingstate-space

How can i check “whether two state space are equivalent" in SMT Solver like z3

I'm a SMT Beginner. I am confused how to check “whether two state space are equivalent" and encoding this problem in SMT.

For example, I have a register called "reg". Then, I write "dataIn1" and "dataIn2" to the "reg" in sequence. as follows .

reg = BitVec('reg',1)
dataIn1 = BitVec('dataIn1',1)
dataIn2 = BitVec('dataIn2',1)

state_space_1 = reg==dataIn1
state_space_2 = reg==dataIn2

Obviously, both state_space_1 and state_space_2 represent that "reg" can be either 0 or 1. So, state_space_1 and state_space_2 are equivalent.

However, how can I check “whether state_space_1 and state_space_2 are equivalent" and encoding this problem in SMT solver like z3.

Solution

  • Your conclusion that Obviously... state_space_1 and state_space_2 are equivalent isn't true. Note that you have three separate variables here: reg, dataIn1 and dataIn2. And state_space_1 represents the part of the space where reg equals dataIn1, and state_space_2 represents the part of the space where reg equals dataIn2. There's no reason to expect these two spaces to be the same.

    Here's some more detail. In a typical SAT/SMT query, you ask the question "is there a satisfying model for the constraints I've asserted?" So, to check equivalence, one asks if two expressions can differ. That is, ask if X != Y can be satisfied. If the solver can find a model for this, then you know they are not equal, and the model represents how they differ. If the solver says unsat, then you know that X = Y must hold, i.e., they represent the exact same state-space.

    Based on this your example would be coded as:

    from z3 import *

reg     = BitVec('reg', 1)
dataIn1 = BitVec('dataIn1', 1)
dataIn2 = BitVec('dataIn2', 1)

state_space_1 = reg == dataIn1
state_space_2 = reg == dataIn2

s = Solver()
s.add(Not(state_space_1 == state_space_2))
print(s.check())
print(s.model())

    This prints:

    sat
[dataIn2 = 1, dataIn1 = 0, reg = 0]

    So, we conclude that state_space_1 and state_space_2 do not represent the same state-space. They differ when dataIn1 is 0, dataIn2 is 1, and reg is 0.

    If you are new to SMT solving, you might want to skim through Yurichev's SAT/SMT by example document (https://sat-smt.codes/SAT_SMT_by_example.pdf), which should give you a good overview of the techniques involved from an end-user perspective.

    To find out more regarding z3 programming, https://theory.stanford.edu/~nikolaj/programmingz3.html is an excellent resource.