<s> """<STR_LIT>""" <EOL> from ivy_utils import flatten , gen_to_set , UniqueRenamer , compose_names , split_name , IvyError <EOL> import ivy_utils as iu <EOL> import ivy_logic <EOL> import re <EOL> class AST ( object ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , * args ) : <EOL> self . args = args <EOL> def clone ( self , args ) : <EOL> res = type ( self ) ( * args ) <EOL> if hasattr ( self , '<STR_LIT>' ) : <EOL> res . lineno = self . lineno <EOL> return res <EOL> class Symbol ( AST ) : <EOL> def __init__ ( self , rep , sort ) : <EOL> assert isinstance ( rep , str ) <EOL> self . rep = rep <EOL> self . sort = sort <EOL> def __repr__ ( self ) : <EOL> return self . rep <EOL> def __hash__ ( self ) : <EOL> return hash ( self . rep ) <EOL> def __eq__ ( self , other ) : <EOL> return type ( self ) == type ( other ) and self . rep == other . rep <EOL> def nary_repr ( op , args ) : <EOL> res = ( '<STR_LIT:U+0020>' + op + '<STR_LIT:U+0020>' ) . join ( [ repr ( a ) for a in args ] ) <EOL> return ( '<STR_LIT:(>' + res + '<STR_LIT:)>' ) if len ( args ) > <NUM_LIT:1> else res <EOL> class Formula ( AST ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , * args ) : <EOL> self . args = list ( args ) <EOL> class And ( Formula ) : <EOL> """<STR_LIT>""" <EOL> def __repr__ ( self ) : <EOL> if not self . args : <EOL> return "<STR_LIT:true>" <EOL> return nary_repr ( '<STR_LIT:&>' , self . args ) <EOL> class Or ( Formula ) : <EOL> """<STR_LIT>""" <EOL> def __repr__ ( self ) : <EOL> if not self . args : <EOL> return "<STR_LIT:false>" <EOL> return nary_repr ( '<STR_LIT:|>' , self . args ) <EOL> class Not ( Formula ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , * args ) : <EOL> assert len ( args ) == <NUM_LIT:1> <EOL> self . args = args <EOL> def __repr__ ( self ) : <EOL> if isinstance ( self . args [ <NUM_LIT:0> ] , Atom ) and is_equals ( self . args [ <NUM_LIT:0> ] . rep ) : <EOL> return '<STR_LIT>' . join ( repr ( x ) for x in self . args [ <NUM_LIT:0> ] . args ) <EOL> return '<STR_LIT>' + repr ( self . args [ <NUM_LIT:0> ] ) <EOL> class Let ( Formula ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , * args ) : <EOL> assert len ( args ) >= <NUM_LIT:1> <EOL> self . args = args <EOL> def __repr__ ( self ) : <EOL> res = repr ( self . args [ - <NUM_LIT:1> ] ) <EOL> if len ( self . args ) > <NUM_LIT:1> : <EOL> res = '<STR_LIT>' + '<STR_LIT:U+002CU+0020>' . join ( [ repr ( x ) for x in self . args [ <NUM_LIT:0> : - <NUM_LIT:1> ] ] ) + '<STR_LIT>' + res <EOL> return res <EOL> def defines ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . relname <EOL> def to_constraint ( self ) : <EOL> return Iff ( * self . args ) <EOL> class Definition ( Formula ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , * args ) : <EOL> assert len ( args ) == <NUM_LIT:2> <EOL> self . args = args <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT>' . join ( [ repr ( x ) for x in self . args ] ) <EOL> def defines ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . rep <EOL> def to_constraint ( self ) : <EOL> if isinstance ( self . args [ <NUM_LIT:0> ] , App ) : <EOL> return Atom ( equals , self . args ) <EOL> return Iff ( * self . args ) <EOL> class Implies ( Formula ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , * args ) : <EOL> assert len ( args ) == <NUM_LIT:2> <EOL> self . args = args <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT>' . join ( [ repr ( x ) for x in self . args ] ) <EOL> class Iff ( Formula ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , * args ) : <EOL> assert len ( args ) == <NUM_LIT:2> <EOL> self . args = args <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT>' . join ( [ repr ( x ) for x in self . args ] ) <EOL> class Ite ( AST ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , * args ) : <EOL> assert len ( args ) == <NUM_LIT:3> <EOL> self . args = args <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT:(>' + repr ( self . args [ <NUM_LIT:1> ] ) + '<STR_LIT>' + repr ( self . args [ <NUM_LIT:0> ] ) + '<STR_LIT>' + repr ( self . args [ <NUM_LIT:2> ] ) + '<STR_LIT:)>' <EOL> class Quantifier ( Formula ) : <EOL> def __init__ ( self , bounds , body ) : <EOL> self . bounds = bounds <EOL> self . args = [ body ] <EOL> class Forall ( Quantifier ) : <EOL> pass <EOL> class Exists ( Quantifier ) : <EOL> pass <EOL> class Atom ( Formula ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , relsym , * terms ) : <EOL> self . rep = relsym <EOL> self . args = flatten ( terms ) <EOL> def __repr__ ( self ) : <EOL> if is_equals ( self . rep ) and len ( self . args ) == <NUM_LIT:2> : <EOL> return '<STR_LIT>' . join ( repr ( x ) for x in self . args ) <EOL> if not self . args : <EOL> return str ( self . rep ) <EOL> return str ( self . rep ) + "<STR_LIT:(>" + '<STR_LIT:U+002CU+0020>' . join ( str ( x ) for x in self . args ) + "<STR_LIT:)>" <EOL> def clone ( self , args ) : <EOL> return type ( self ) ( self . rep , list ( args ) ) <EOL> def __eq__ ( self , other ) : <EOL> return type ( self ) == type ( other ) and self . rep == other . rep and self . args == other . args <EOL> def is_numeral ( self ) : <EOL> return False <EOL> def prefix ( self , s ) : <EOL> return Atom ( s + self . rep , * self . args ) <EOL> @ property <EOL> def terms ( self ) : <EOL> return self . args <EOL> @ terms . setter <EOL> def terms ( self , value ) : <EOL> self . args = value <EOL> @ property <EOL> def relname ( self ) : <EOL> return self . rep <EOL> @ relname . setter <EOL> def relname ( self , value ) : <EOL> self . rep = value <EOL> class Term ( AST ) : <EOL> def __eq__ ( self , other ) : <EOL> return _eq_lit ( self , other ) <EOL> def __ne__ ( self , other ) : <EOL> return _neq_lit ( self , other ) <EOL> class Old ( Term ) : <EOL> def __init__ ( self , term ) : <EOL> self . args = [ term ] <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT>' + repr ( self . args [ <NUM_LIT:0> ] ) <EOL> class App ( Term ) : <EOL> def __init__ ( self , funsym , * terms ) : <EOL> self . rep = funsym <EOL> self . args = flatten ( terms ) <EOL> def __repr__ ( self ) : <EOL> if self . args : <EOL> res = repr ( self . rep ) + "<STR_LIT:(>" + '<STR_LIT:U+002CU+0020>' . join ( repr ( x ) for x in self . args ) + "<STR_LIT:)>" <EOL> else : <EOL> res = repr ( self . rep ) <EOL> if hasattr ( self , '<STR_LIT>' ) : <EOL> res += '<STR_LIT::>' + repr ( self . sort ) <EOL> return res <EOL> def clone ( self , args ) : <EOL> return type ( self ) ( self . rep , * args ) <EOL> def __eq__ ( self , other ) : <EOL> return type ( self ) == type ( other ) and self . rep == other . rep and self . args == other . args <EOL> def is_numeral ( self ) : <EOL> return self . rep . rep [ <NUM_LIT:0> ] . isdigit ( ) <EOL> def prefix ( self , s ) : <EOL> res = App ( s + self . rep ) <EOL> if hasattr ( self , '<STR_LIT>' ) : <EOL> res . sort = self . sort <EOL> return res <EOL> Constant = App <EOL> class Variable ( Term ) : <EOL> def __init__ ( self , rep , sort ) : <EOL> assert isinstance ( rep , str ) <EOL> self . rep = rep <EOL> self . args = [ ] <EOL> self . sort = sort <EOL> def __repr__ ( self ) : <EOL> res = self . rep <EOL> res += '<STR_LIT::>' + str ( self . sort ) <EOL> return res <EOL> def clone ( self , args ) : <EOL> return self <EOL> def __eq__ ( self , other ) : <EOL> return type ( self ) == type ( other ) and self . rep == other . rep <EOL> def __hash__ ( self ) : <EOL> return hash ( self . rep ) <EOL> def to_const ( self , prefix ) : <EOL> res = App ( prefix + self . rep ) <EOL> if hasattr ( self , '<STR_LIT>' ) : <EOL> res . sort = self . sort <EOL> return res <EOL> class Literal ( AST ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , polarity , atom ) : <EOL> self . polarity = polarity <EOL> self . atom = atom <EOL> def __repr__ ( self ) : <EOL> return ( '<STR_LIT>' if self . polarity == <NUM_LIT:0> else '<STR_LIT>' ) + repr ( self . atom ) <EOL> def __invert__ ( self ) : <EOL> """<STR_LIT>""" <EOL> return Literal ( <NUM_LIT:1> - self . polarity , self . atom ) <EOL> def clone ( self , args ) : <EOL> return Literal ( self . polarity , * args ) <EOL> def __eq__ ( self , other ) : <EOL> return type ( self ) == type ( other ) and self . polarity == other . polarity and self . args == other . args <EOL> @ property <EOL> def args ( self ) : <EOL> return [ self . atom ] <EOL> @ args . setter <EOL> def args ( self , value ) : <EOL> assert len ( value ) == <NUM_LIT:1> <EOL> self . atom = value [ <NUM_LIT:0> ] <EOL> def _eq_lit ( x , y ) : <EOL> return Literal ( <NUM_LIT:1> , Atom ( equals , ( x , y ) ) ) <EOL> def _neq_lit ( x , y ) : <EOL> return Literal ( <NUM_LIT:0> , Atom ( equals , ( x , y ) ) ) <EOL> class Predicate ( object ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , name , arity ) : <EOL> self . name = name <EOL> self . arity = arity <EOL> def __call__ ( self , * terms ) : <EOL> assert len ( terms ) == self . arity <EOL> return Literal ( <NUM_LIT:1> , Atom ( self . name , terms ) ) <EOL> class Sort ( AST ) : <EOL> pass <EOL> class EnumeratedSort ( Sort ) : <EOL> def __init__ ( self , extension ) : <EOL> self . extension = extension <EOL> self . dom = [ ] <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT:{>' + '<STR_LIT:U+002C>' . join ( self . extension ) + '<STR_LIT:}>' <EOL> def defines ( self ) : <EOL> return self . extension <EOL> def range ( self ) : <EOL> return self <EOL> class ConstantSort ( Sort ) : <EOL> def __init__ ( self , rep , prover_sort = None ) : <EOL> self . rep , self . prover_sort = rep , prover_sort <EOL> self . rng = self <EOL> self . dom = [ ] <EOL> def __repr__ ( self ) : <EOL> return self . rep <EOL> def __str__ ( self ) : <EOL> return self . rep <EOL> def __eq__ ( self , other ) : <EOL> return type ( other ) == type ( self ) and other . rep == self . rep <EOL> def defines ( self ) : <EOL> return [ ] <EOL> def range ( self ) : <EOL> return self <EOL> UninterpretedSort = ConstantSort <EOL> class FunctionSort ( Sort ) : <EOL> def __init__ ( self , dom , rng ) : <EOL> self . dom , self . rng = dom , rng <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT>' . join ( repr ( s ) for s in self . dom ) + '<STR_LIT>' + repr ( self . rng ) <EOL> def defines ( self ) : <EOL> return [ ] <EOL> def range ( self ) : <EOL> return self . rng <EOL> class RelationSort ( Sort ) : <EOL> def __init__ ( self , dom ) : <EOL> self . dom = dom <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT>' . join ( repr ( s ) for s in self . dom ) <EOL> def defines ( self ) : <EOL> return [ ] <EOL> class Tuple ( AST ) : <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT:(>' + '<STR_LIT:U+002C>' . join ( repr ( s ) for s in self . args ) + '<STR_LIT:)>' <EOL> def lineno ( c ) : <EOL> try : <EOL> return c . lineno <EOL> except : <EOL> return None <EOL> class Decl ( AST ) : <EOL> def __init__ ( self , * args ) : <EOL> self . args = args <EOL> def __repr__ ( self ) : <EOL> res = self . name ( ) + '<STR_LIT:U+0020>' + '<STR_LIT:U+002C>' . join ( [ repr ( a ) for a in self . args ] ) <EOL> return res <EOL> def defines ( self ) : <EOL> return [ ] <EOL> class ModuleDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ( c . defines ( ) , lineno ( c ) ) for c in self . args ] <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT>' + '<STR_LIT:U+002C>' . join ( repr ( d . args [ <NUM_LIT:0> ] ) + '<STR_LIT>' + repr ( d . args [ <NUM_LIT:1> ] ) + '<STR_LIT>' for d in self . args ) <EOL> class MacroDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ( c . defines ( ) , lineno ( c ) ) for c in self . args ] <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT>' + '<STR_LIT:U+002C>' . join ( repr ( d . args [ <NUM_LIT:0> ] ) + '<STR_LIT>' + repr ( d . args [ <NUM_LIT:1> ] ) + '<STR_LIT>' for d in self . args ) <EOL> class LabeledFormula ( AST ) : <EOL> @ property <EOL> def label ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] <EOL> @ property <EOL> def formula ( self ) : <EOL> return self . args [ <NUM_LIT:1> ] <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT:[>' + str ( self . label ) + '<STR_LIT>' + str ( self . formula ) if self . label else str ( self . formula ) <EOL> class AxiomDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> class ConjectureDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> class SchemaDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ( c . defines ( ) , lineno ( c ) ) for c in self . args ] <EOL> class Instantiation ( AST ) : <EOL> def __init__ ( self , * args ) : <EOL> self . args = args <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT>' . join ( repr ( x ) for x in self . args ) if self . args [ <NUM_LIT:0> ] else repr ( self . args [ <NUM_LIT:1> ] ) <EOL> class InstantiateDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> class RelationDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ( c . relname , lineno ( c ) ) for c in self . args if c . relname not in iu . polymorphic_symbols ] <EOL> class ConstantDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ( c . rep , lineno ( c ) ) for c in self . args if c . rep not in iu . polymorphic_symbols ] <EOL> class DerivedDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ( c . defines ( ) , lineno ( c ) ) for c in self . args ] <EOL> class ProgressDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ( c . defines ( ) , lineno ( c ) ) for c in self . args ] <EOL> class RelyDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ] <EOL> class MixOrdDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ] <EOL> class ConceptDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ( c . defines ( ) , lineno ( c ) ) for c in self . args ] <EOL> class ActionDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT:action>' <EOL> def defines ( self ) : <EOL> return [ ( c . defines ( ) , lineno ( c ) ) for c in self . args ] <EOL> class StateDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT:state>' <EOL> class InitDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> class UpdateDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> class TypeDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT:type>' <EOL> def defines ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . defines ( ) <EOL> class AssertDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ] <EOL> class InterpretDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ] <EOL> class MixinDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ] <EOL> class MixinDef ( AST ) : <EOL> def mixer ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . relname <EOL> def mixee ( self ) : <EOL> return self . args [ <NUM_LIT:1> ] . relname <EOL> class MixinBeforeDef ( MixinDef ) : <EOL> pass <EOL> class MixinAfterDef ( MixinDef ) : <EOL> pass <EOL> class IsolateDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ( c . name ( ) , lineno ( c ) ) for c in self . args ] <EOL> class IsolateDef ( AST ) : <EOL> def name ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . relname <EOL> def verified ( self ) : <EOL> return self . args [ <NUM_LIT:1> : len ( self . args ) - self . with_args ] <EOL> def present ( self ) : <EOL> return self . args [ len ( self . args ) - self . with_args : ] <EOL> def __repr__ ( self ) : <EOL> return ( '<STR_LIT:U+002C>' . join ( repr ( a ) for a in self . verified ( ) ) + <EOL> ( ( '<STR_LIT>' + '<STR_LIT:U+002C>' . join ( repr ( a ) for a in self . present ( ) ) ) if self . present ( ) else '<STR_LIT>' ) ) <EOL> class ExportDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ] <EOL> class ExportDef ( AST ) : <EOL> def exported ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . relname <EOL> def scope ( self ) : <EOL> return self . args [ <NUM_LIT:1> ] . relname <EOL> def __repr__ ( self ) : <EOL> return self . exported ( ) + ( '<STR_LIT>' . format ( self . scope ( ) ) if self . scope ( ) else '<STR_LIT>' ) <EOL> class DelegateDecl ( Decl ) : <EOL> def name ( self ) : <EOL> return '<STR_LIT>' <EOL> def defines ( self ) : <EOL> return [ ] <EOL> class DelegateDef ( AST ) : <EOL> def delegated ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . relname <EOL> def delegee ( self ) : <EOL> if len ( self . args ) > <NUM_LIT:1> : <EOL> return self . args [ <NUM_LIT:1> ] . relname <EOL> return None <EOL> def __repr__ ( self ) : <EOL> s = self . delegated ( ) <EOL> if len ( self . args ) > <NUM_LIT:1> : <EOL> s += '<STR_LIT>' + self . delegee <EOL> return s <EOL> class TypeDef ( Definition ) : <EOL> def __init__ ( self , name , sort ) : <EOL> self . args = [ name , sort ] <EOL> def __repr__ ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] + '<STR_LIT>' + repr ( self . args [ <NUM_LIT:1> ] ) <EOL> def defines ( self ) : <EOL> syms = [ self . args [ <NUM_LIT:0> ] ] + self . args [ <NUM_LIT:1> ] . defines ( ) <EOL> return [ ( sym , lineno ( self ) ) for sym in syms ] <EOL> class ActionDef ( Definition ) : <EOL> def __init__ ( self , atom , action , formals = [ ] , returns = [ ] ) : <EOL> self . formal_params = [ s . prefix ( '<STR_LIT>' ) for s in formals ] <EOL> self . formal_returns = [ s . prefix ( '<STR_LIT>' ) for s in returns ] <EOL> if formals or returns : <EOL> subst = dict ( ( x . rep , y . rep ) for x , y in zip ( formals + returns , self . formal_params + self . formal_returns ) ) <EOL> action = subst_prefix_atoms_ast ( action , subst , None , None ) <EOL> self . args = [ atom , action ] <EOL> def __repr__ ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . relname + '<STR_LIT>' + str ( self . args [ <NUM_LIT:1> ] ) <EOL> def defines ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . relname <EOL> def clone ( self , args ) : <EOL> res = ActionDef ( args [ <NUM_LIT:0> ] , args [ <NUM_LIT:1> ] ) <EOL> res . formal_params = self . formal_params <EOL> res . formal_returns = self . formal_returns <EOL> return res <EOL> def rewrite ( self , rewrite ) : <EOL> res = self . clone ( ast_rewrite ( self . args , rewrite ) ) <EOL> if hasattr ( self , '<STR_LIT>' ) : <EOL> res . formal_params = [ rewrite_param ( p , rewrite ) for p in self . formal_params ] <EOL> if hasattr ( self , '<STR_LIT>' ) : <EOL> res . formal_returns = [ rewrite_param ( p , rewrite ) for p in self . formal_returns ] <EOL> return res <EOL> def rewrite_param ( p , rewrite ) : <EOL> res = App ( p . rep ) <EOL> res . sort = ast_rewrite ( p . sort , rewrite ) <EOL> return res <EOL> class StateDef ( Definition ) : <EOL> def __init__ ( self , name , state ) : <EOL> self . args = [ Atom ( name , [ ] ) , state ] <EOL> def __repr__ ( self ) : <EOL> return self . args [ <NUM_LIT:0> ] . relname + '<STR_LIT>' + repr ( self . args [ <NUM_LIT:1> ] ) <EOL> universe = '<STR_LIT:S>' <EOL> equals = Symbol ( '<STR_LIT:=>' , RelationSort ( [ None , None ] ) ) <EOL> def Equals ( x , y ) : <EOL> return Atom ( equals , x , y ) <EOL> def is_equals ( symbol ) : <EOL> return isinstance ( symbol , Symbol ) and symbol . rep == '<STR_LIT:=>' <EOL> def is_enumerated ( term ) : <EOL> return isinstance ( term . get_sort ( ) , EnumeratedSort ) <EOL> def app_to_atom ( app ) : <EOL> if isinstance ( app , Old ) or isinstance ( app , Quantifier ) : <EOL> return app <EOL> res = Atom ( app . rep , app . args ) <EOL> if hasattr ( app , '<STR_LIT>' ) : <EOL> res . lineno = app . lineno <EOL> return res <EOL> def apps_to_atoms ( apps ) : <EOL> return [ app_to_atom ( app ) for app in apps ] <EOL> name_parser = re . compile ( r'<STR_LIT>' ) <EOL> def str_subst ( s , subst ) : <EOL> names = split_name ( s ) <EOL> return compose_names ( subst . get ( names [ <NUM_LIT:0> ] , names [ <NUM_LIT:0> ] ) , * names [ <NUM_LIT:1> : ] ) <EOL> def subst_subscripts_comp ( s , subst ) : <EOL> assert s != None <EOL> g = name_parser . findall ( s ) <EOL> if not g : <EOL> return s <EOL> res = str_subst ( g [ <NUM_LIT:0> ] , subst ) + '<STR_LIT>' . join ( ( '<STR_LIT:[>' + str_subst ( x [ <NUM_LIT:1> : - <NUM_LIT:1> ] , subst ) + '<STR_LIT:]>' if x . startswith ( '<STR_LIT:[>' ) else x ) for x in g [ <NUM_LIT:1> : ] ) <EOL> return res <EOL> def subst_subscripts ( s , subst ) : <EOL> return subst_subscripts_comp ( s , subst ) <EOL> class AstRewriteSubstConstants ( object ) : <EOL> def __init__ ( self , subst ) : <EOL> self . subst = subst <EOL> def rewrite_name ( self , name ) : <EOL> return name <EOL> def rewrite_atom ( self , atom ) : <EOL> subst = self . subst <EOL> return subst [ atom . rep ] if not atom . args and atom . rep in subst else atom <EOL> class AstRewriteSubstConstantsParams ( object ) : <EOL> def __init__ ( self , subst , psubst ) : <EOL> self . subst = subst <EOL> self . psubst = psubst <EOL> def rewrite_name ( self , name ) : <EOL> return subst_subscripts ( name , self . psubst ) <EOL> def rewrite_atom ( self , atom ) : <EOL> subst = self . subst <EOL> return subst [ atom . rep ] if not atom . args and atom . rep in subst else atom <EOL> class AstRewriteSubstPrefix ( object ) : <EOL> def __init__ ( self , subst , pref , to_pref = None ) : <EOL> self . subst , self . pref , self . to_pref = subst , pref , to_pref <EOL> def rewrite_name ( self , name ) : <EOL> return subst_subscripts ( name , self . subst ) <EOL> def rewrite_atom ( self , atom ) : <EOL> return compose_atoms ( self . pref , atom ) if self . pref and ( self . to_pref == None or atom . rep in self . to_pref ) else atom <EOL> class AstRewritePostfix ( object ) : <EOL> def __init__ ( self , post ) : <EOL> self . post = post <EOL> def rewrite_name ( self , name ) : <EOL> return name <EOL> def rewrite_atom ( self , atom ) : <EOL> return compose_atoms ( atom , self . post ) <EOL> class AstRewriteAddParams ( object ) : <EOL> def __init__ ( self , params ) : <EOL> self . params = params <EOL> def rewrite_name ( self , name ) : <EOL> return name <EOL> def rewrite_atom ( self , atom ) : <EOL> return atom . clone ( atom . args + self . params ) <EOL> def ast_rewrite ( x , rewrite ) : <EOL> if isinstance ( x , str ) : <EOL> return rewrite . rewrite_name ( x ) <EOL> if isinstance ( x , list ) : <EOL> return [ ast_rewrite ( e , rewrite ) for e in x ] <EOL> if isinstance ( x , tuple ) : <EOL> return tuple ( ast_rewrite ( e , rewrite ) for e in x ) <EOL> if isinstance ( x , Variable ) : <EOL> return Variable ( x . rep , rewrite . rewrite_name ( x . sort ) ) <EOL> if isinstance ( x , Atom ) or isinstance ( x , App ) : <EOL> atom = type ( x ) ( rewrite . rewrite_name ( x . rep ) , ast_rewrite ( x . args , rewrite ) ) <EOL> copy_attributes_ast ( x , atom ) <EOL> if hasattr ( x , '<STR_LIT>' ) : <EOL> atom . sort = rewrite . rewrite_name ( x . sort ) <EOL> return rewrite . rewrite_atom ( atom ) <EOL> if isinstance ( x , Literal ) : <EOL> return Literal ( x . polarity , ast_rewrite ( x . atom , rewrite ) ) <EOL> if isinstance ( x , Quantifier ) : <EOL> return type ( x ) ( ast_rewrite ( x . bounds , rewrite ) , ast_rewrite ( x . args [ <NUM_LIT:0> ] , rewrite ) ) <EOL> if hasattr ( x , '<STR_LIT>' ) : <EOL> return x . rewrite ( rewrite ) <EOL> if isinstance ( x , LabeledFormula ) : <EOL> arg0 = x . args [ <NUM_LIT:0> ] <EOL> if x . args [ <NUM_LIT:0> ] == None : <EOL> if isinstance ( rewrite , AstRewriteSubstPrefix ) and rewrite . pref != None : <EOL> arg0 = Atom ( rewrite . pref , [ ] ) <EOL> else : <EOL> arg0 = rewrite . rewrite_atom ( x . args [ <NUM_LIT:0> ] ) <EOL> res = x . clone ( [ arg0 , ast_rewrite ( x . args [ <NUM_LIT:1> ] , rewrite ) ] ) <EOL> return res <EOL> if hasattr ( x , '<STR_LIT:args>' ) : <EOL> return x . clone ( ast_rewrite ( x . args , rewrite ) ) <EOL> print "<STR_LIT>" . format ( x , type ( x ) ) <EOL> assert False <EOL> def subst_prefix_atoms_ast ( ast , subst , pref , to_pref ) : <EOL> po = variables_distinct_ast ( pref , ast ) if pref else pref <EOL> return ast_rewrite ( ast , AstRewriteSubstPrefix ( subst , po , to_pref ) ) <EOL> def postfix_atoms_ast ( ast , post ) : <EOL> po = variables_distinct_ast ( post , ast ) <EOL> return ast_rewrite ( ast , AstRewritePostfix ( po ) ) <EOL> def add_parameters_ast ( ast , params ) : <EOL> return ast_rewrite ( ast , AstRewriteAddParams ( params ) ) <EOL> def copy_attributes_ast ( x , y ) : <EOL> if hasattr ( x , '<STR_LIT>' ) : <EOL> y . lineno = x . lineno <EOL> if hasattr ( x , '<STR_LIT>' ) : <EOL> y . sort = x . sort <EOL> def substitute_ast ( ast , subs ) : <EOL> """<STR_LIT>""" <EOL> if isinstance ( ast , Variable ) : <EOL> return subs . get ( ast . rep , ast ) <EOL> else : <EOL> res = ast . clone ( [ substitute_ast ( x , subs ) for x in ast . args ] ) <EOL> copy_attributes_ast ( ast , res ) <EOL> return res <EOL> def variables_distinct_ast ( ast1 , ast2 ) : <EOL> """<STR_LIT>""" <EOL> map1 = distinct_variable_renaming ( used_variables_ast ( ast1 ) , used_variables_ast ( ast2 ) ) <EOL> return substitute_ast ( ast1 , map1 ) <EOL> def distinct_variable_renaming ( vars1 , vars2 ) : <EOL> rn = UniqueRenamer ( '<STR_LIT>' , ( v . rep for v in vars2 ) ) <EOL> return dict ( ( v . rep , rename_variable ( v , rn ( v . rep ) ) ) for v in vars1 ) <EOL> def rename_variable ( v , name ) : <EOL> return type ( v ) ( name , v . sort ) <EOL> def variables_ast ( ast ) : <EOL> if isinstance ( ast , Variable ) : <EOL> yield ast <EOL> elif ast != None and not isinstance ( ast , str ) : <EOL> for arg in ast . args : <EOL> for x in variables_ast ( arg ) : <EOL> yield x <EOL> used_variables_ast = gen_to_set ( variables_ast ) <EOL> def compose_atoms ( pr , atom ) : <EOL> if atom == None : <EOL> return pr <EOL> hname = compose_names ( pr . rep , atom . rep ) <EOL> args = pr . args + atom . args <EOL> res = type ( atom ) ( hname , args ) <EOL> copy_attributes_ast ( atom , res ) <EOL> return res <EOL> def is_true ( ast ) : <EOL> return isinstance ( ast , And ) and len ( ast . args ) == <NUM_LIT:0> <EOL> def is_false ( ast ) : <EOL> return isinstance ( ast , Or ) and len ( ast . args ) == <NUM_LIT:0> <EOL> class Range ( AST ) : <EOL> def __init__ ( self , lo , hi ) : <EOL> self . args = [ ] <EOL> self . lo , self . hi = lo , hi <EOL> def __str__ ( self ) : <EOL> return '<STR_LIT:{>' + str ( self . lo ) + '<STR_LIT:..>' + str ( self . hi ) + '<STR_LIT:}>' <EOL> @ property <EOL> def rep ( self ) : <EOL> return self <EOL> @ property <EOL> def card ( self ) : <EOL> return int ( self . hi ) - int ( self . lo ) + <NUM_LIT:1> <EOL> class ASTContext ( object ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , ast ) : <EOL> self . ast = ast <EOL> def __enter__ ( self ) : <EOL> return self <EOL> def __exit__ ( self , exc_type , exc_val , exc_tb ) : <EOL> if isinstance ( exc_val , ivy_logic . Error ) : <EOL> raise IvyError ( self . ast , str ( exc_val ) ) <EOL> if exc_type == IvyError and exc_val . lineno == None and hasattr ( self . ast , '<STR_LIT>' ) : <EOL> if isinstance ( self . ast . lineno , tuple ) : <EOL> exc_val . filename , exc_val . lineno = self . ast . lineno <EOL> else : <EOL> exc_val . lineno = self . ast . lineno <EOL> return False </s>
