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.
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.