(self, stack, tokens, key)
Utility function that handles _ special function in SMTLIB
Utility function that handles _ special function in SMTLIB
Utility function that handles _ special function in SMTLIB
def _smtlib_underscore(self, stack, tokens, key):
        #pylint: disable=unused-argument
        """Utility function that handles _ special function in SMTLIB"""
        mgr = self.env.formula_manager

        op = self.parse_atom(tokens, "expression")

        fun = None
        if op == "extract":
            send = self.parse_atom(tokens, "expression")
            sstart = self.parse_atom(tokens, "expression")
            try:
                start = int(sstart)
                end = int(send)
            except ValueError:
                raise PysmtSyntaxError("Expected number in '_ extract' "
                                       "expression", tokens.pos_info)
            fun = lambda x : mgr.BVExtract(x, start, end)

        elif op == "zero_extend":
            swidth = self.parse_atom(tokens, "expression")
            try:
                width = int(swidth)
            except ValueError:
                raise PysmtSyntaxError("Expected number in '_ zero_extend' "
                                       "expression", tokens.pos_info)
            fun = lambda x: mgr.BVZExt(x, width)

        elif op == "repeat":
            scount = self.parse_atom(tokens, "expression")
            try:
                count = int(scount)
            except ValueError:
                raise PysmtSyntaxError("Expected number in '_ repeat' "
                                       "expression", tokens.pos_info)
            fun = lambda x: mgr.BVRepeat(x, count)

        elif op == "rotate_left":
            sstep = self.parse_atom(tokens, "expression")
            try:
                step = int(sstep)
            except ValueError:
                raise PysmtSyntaxError("Expected number in '_ rotate_left' "
                                       "expression", tokens.pos_info)
            fun = lambda x: mgr.BVRol(x, step)

        elif op == "rotate_right":
            sstep = self.parse_atom(tokens, "expression")
            try:
                step = int(sstep)
            except ValueError:
                raise PysmtSyntaxError("Expected number in '_ rotate_left' "
                                       "expression", tokens.pos_info)
            fun = lambda x: mgr.BVRor(x, step)

        elif op == "sign_extend":
            swidth = self.parse_atom(tokens, "expression")
            try:
                width = int(swidth)
            except ValueError:
                raise PysmtSyntaxError("Expected number in '(_ sign_extend) "
                                       "expression'", tokens.pos_info)
            fun = lambda x: mgr.BVSExt(x, width)

        elif op.startswith("bv"):
            try:
                v = int(op[2:])
                width = int(self.parse_atom(tokens, "expression"))
            except ValueError:
                raise PysmtSyntaxError("Expected number in '_ bv' expression: "
                                       "'%s'" % op, tokens.pos_info)
            fun = mgr.BV(v, width)

        else:
            raise PysmtSyntaxError("Unexpected '_' expression '%s'" % op,
                                   tokens.pos_info)

        stack[-1].append(lambda : fun)
def _smtlib_underscore ( self , stack , tokens , key ) : #pylint: disable=unused-argument mgr = self . env . formula_manager op = self . parse_atom ( tokens , "expression" ) fun = None if op == "extract" : send = self . parse_atom ( tokens , "expression" ) sstart = self . parse_atom ( tokens , "expression" ) try : start = int ( sstart ) end = int ( send ) except ValueError : raise PysmtSyntaxError ( "Expected number in '_ extract' " "expression" , tokens . pos_info ) fun = lambda x : mgr . BVExtract ( x , start , end ) elif op == "zero_extend" : swidth = self . parse_atom ( tokens , "expression" ) try : width = int ( swidth ) except ValueError : raise PysmtSyntaxError ( "Expected number in '_ zero_extend' " "expression" , tokens . pos_info ) fun = lambda x : mgr . BVZExt ( x , width ) elif op == "repeat" : scount = self . parse_atom ( tokens , "expression" ) try : count = int ( scount ) except ValueError : raise PysmtSyntaxError ( "Expected number in '_ repeat' " "expression" , tokens . pos_info ) fun = lambda x : mgr . BVRepeat ( x , count ) elif op == "rotate_left" : sstep = self . parse_atom ( tokens , "expression" ) try : step = int ( sstep ) except ValueError : raise PysmtSyntaxError ( "Expected number in '_ rotate_left' " "expression" , tokens . pos_info ) fun = lambda x : mgr . BVRol ( x , step ) elif op == "rotate_right" : sstep = self . parse_atom ( tokens , "expression" ) try : step = int ( sstep ) except ValueError : raise PysmtSyntaxError ( "Expected number in '_ rotate_left' " "expression" , tokens . pos_info ) fun = lambda x : mgr . BVRor ( x , step ) elif op == "sign_extend" : swidth = self . parse_atom ( tokens , "expression" ) try : width = int ( swidth ) except ValueError : raise PysmtSyntaxError ( "Expected number in '(_ sign_extend) " "expression'" , tokens . pos_info ) fun = lambda x : mgr . BVSExt ( x , width ) elif op . startswith ( "bv" ) : try : v = int ( op [ 2 : ] ) width = int ( self . parse_atom ( tokens , "expression" ) ) except ValueError : raise PysmtSyntaxError ( "Expected number in '_ bv' expression: " "'%s'" % op , tokens . pos_info ) fun = mgr . BV ( v , width ) else : raise PysmtSyntaxError ( "Unexpected '_' expression '%s'" % op , tokens . pos_info ) stack [ - 1 ] . append ( lambda : fun )