<s> """<STR_LIT:U+0020>""" <EOL> from operator import itemgetter <EOL> from general import IvyError <EOL> from utils . recstruct_object import recstruct <EOL> class SortError ( IvyError ) : <EOL> pass <EOL> class UninterpretedSort ( recstruct ( '<STR_LIT>' , [ '<STR_LIT:name>' ] , [ ] ) ) : <EOL> __slots__ = ( ) <EOL> def __str__ ( self ) : <EOL> return self . name <EOL> class BooleanSort ( recstruct ( '<STR_LIT>' , [ ] , [ ] ) ) : <EOL> __slots__ = ( ) <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' <EOL> Boolean = BooleanSort ( ) <EOL> class FunctionSort ( recstruct ( '<STR_LIT>' , [ ] , [ '<STR_LIT>' ] ) ) : <EOL> __slots__ = ( ) <EOL> @ classmethod <EOL> def _preprocess_ ( cls , * sorts ) : <EOL> if len ( sorts ) == <NUM_LIT:0> : <EOL> raise IvyError ( "<STR_LIT>" ) <EOL> if any ( not first_order_sort ( s ) for s in sorts ) : <EOL> raise IvyError ( "<STR_LIT>" ) <EOL> return sorts <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' . join ( str ( s ) for s in self . domain ) + '<STR_LIT>' + str ( self . range ) <EOL> domain = property ( itemgetter ( slice ( None , - <NUM_LIT:1> ) ) , doc = '<STR_LIT>' ) <EOL> range = property ( itemgetter ( - <NUM_LIT:1> ) ) <EOL> arity = property ( lambda self : len ( self . domain ) ) <EOL> class TopSort ( recstruct ( '<STR_LIT>' , [ '<STR_LIT>' ] , [ ] ) ) : <EOL> """<STR_LIT>""" <EOL> __slots__ = ( ) <EOL> @ classmethod <EOL> def _preprocess_ ( cls , name ) : <EOL> return ( name , ) <EOL> def __str__ ( self ) : <EOL> return self . name <EOL> def is_sort_variable ( self ) : <EOL> return self . name != '<STR_LIT>' <EOL> TopS = TopSort ( ) <EOL> def first_order_sort ( s ) : <EOL> return type ( s ) is not FunctionSort <EOL> def contains_topsort ( x ) : <EOL> """<STR_LIT>""" <EOL> return ( <EOL> x == TopS or <EOL> hasattr ( x , '<STR_LIT>' ) and contains_topsort ( x . sort ) or <EOL> any ( contains_topsort ( y ) for y in x ) <EOL> ) <EOL> def is_polymorphic ( x ) : <EOL> """<STR_LIT>""" <EOL> return ( <EOL> type ( x ) == TopSort and x . is_sort_variable ( ) or <EOL> hasattr ( x , '<STR_LIT>' ) and is_polymorphic ( x . sort ) or <EOL> any ( is_polymorphic ( y ) for y in x ) <EOL> ) <EOL> class Var ( recstruct ( '<STR_LIT>' , [ '<STR_LIT:name>' , '<STR_LIT>' ] , [ ] ) ) : <EOL> __slots__ = ( ) <EOL> @ classmethod <EOL> def _preprocess_ ( cls , name , sort ) : <EOL> if name and not name [ <NUM_LIT:0> ] . isupper ( ) : <EOL> raise IvyError ( "<STR_LIT>" . format ( name ) ) <EOL> return name , sort <EOL> def __str__ ( self ) : <EOL> return self . name <EOL> def __call__ ( self , * terms ) : <EOL> return Apply ( self , * terms ) <EOL> class Const ( recstruct ( '<STR_LIT>' , [ '<STR_LIT:name>' , '<STR_LIT>' ] , [ ] ) ) : <EOL> __slots__ = ( ) <EOL> @ classmethod <EOL> def _preprocess_ ( cls , name , sort ) : <EOL> return name , sort <EOL> def __str__ ( self ) : <EOL> return self . name <EOL> def __call__ ( self , * terms ) : <EOL> return Apply ( self , * terms ) <EOL> class Apply ( recstruct ( '<STR_LIT>' , [ ] , [ '<STR_LIT>' , '<STR_LIT>' ] ) ) : <EOL> __slots__ = ( ) <EOL> @ classmethod <EOL> def _preprocess_ ( cls , func , * terms ) : <EOL> if type ( func . sort ) is TopSort : <EOL> pass <EOL> elif type ( func . sort ) is not FunctionSort : <EOL> raise SortError ( "<STR_LIT>" . format ( func ) ) <EOL> elif func . sort . arity != len ( terms ) : <EOL> print func . sort . arity <EOL> print func . sort <EOL> raise SortError ( "<STR_LIT>" . format ( <EOL> str ( func ) , <EOL> '<STR_LIT:U+002CU+0020>' . join ( str ( t ) for t in terms ) <EOL> ) ) <EOL> else : <EOL> bad_sorts = [ i for i in range ( func . sort . arity ) if <EOL> terms [ i ] . sort != func . sort . domain [ i ] and <EOL> not any ( type ( t ) is TopSort for t in ( terms [ i ] . sort , func . sort . domain [ i ] ) ) ] <EOL> if len ( bad_sorts ) > <NUM_LIT:0> : <EOL> raise SortError ( "<STR_LIT>" . format ( <EOL> str ( func ) , <EOL> '<STR_LIT:U+002CU+0020>' . join ( repr ( t ) for t in terms ) , <EOL> bad_sorts , <EOL> ) ) <EOL> return ( func , ) + terms <EOL> def __str__ ( self ) : <EOL> if len ( self . terms ) == <NUM_LIT:0> : <EOL> return str ( self . func ) <EOL> else : <EOL> return '<STR_LIT>' . format ( <EOL> str ( self . func ) , <EOL> '<STR_LIT:U+002CU+0020>' . join ( str ( t ) for t in self . terms ) <EOL> ) <EOL> sort = property ( lambda self : TopS if self . func . sort == TopS else <EOL> self . func . sort . range ) <EOL> class Eq ( recstruct ( '<STR_LIT>' , [ ] , [ '<STR_LIT>' , '<STR_LIT>' ] ) ) : <EOL> __slots__ = ( ) <EOL> sort = Boolean <EOL> @ classmethod <EOL> def _preprocess_ ( cls , t1 , t2 ) : <EOL> if TopS in ( t1 . sort , t2 . sort ) : <EOL> pass <EOL> elif t1 . sort != t2 . sort : <EOL> raise SortError ( "<STR_LIT>" . format ( t1 , t1 . sort , t2 , t2 . sort ) ) <EOL> elif not first_order_sort ( t1 . sort ) : <EOL> raise SortError ( "<STR_LIT>" . format ( t1 , t2 ) ) <EOL> return t1 , t2 <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' . format ( self . t1 , self . t2 ) <EOL> class Ite ( recstruct ( '<STR_LIT>' , [ ] , [ '<STR_LIT>' , '<STR_LIT>' , '<STR_LIT>' ] ) ) : <EOL> __slots__ = ( ) <EOL> @ classmethod <EOL> def _preprocess_ ( cls , cond , t_then , t_else ) : <EOL> if cond . sort not in ( Boolean , TopS ) : <EOL> raise SortError ( "<STR_LIT>" . format ( body ) ) <EOL> elif TopS in ( t_then . sort , t_else . sort ) : <EOL> pass <EOL> elif t_then . sort != t_else . sort : <EOL> raise SortError ( "<STR_LIT>" . format ( t_then , t_else ) ) <EOL> elif not first_order_sort ( t_then . sort ) : <EOL> pass <EOL> return cond , t_then , t_else <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' . format ( self . cond , self . t_then , self . t_else ) <EOL> sort = property ( lambda self : self . t_then . sort if self . t_then . sort != TopS else self . t_else . sort ) <EOL> class Not ( recstruct ( '<STR_LIT>' , [ ] , [ '<STR_LIT:body>' ] ) ) : <EOL> __slots__ = ( ) <EOL> sort = Boolean <EOL> @ classmethod <EOL> def _preprocess_ ( cls , body ) : <EOL> if body . sort not in ( Boolean , TopS ) : <EOL> raise SortError ( "<STR_LIT>" . format ( body ) ) <EOL> return ( body , ) <EOL> def __str__ ( self ) : <EOL> if type ( self . body ) is Eq : <EOL> return '<STR_LIT>' . format ( self . body . t1 , self . body . t2 ) <EOL> else : <EOL> return '<STR_LIT>' . format ( self . body ) <EOL> class And ( recstruct ( '<STR_LIT>' , [ ] , [ '<STR_LIT>' ] ) ) : <EOL> __slots__ = ( ) <EOL> sort = Boolean <EOL> @ classmethod <EOL> def _preprocess_ ( cls , * terms ) : <EOL> bad_sorts = [ i for i , t in enumerate ( terms ) <EOL> if t . sort not in ( Boolean , TopS ) ] <EOL> if len ( bad_sorts ) > <NUM_LIT:0> : <EOL> raise SortError ( "<STR_LIT>" . format ( <EOL> '<STR_LIT:U+002CU+0020>' . join ( str ( t ) for t in terms ) , <EOL> bad_sorts , <EOL> ) ) <EOL> return sorted ( set ( terms ) ) <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' . format ( <EOL> '<STR_LIT:U+002CU+0020>' . join ( str ( t ) for t in self ) <EOL> ) <EOL> class Or ( recstruct ( '<STR_LIT>' , [ ] , [ '<STR_LIT>' ] ) ) : <EOL> __slots__ = ( ) <EOL> sort = Boolean <EOL> @ classmethod <EOL> def _preprocess_ ( cls , * terms ) : <EOL> bad_sorts = [ i for i , t in enumerate ( terms ) <EOL> if t . sort not in ( Boolean , TopS ) ] <EOL> if len ( bad_sorts ) > <NUM_LIT:0> : <EOL> raise SortError ( "<STR_LIT>" . format ( <EOL> '<STR_LIT:U+002CU+0020>' . join ( str ( t ) for t in terms ) , <EOL> bad_sorts , <EOL> ) ) <EOL> return sorted ( set ( terms ) ) <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' . format ( <EOL> '<STR_LIT:U+002CU+0020>' . join ( str ( t ) for t in self ) <EOL> ) <EOL> class Implies ( recstruct ( '<STR_LIT>' , [ ] , [ '<STR_LIT>' , '<STR_LIT>' ] ) ) : <EOL> __slots__ = ( ) <EOL> sort = Boolean <EOL> @ classmethod <EOL> def _preprocess_ ( cls , t1 , t2 ) : <EOL> bad_sorts = [ i for i , t in enumerate ( [ t1 , t2 ] ) <EOL> if t . sort not in ( Boolean , TopS ) ] <EOL> if len ( bad_sorts ) > <NUM_LIT:0> : <EOL> raise SortError ( "<STR_LIT>" . format ( <EOL> t1 , t2 , bad_sorts , <EOL> ) ) <EOL> return t1 , t2 <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' . format ( self . t1 , self . t2 ) <EOL> class Iff ( recstruct ( '<STR_LIT>' , [ ] , [ '<STR_LIT>' , '<STR_LIT>' ] ) ) : <EOL> __slots__ = ( ) <EOL> sort = Boolean <EOL> @ classmethod <EOL> def _preprocess_ ( cls , t1 , t2 ) : <EOL> bad_sorts = [ i for i , t in enumerate ( [ t1 , t2 ] ) <EOL> if t . sort not in ( Boolean , TopS ) ] <EOL> if len ( bad_sorts ) > <NUM_LIT:0> : <EOL> raise SortError ( "<STR_LIT>" . format ( <EOL> t1 , t2 , bad_sorts , <EOL> ) ) <EOL> return t1 , t2 <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' . format ( self . t1 , self . t2 ) <EOL> class ForAll ( recstruct ( '<STR_LIT>' , [ '<STR_LIT>' ] , [ '<STR_LIT:body>' ] ) ) : <EOL> __slots__ = ( ) <EOL> sort = Boolean <EOL> @ classmethod <EOL> def _preprocess_ ( cls , variables , body ) : <EOL> if not all ( type ( v ) is Var for v in variables ) : <EOL> raise IvyError ( "<STR_LIT>" ) <EOL> if body . sort not in ( Boolean , TopS ) : <EOL> raise SortError ( "<STR_LIT>" , body ) <EOL> return frozenset ( variables ) , body <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' . format ( <EOL> '<STR_LIT:U+002CU+0020>' . join ( '<STR_LIT>' . format ( v . name , v . sort ) for v in sorted ( self . variables ) ) , <EOL> self . body ) <EOL> class Exists ( recstruct ( '<STR_LIT>' , [ '<STR_LIT>' ] , [ '<STR_LIT:body>' ] ) ) : <EOL> __slots__ = ( ) <EOL> sort = Boolean <EOL> @ classmethod <EOL> def _preprocess_ ( cls , variables , body ) : <EOL> if not all ( type ( v ) is Var for v in variables ) : <EOL> raise IvyError ( "<STR_LIT>" ) <EOL> if body . sort not in ( Boolean , TopS ) : <EOL> raise SortError ( "<STR_LIT>" , body ) <EOL> return frozenset ( variables ) , body <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT>' . format ( <EOL> '<STR_LIT:U+002CU+0020>' . join ( '<STR_LIT>' . format ( v . name , v . sort ) for v in sorted ( self . variables ) ) , <EOL> self . body ) <EOL> true = Const ( '<STR_LIT:true>' , Boolean ) <EOL> false = Const ( '<STR_LIT:false>' , Boolean ) <EOL> if __name__ == '<STR_LIT:__main__>' : <EOL> S = UninterpretedSort ( '<STR_LIT:S>' ) <EOL> X , Y , Z = ( Var ( n , S ) for n in [ '<STR_LIT:X>' , '<STR_LIT:Y>' , '<STR_LIT>' ] ) <EOL> BinRel = FunctionSort ( S , S , Boolean ) <EOL> leq = Const ( '<STR_LIT>' , BinRel ) <EOL> transitive1 = ForAll ( ( X , Y , Z ) , Implies ( And ( leq ( X , Y ) , leq ( Y , Z ) ) , leq ( X , Z ) ) ) <EOL> transitive2 = ForAll ( ( X , Y , Z ) , Or ( Not ( leq ( X , Y ) ) , Not ( leq ( Y , Z ) ) , leq ( X , Z ) ) ) <EOL> transitive3 = Not ( Exists ( ( X , Y , Z ) , And ( leq ( X , Y ) , leq ( Y , Z ) , Not ( leq ( X , Z ) ) ) ) ) <EOL> antisymmetric = ForAll ( ( X , Y ) , Implies ( And ( leq ( X , Y ) , leq ( Y , X ) ) , Eq ( Y , X ) ) ) <EOL> assert Eq ( X , Y ) == Eq ( Y , X ) <EOL> X , Y = ( Var ( n , TopS ) for n in [ '<STR_LIT:X>' , '<STR_LIT:Y>' ] ) <EOL> f = Const ( '<STR_LIT:f>' , FunctionSort ( TopS , TopS , Boolean ) ) <EOL> g = Const ( '<STR_LIT:g>' , FunctionSort ( S , S , Boolean ) ) <EOL> h = Const ( '<STR_LIT:h>' , TopS ) <EOL> partial_function1 = ForAll ( [ X , Y , Z ] , Implies ( And ( f ( X , Y ) , f ( X , Z ) ) , Eq ( Y , Z ) ) ) <EOL> partial_function2 = ForAll ( [ X , Y , Z ] , Implies ( And ( g ( X , Y ) , g ( X , Z ) ) , Eq ( Y , Z ) ) ) <EOL> partial_function3 = ForAll ( [ X , Y , Z ] , Implies ( And ( h ( X , Y ) , h ( X , Z ) ) , Eq ( Y , Z ) ) ) <EOL> assert contains_topsort ( X ) <EOL> assert not contains_topsort ( Z ) <EOL> assert contains_topsort ( f ) <EOL> assert not contains_topsort ( g ) <EOL> assert contains_topsort ( h ) </s>
