Skip to content

Commit

Permalink
Test.
Browse files Browse the repository at this point in the history
  • Loading branch information
mpreiner committed Apr 22, 2024
1 parent 8ea5677 commit 24478e4
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 31 deletions.
60 changes: 30 additions & 30 deletions ddsmt/mutators_bv.py
Original file line number Diff line number Diff line change
Expand Up @@ -457,35 +457,35 @@ def __str__(self):
return 'merge previous bit-width reductions'


class BvMergeExtend:
"""Merge nested zero_extend/sign_extend terms.
For example, ``((_ zero_extend 5) ((_ zero_extend 4) x))`` is transformed
into ``((zero_extend 9) x)``.
"""

def filter(self, node):
return (is_indexed_operator_app(node, 'zero_extend') and \
is_indexed_operator_app(node[1], 'zero_extend')) or \
(is_indexed_operator_app(node, 'sign_extend') and
is_indexed_operator_app(node[1], 'sign_extend'))

def mutations(self, node):
op = 'sign_extend'
if is_indexed_operator_app(node, 'zero_extend'):
op = 'zero_extend'

n = node
ext = 0
while is_indexed_operator_app(n, op):
indices = get_indices(n[0], op)
ext += indices[0]
n = n[1]

return [Simplification({node.id: Node(('_', op, ext), n)}, [])]

def __str__(self):
return 'merge nested zero_extend/sign_extend'
#class BvMergeExtend:
# """Merge nested zero_extend/sign_extend terms.
#
# For example, ``((_ zero_extend 5) ((_ zero_extend 4) x))`` is transformed
# into ``((zero_extend 9) x)``.
# """
#
# def filter(self, node):
# return (is_indexed_operator_app(node, 'zero_extend') and \
# is_indexed_operator_app(node[1], 'zero_extend')) or \
# (is_indexed_operator_app(node, 'sign_extend') and
# is_indexed_operator_app(node[1], 'sign_extend'))
#
# def mutations(self, node):
# op = 'sign_extend'
# if is_indexed_operator_app(node, 'zero_extend'):
# op = 'zero_extend'
#
# n = node
# ext = 0
# while is_indexed_operator_app(n, op):
# indices = get_indices(n[0], op)
# ext += indices[0]
# n = n[1]
#
# return [Simplification({node.id: Node(('_', op, ext), n)}, [])]
#
# def __str__(self):
# return 'merge nested zero_extend/sign_extend'


def get_mutators():
Expand All @@ -506,7 +506,7 @@ def get_mutators():
'BVTransformToBool': 'bv-to-bool',
'BVZeroExtendPredicate': 'bv-zeroextend-pred',
'BVReduceBW': 'bv-reduce-bitwidth',
'BvMergeExtend': 'bv-merge-extend',
# 'BvMergeExtend': 'bv-merge-extend',
}


Expand Down
2 changes: 1 addition & 1 deletion ddsmt/tests/test_mutators_bv.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
def test_bv_get_mutators():
d = mutators_bv.get_mutators()
assert isinstance(d, dict)
assert len(d) == 15
assert len(d) == 14


def test_bv_is_relevant():
Expand Down

0 comments on commit 24478e4

Please sign in to comment.