parameters: (self)
return_statement: return r
docstring: Return a list with all symbols that have an interpretation in the model `self`.
          >>> f = Function('f', IntSort(), IntSort())
          >>> x = Int('x')
          >>> s = Solver()
          >>> s.add(x > 0, x < 2, f(x) == 0)
          >>> s.check()
          sat
          >>> m = s.model()
          >>> m.decls()
          [x, f]
docstring_summary: Return a list with all symbols that have an interpretation in the model `self`.
          >>> f = Function('f', IntSort(), IntSort())
          >>> x = Int('x')
          >>> s = Solver()
          >>> s.add(x > 0, x < 2, f(x) == 0)
          >>> s.check()
          sat
          >>> m = s.model()
          >>> m.decls()
          [x, f]
docstring_tokens: Return a list with all symbols that have an interpretation in the model self . >>> f = Function ( f IntSort () IntSort () ) >>> x = Int ( x ) >>> s = Solver () >>> s . add ( x > 0 x < 2 f ( x ) == 0 ) >>> s . check () sat >>> m = s . model () >>> m . decls () [ x f ]
function: def decls(self):
          """Return a list with all symbols that have an interpretation in the model `self`.
          >>> f = Function('f', IntSort(), IntSort())
          >>> x = Int('x')
          >>> s = Solver()
          >>> s.add(x > 0, x < 2, f(x) == 0)
          >>> s.check()
          sat
          >>> m = s.model()
          >>> m.decls()
          [x, f]
          """
          r = []
          for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)):
              r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx))
          for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)):
              r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
          return r
function_tokens: def decls ( self ) : r = [ ] for i in range ( Z3_model_get_num_consts ( self . ctx . ref ( ) , self . model ) ) : r . append ( FuncDeclRef ( Z3_model_get_const_decl ( self . ctx . ref ( ) , self . model , i ) , self . ctx ) ) for i in range ( Z3_model_get_num_funcs ( self . ctx . ref ( ) , self . model ) ) : r . append ( FuncDeclRef ( Z3_model_get_func_decl ( self . ctx . ref ( ) , self . model , i ) , self . ctx ) ) return r