<s> """<STR_LIT>""" <EOL> from itertools import product , chain <EOL> from logic import ( Var , Const , Apply , Eq , Ite , Not , And , Or , Implies , <EOL> Iff , ForAll , Exists ) <EOL> from logic import ( UninterpretedSort , FunctionSort , Boolean , TopSort , <EOL> SortError , contains_topsort , is_polymorphic ) <EOL> from logic_util import used_constants , free_variables <EOL> class SortVar ( object ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self ) : <EOL> self . instance = None <EOL> def __str__ ( self ) : <EOL> if self . instance is not None : <EOL> return str ( self . instance ) <EOL> else : <EOL> return repr ( self ) <EOL> def find ( x ) : <EOL> """<STR_LIT>""" <EOL> if type ( x ) is not SortVar or x . instance is None : <EOL> return x <EOL> else : <EOL> x . instance = find ( x . instance ) <EOL> return x . instance <EOL> def occurs_in ( s1 , s2 ) : <EOL> """<STR_LIT>""" <EOL> s1 = find ( s1 ) <EOL> s2 = find ( s2 ) <EOL> return ( s1 == s2 or ( <EOL> type ( s2 ) is FunctionSort and <EOL> any ( occurs_in ( s1 , x ) for x in s2 ) <EOL> ) ) <EOL> def unify ( s1 , s2 ) : <EOL> """<STR_LIT>""" <EOL> s1 = find ( s1 ) <EOL> s2 = find ( s2 ) <EOL> if ( s1 == s2 or <EOL> type ( s1 ) is TopSort or <EOL> type ( s2 ) is TopSort ) : <EOL> pass <EOL> elif type ( s1 ) is SortVar : <EOL> assert s1 . instance is None <EOL> if occurs_in ( s1 , s2 ) : <EOL> raise SortError ( "<STR_LIT>" . format ( s1 , s2 ) ) <EOL> else : <EOL> s1 . instance = s2 <EOL> elif type ( s2 ) is SortVar : <EOL> unify ( s2 , s1 ) <EOL> elif ( type ( s1 ) is FunctionSort and <EOL> type ( s2 ) is FunctionSort and <EOL> s1 . arity == s2 . arity ) : <EOL> for x , y in zip ( s1 , s2 ) : <EOL> unify ( x , y ) <EOL> else : <EOL> raise SortError ( "<STR_LIT>" . format ( s1 , s2 ) ) <EOL> def convert_from_sortvars ( s ) : <EOL> """<STR_LIT>""" <EOL> s = find ( s ) <EOL> if type ( s ) is SortVar : <EOL> return TopSort ( ) <EOL> elif type ( s ) is FunctionSort : <EOL> return FunctionSort ( * ( <EOL> convert_from_sortvars ( x ) for x in s <EOL> ) ) <EOL> else : <EOL> return s <EOL> def insert_sortvars ( s , env ) : <EOL> """<STR_LIT>""" <EOL> if type ( s ) is TopSort and s . is_sort_variable ( ) : <EOL> if s not in env : <EOL> env [ s ] = SortVar ( ) <EOL> return env [ s ] <EOL> elif type ( s ) is FunctionSort : <EOL> return FunctionSort ( * ( <EOL> insert_sortvars ( x , env ) for x in s <EOL> ) ) <EOL> else : <EOL> return s <EOL> def infer_sorts ( t , env = None ) : <EOL> """<STR_LIT>""" <EOL> if env is None : <EOL> names = free_variables ( t , by_name = True ) . union ( <EOL> x . name for x in used_constants ( t ) <EOL> ) <EOL> env = dict ( ( name , SortVar ( ) ) for name in names ) <EOL> if type ( t ) in ( Var , Const ) : <EOL> if is_polymorphic ( t ) : <EOL> s = insert_sortvars ( t . sort , { } ) <EOL> else : <EOL> s = env [ t . name ] <EOL> unify ( s , t . sort ) <EOL> return s , lambda : type ( t ) ( t . name , convert_from_sortvars ( s ) ) <EOL> elif type ( t ) is Apply : <EOL> func_s , func_t = infer_sorts ( t . func , env ) <EOL> xys = [ infer_sorts ( tt , env ) for tt in t . terms ] <EOL> terms_s = [ x for x , y in xys ] <EOL> terms_t = [ y for x , y in xys ] <EOL> sorts = terms_s + [ SortVar ( ) ] <EOL> unify ( func_s , FunctionSort ( * sorts ) ) <EOL> return sorts [ - <NUM_LIT:1> ] , lambda : Apply ( func_t ( ) , * ( <EOL> x ( ) for x in terms_t <EOL> ) ) <EOL> elif type ( t ) is Eq : <EOL> s1 , t1 = infer_sorts ( t . t1 , env ) <EOL> s2 , t2 = infer_sorts ( t . t2 , env ) <EOL> unify ( s1 , s2 ) <EOL> return Boolean , lambda : Eq ( t1 ( ) , t2 ( ) ) <EOL> elif type ( t ) is Ite : <EOL> s_cond , t_cond = infer_sorts ( t . cond , env ) <EOL> s_then , t_then = infer_sorts ( t . t_then , env ) <EOL> s_else , t_else = infer_sorts ( t . t_else , env ) <EOL> unify ( s_cond , Boolean ) <EOL> unify ( s_then , s_else ) <EOL> return s_then , lambda : Ite ( t_cond ( ) , t_then ( ) , t_else ( ) ) <EOL> elif type ( t ) in ( Not , And , Or , Implies , Iff ) : <EOL> xys = [ infer_sorts ( tt , env ) for tt in t ] <EOL> terms_s = [ x for x , y in xys ] <EOL> terms_t = [ y for x , y in xys ] <EOL> for s in terms_s : <EOL> unify ( s , Boolean ) <EOL> return Boolean , lambda : type ( t ) ( * [ <EOL> x ( ) for x in terms_t <EOL> ] ) <EOL> elif type ( t ) in ( ForAll , Exists ) : <EOL> env = env . copy ( ) <EOL> env . update ( ( v . name , SortVar ( ) ) for v in t . variables ) <EOL> vars_t = [ infer_sorts ( v , env ) [ <NUM_LIT:1> ] for v in t . variables ] <EOL> body_s , body_t = infer_sorts ( t . body , env ) <EOL> unify ( body_s , Boolean ) <EOL> return Boolean , lambda : type ( t ) ( <EOL> [ x ( ) for x in vars_t ] , <EOL> body_t ( ) , <EOL> ) <EOL> elif hasattr ( t , '<STR_LIT>' ) : <EOL> xys = [ infer_sorts ( tt , env ) for tt in t . args ] <EOL> terms_t = [ y for x , y in xys ] <EOL> return TopSort ( ) , lambda : t . clone ( [ <EOL> x ( ) for x in terms_t <EOL> ] ) <EOL> else : <EOL> assert False , type ( t ) <EOL> def concretize_sorts ( t , sort = None ) : <EOL> """<STR_LIT>""" <EOL> s , tt = infer_sorts ( t ) <EOL> if sort is not None : <EOL> unify ( s , sort ) <EOL> return tt ( ) <EOL> if __name__ == '<STR_LIT:__main__>' : <EOL> S = UninterpretedSort ( '<STR_LIT:S>' ) <EOL> T = TopSort ( ) <EOL> UnaryRelationS = FunctionSort ( S , Boolean ) <EOL> BinaryRelationS = FunctionSort ( S , S , Boolean ) <EOL> UnaryRelationT = FunctionSort ( T , Boolean ) <EOL> BinaryRelationT = FunctionSort ( T , T , Boolean ) <EOL> XS , YS = ( Var ( n , S ) for n in [ '<STR_LIT:X>' , '<STR_LIT:Y>' ] ) <EOL> XT , YT = ( Var ( n , T ) for n in [ '<STR_LIT:X>' , '<STR_LIT:Y>' ] ) <EOL> xs , ys = ( Const ( n , S ) for n in [ '<STR_LIT:x>' , '<STR_LIT:y>' ] ) <EOL> xt , yt = ( Const ( n , T ) for n in [ '<STR_LIT:x>' , '<STR_LIT:y>' ] ) <EOL> rs = Const ( '<STR_LIT:r>' , BinaryRelationS ) <EOL> ps = Const ( '<STR_LIT:p>' , UnaryRelationS ) <EOL> rt = Const ( '<STR_LIT:r>' , BinaryRelationT ) <EOL> pt = Const ( '<STR_LIT:p>' , UnaryRelationT ) <EOL> tt = Const ( '<STR_LIT>' , T ) <EOL> TT = Var ( '<STR_LIT>' , T ) <EOL> f1 = And ( ps ( XS ) , ps ( xs ) ) <EOL> cf1 = concretize_sorts ( f1 ) <EOL> print repr ( f1 ) <EOL> print repr ( cf1 ) <EOL> assert f1 == cf1 <EOL> print <EOL> f2 = And ( ps ( XT ) , pt ( xs ) ) <EOL> cf2 = concretize_sorts ( f2 ) <EOL> print repr ( f2 ) <EOL> print repr ( cf2 ) <EOL> print <EOL> f3 = Exists ( [ TT ] , And ( ps ( XT ) , TT ( xs ) ) ) <EOL> cf3 = concretize_sorts ( f3 ) <EOL> print repr ( f3 ) <EOL> print repr ( cf3 ) <EOL> print <EOL> f4 = Iff ( xt , Ite ( yt , xt , XT ) ) <EOL> cf4 = concretize_sorts ( f4 ) <EOL> print repr ( f4 ) <EOL> print repr ( cf4 ) <EOL> print <EOL> """<STR_LIT>""" </s>
