Skip to content

Commit

Permalink
Value sets of state variables are not transitioned anymore
Browse files Browse the repository at this point in the history
  • Loading branch information
@ckirsch
ckirsch committed Jan 15, 2025
1 parent f6a81d9 commit 9b3143f
Showing 1 changed file with 48 additions and 13 deletions.
61 changes: 48 additions & 13 deletions tools/bitme.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -510,6 +510,19 @@ def set_value(self, sid_line, value, constraint_line):
self.values[value] = Values.OR(constraint_line, self.values[value])
return self

def is_equal(self, values):
# naive check for semantical equivalence
if not isinstance(values, Values) or len(self.values) != len(values.values):
return False
else:
for value in self.values:
if value in values.values:
if self.values[value] != values.values[value]:
return False
else:
return False
return True

class Expression(Line):
def __init__(self, nid, sid_line, domain, comment, line_no):
super().__init__(nid, comment, line_no)
Expand All @@ -525,6 +538,10 @@ def get_domain(self):
# filter out uninitialized states
return [state for state in self.domain if state.init_line is not None]

def is_equal(self, exp_line):
# checking semantical equivalence is delegated to solvers
return False

def get_expression(self):
return self

Expand Down Expand Up @@ -777,10 +794,10 @@ def get_instance(self, step):
def set_instance(self, instance, step):
self.cache_instance[step] = instance
if Instance.PROPAGATE > 0:
self.cache_instance[step] = self.cache_instance[step].get_values(step).get_expression()
self.cache_instance[step] = self.cache_instance[step].get_values(step)

def get_z3_select(self, step):
instance = self.get_instance(step)
instance = self.get_instance(step).get_expression()
assert step not in self.cache_z3_instance
domain = instance.get_domain()
if domain:
Expand All @@ -791,7 +808,7 @@ def get_z3_select(self, step):
return self.cache_z3_instance[step]

def get_z3_substitute(self, step):
instance = self.get_instance(step)
instance = self.get_instance(step).get_expression()
assert step not in self.cache_z3_instance
self.cache_z3_instance[step] = instance.get_z3()
domain = instance.get_domain()
Expand All @@ -812,7 +829,7 @@ def get_z3_instance(self, step):
return self.get_z3_substitute(step)

def get_bitwuzla_select(self, step, tm):
instance = self.get_instance(step)
instance = self.get_instance(step).get_expression()
assert step not in self.cache_bitwuzla_instance
domain = instance.get_domain()
if domain:
Expand All @@ -824,7 +841,7 @@ def get_bitwuzla_select(self, step, tm):
return self.cache_bitwuzla_instance[step]

def get_bitwuzla_substitute(self, step, tm):
instance = self.get_instance(step)
instance = self.get_instance(step).get_expression()
assert step not in self.cache_bitwuzla_instance
self.cache_bitwuzla_instance[step] = instance.get_bitwuzla(tm)
domain = instance.get_domain()
Expand Down Expand Up @@ -2028,13 +2045,22 @@ def __str__(self):
def get_z3_step(self, step):
self.state_line.set_instance(self.exp_line, step)
if step not in self.cache_z3_next_state:
self.cache_z3_next_state[step] = self.state_line.get_z3_name(step + 1) == self.state_line.get_z3_instance(step)
if isinstance(self.state_line.get_instance(step), Values):
self.cache_z3_next_state[step] = z3.BoolVal(True)
else:
self.cache_z3_next_state[step] = self.state_line.get_z3_name(step + 1) == self.state_line.get_z3_instance(step)
return self.cache_z3_next_state[step]

def get_z3_is_state_changing(self, step):
self.state_line.set_instance(self.exp_line, step)
if step not in self.cache_z3_is_state_changing:
self.cache_z3_is_state_changing[step] = self.state_line.get_z3_name(step) != self.state_line.get_z3_instance(step)
if self.state_line.has_instance(step - 1):
if self.state_line.get_instance(step).is_equal(self.state_line.get_instance(step - 1)):
self.cache_z3_is_state_changing[step] = z3.BoolVal(False)
else:
self.cache_z3_is_state_changing[step] = self.state_line.get_z3_instance(step) != self.state_line.get_z3_instance(step - 1)
else:
self.cache_z3_is_state_changing[step] = z3.BoolVal(False)
return self.cache_z3_is_state_changing[step]

def get_z3_state_is_not_changing(self, step):
Expand All @@ -2046,17 +2072,26 @@ def get_z3_state_is_not_changing(self, step):
def get_bitwuzla_step(self, step, tm):
self.state_line.set_instance(self.exp_line, step)
if step not in self.cache_bitwuzla_next_state:
self.cache_bitwuzla_next_state[step] = tm.mk_term(bitwuzla.Kind.EQUAL,
[self.state_line.get_bitwuzla_name(step + 1, tm),
self.state_line.get_bitwuzla_instance(step, tm)])
if isinstance(self.state_line.get_instance(step), Values):
self.cache_bitwuzla_next_state[step] = tm.mk_true()
else:
self.cache_bitwuzla_next_state[step] = tm.mk_term(bitwuzla.Kind.EQUAL,
[self.state_line.get_bitwuzla_name(step + 1, tm),
self.state_line.get_bitwuzla_instance(step, tm)])
return self.cache_bitwuzla_next_state[step]

def get_bitwuzla_is_state_changing(self, step, tm):
self.state_line.set_instance(self.exp_line, step)
if step not in self.cache_bitwuzla_is_state_changing:
self.cache_bitwuzla_is_state_changing[step] = tm.mk_term(bitwuzla.Kind.DISTINCT,
[self.state_line.get_bitwuzla_name(step, tm),
self.state_line.get_bitwuzla_instance(step, tm)])
if self.state_line.has_instance(step - 1):
if self.state_line.get_instance(step).is_equal(self.state_line.get_instance(step - 1)):
self.cache_bitwuzla_is_state_changing[step] = tm.mk_false()
else:
self.cache_bitwuzla_is_state_changing[step] = tm.mk_term(bitwuzla.Kind.DISTINCT,
[self.state_line.get_bitwuzla_instance(step, tm),
self.state_line.get_bitwuzla_instance(step - 1, tm)])
else:
self.cache_bitwuzla_is_state_changing[step] = tm.mk_false()
return self.cache_bitwuzla_is_state_changing[step]

def get_bitwuzla_state_is_not_changing(self, step, tm):
Expand Down

0 comments on commit 9b3143f

Please sign in to comment.