parameters: (self,fmla)
return_statement: return (vs,insts)
docstring: Return the set of satisfying assignments to the free variables in fmla. Returns
              a table in the format (vars,rows), where each row is a tuple of values of the
              variables in vars.
docstring_summary: Return the set of satisfying assignments to the free variables in fmla. Returns
              a table in the format (vars,rows), where each row is a tuple of values of the
              variables in vars.
docstring_tokens: Return the set of satisfying assignments to the free variables in fmla . Returns a table in the format ( vars rows ) where each row is a tuple of values of the variables in vars .
function: def check(self,fmla):
          """ Return the set of satisfying assignments to the free variables in fmla. Returns
              a table in the format (vars,rows), where each row is a tuple of values of the
              variables in vars.
          """
          vs = list(variables_ast(fmla))
          s = self.solver
          m = self.model
          ranges = [enumerated_range(x.sort) if isinstance(x.sort,ivy_logic.EnumeratedSort) else
                    self.constants[x.sort] for x in vs]
          z3_fmla = literal_to_z3(fmla)
  #        print "z3_fmla = {}".format(z3_fmla)
          z3_vs = [term_to_z3(v) for v in vs]
          insts = []
          for tup in itertools.product(*ranges):
              interp = zip(z3_vs,tup)
              fact = substitute(z3_fmla,*interp)
              fact_val = m.eval(fact,model_completion=True)
  #            print "%s = %s" % (fact,fact_val)
              if z3.is_true(fact_val):
                  args = [constant_from_z3(v.sort,y) for v,y in zip(vs,tup)]
                  insts.append(args)
          return (vs,insts)
function_tokens: def check ( self , fmla ) : vs = list ( variables_ast ( fmla ) ) s = self . solver m = self . model ranges = [ enumerated_range ( x . sort ) if isinstance ( x . sort , ivy_logic . EnumeratedSort ) else self . constants [ x . sort ] for x in vs ] z3_fmla = literal_to_z3 ( fmla ) #        print "z3_fmla = {}".format(z3_fmla) z3_vs = [ term_to_z3 ( v ) for v in vs ] insts = [ ] for tup in itertools . product ( * ranges ) : interp = zip ( z3_vs , tup ) fact = substitute ( z3_fmla , * interp ) fact_val = m . eval ( fact , model_completion = True ) #            print "%s = %s" % (fact,fact_val) if z3 . is_true ( fact_val ) : args = [ constant_from_z3 ( v . sort , y ) for v , y in zip ( vs , tup ) ] insts . append ( args ) return ( vs , insts )