(self, stack, tokens, key)
Utility function that handles 'as' that is a special function in SMTLIB
Utility function that handles 'as' that is a special function in SMTLIB
Utility function that handles as that is a special function in SMTLIB
def _enter_smtlib_as(self, stack, tokens, key):
        """Utility function that handles 'as' that is a special function in SMTLIB"""
        #pylint: disable=unused-argument
        what = self.parse_atom(tokens, "expression")
        ty = self.parse_type(tokens, "expression")
        if what == "const":
            assert ty.is_array_type(), "(as const x) is supported only for array constants"
            def res(expr):
                return self.env.formula_manager.Array(ty.index_type, expr)
            def handler():
                return res
            stack[-1].append(handler)
        else:
            def handler():
                return self.env.formula_manager.Symbol(what, ty)
            stack[-1].append(handler)
def _enter_smtlib_as ( self , stack , tokens , key ) : #pylint: disable=unused-argument what = self . parse_atom ( tokens , "expression" ) ty = self . parse_type ( tokens , "expression" ) if what == "const" : assert ty . is_array_type ( ) , "(as const x) is supported only for array constants" def res ( expr ) : return self . env . formula_manager . Array ( ty . index_type , expr ) def handler ( ) : return res stack [ - 1 ] . append ( handler ) else : def handler ( ) : return self . env . formula_manager . Symbol ( what , ty ) stack [ - 1 ] . append ( handler )