<s> """<STR_LIT>""" <EOL> from ivy_utils import UniqueRenamer , union_to_list , list_union , list_diff , IvyError , inverse_map , compose_maps , pretty <EOL> from ivy_logic import Variable , Constant , Literal , Atom , Not , And , Or , App , RelationSort , Definition , is_prenex_universal <EOL> from ivy_logic_utils import used_symbols_clauses , rename_clauses , clauses_using_symbols , simplify_clauses , used_variables_clauses , used_constants_clauses , substitute_constants_clause , substitute_constants_clauses , constants_clauses , relations_clauses , eq_lit , condition_clauses , or_clauses , and_clauses , false_clauses , true_clauses , formula_to_clauses , clauses_to_formula , formula_to_clauses_tseitin , is_ground_clause , relations_clause , Clauses , sym_inst , negate_clauses , negate <EOL> from ivy_solver import unsat_core , clauses_imply , clauses_imply_formula , clauses_sat , clauses_case , get_model_clauses , clauses_model_to_clauses , get_small_model <EOL> import ivy_logic <EOL> import ivy_logic_utils as lu <EOL> import ivy_utils as iu <EOL> from logic_util import is_tautology_equality <EOL> def new ( sym ) : <EOL> """<STR_LIT>""" <EOL> return sym . prefix ( '<STR_LIT>' ) <EOL> def is_new ( sym ) : <EOL> return sym . startswith ( '<STR_LIT>' ) <EOL> def new_of ( sym ) : <EOL> return sym . drop_prefix ( '<STR_LIT>' ) <EOL> def old ( sym ) : <EOL> """<STR_LIT>""" <EOL> return sym . prefix ( '<STR_LIT>' ) <EOL> def is_old ( sym ) : <EOL> return sym . startswith ( '<STR_LIT>' ) <EOL> def old_of ( sym ) : <EOL> return sym . drop_prefix ( '<STR_LIT>' ) <EOL> def rename ( sym , rn ) : <EOL> return sym . rename ( rn ) <EOL> def is_skolem ( sym ) : <EOL> """<STR_LIT>""" <EOL> return sym . contains ( '<STR_LIT>' ) <EOL> def null_update ( ) : <EOL> return ( [ ] , true_clauses ( ) , false_clauses ( ) ) <EOL> def pure_state ( clauses ) : <EOL> return ( None , clauses , false_clauses ( ) ) <EOL> def is_pure_state ( state ) : <EOL> return state [ <NUM_LIT:0> ] == None <EOL> def top_state ( ) : <EOL> return pure_state ( true_clauses ( ) ) <EOL> def bottom_state ( ) : <EOL> return pure_state ( false_clauses ( ) ) <EOL> def state_postcond ( state ) : <EOL> return state [ <NUM_LIT:1> ] <EOL> def state_precond ( state ) : <EOL> return state [ <NUM_LIT:2> ] <EOL> def state_to_action ( update ) : <EOL> """<STR_LIT>""" <EOL> updated , postcond , pre = update <EOL> postcond , pre = clausify ( postcond ) , clausify ( pre ) <EOL> renaming = dict ( ) <EOL> for s in updated : <EOL> renaming [ s ] = new ( s ) <EOL> for s in used_symbols_clauses ( postcond ) : <EOL> if is_old ( s ) : <EOL> renaming [ s ] = old_of ( s ) <EOL> return ( updated , rename_clauses ( postcond , renaming ) , pre ) <EOL> def action_to_state ( update ) : <EOL> """<STR_LIT>""" <EOL> updated , tr , pre = update <EOL> renaming = dict ( ) <EOL> for s in updated : <EOL> renaming [ s ] = old ( s ) <EOL> for s in used_symbols_clauses ( tr ) : <EOL> if is_new ( s ) : <EOL> renaming [ s ] = new_of ( s ) <EOL> return ( updated , rename_clauses ( tr , renaming ) , pre ) <EOL> def update_frame_constraint ( update , relations ) : <EOL> """<STR_LIT>""" <EOL> clauses = [ ] <EOL> for sym in update [ <NUM_LIT:0> ] : <EOL> if sym in relations : <EOL> arity = relations [ sym ] <EOL> vs = [ Variable ( "<STR_LIT>" . format ( i ) ) for i in range ( <NUM_LIT:0> , arity ) ] <EOL> lit1 = Literal ( <NUM_LIT:1> , Atom ( sym , vs ) ) <EOL> lit2 = Literal ( <NUM_LIT:1> , Atom ( new ( sym ) , vs ) ) <EOL> clauses += [ [ ~ lit1 , lit2 ] , [ lit1 , ~ lit2 ] ] <EOL> else : <EOL> clauses . append ( [ eq_lit ( Constant ( sym ) , Constant ( new ( sym ) ) ) ] ) <EOL> return Clauses ( clauses ) <EOL> def frame_def ( sym , op ) : <EOL> """<STR_LIT>""" <EOL> lhs = sym_inst ( op ( sym ) if op is new else sym ) <EOL> rhs = sym_inst ( sym if op is new else op ( sym ) ) <EOL> dfn = Definition ( lhs , rhs ) <EOL> return dfn <EOL> def frame ( updated , relations , op ) : <EOL> """<STR_LIT>""" <EOL> return Clauses ( [ ] , [ frame_def ( sym , op ) for sym in updated ] ) <EOL> def symbol_frame_cond ( sym , sig ) : <EOL> """<STR_LIT>""" <EOL> return Clauses ( [ ] , [ frame_def ( sym , new ) ] ) <EOL> def frame_update ( update , in_scope , sig ) : <EOL> """<STR_LIT>""" <EOL> updated , clauses , pre = update <EOL> moded = set ( updated ) <EOL> dfns = [ ] <EOL> for sym in in_scope : <EOL> if sym not in moded : <EOL> updated . append ( sym ) <EOL> dfns . append ( frame_def ( sym , new ) ) <EOL> return ( updated , and_clauses ( clauses , Clauses ( [ ] , dfns ) ) , pre ) <EOL> def diff_frame ( updated1 , updated2 , relations , op ) : <EOL> if updated1 == None or updated2 == None : return Clauses ( [ ] ) <EOL> updated = list_diff ( updated2 , updated1 ) <EOL> return frame ( updated , relations , op ) <EOL> def updated_join ( updated1 , updated2 ) : <EOL> if updated1 == None or updated1 == None : return None <EOL> return list_union ( updated1 , updated2 ) <EOL> def join ( s1 , s2 , relations , op ) : <EOL> u1 , c1 , p1 = s1 <EOL> u2 , c2 , p2 = s2 <EOL> df12 = diff_frame ( u1 , u2 , relations , op ) <EOL> df21 = diff_frame ( u2 , u1 , relations , op ) <EOL> c1 = and_clauses ( c1 , df12 ) <EOL> c2 = and_clauses ( c2 , df21 ) <EOL> p1 = and_clauses ( p1 , df12 ) <EOL> p2 = and_clauses ( p2 , df21 ) <EOL> u = updated_join ( u1 , u2 ) <EOL> c = or_clauses ( c1 , c2 ) <EOL> p = or_clauses ( p1 , p2 ) <EOL> return ( u , c , p ) <EOL> class CounterExample ( object ) : <EOL> def __init__ ( self , clauses ) : <EOL> self . clauses = clauses <EOL> def __nonzero__ ( self ) : <EOL> return False <EOL> def clauses_imply_formula_cex ( clauses , fmla ) : <EOL> if clauses_imply_formula ( clauses , fmla ) : <EOL> return True <EOL> return CounterExample ( conjoin ( clauses , negate_clauses ( formula_to_clauses ( fmla ) ) ) ) <EOL> def implies ( s1 , s2 , axioms , relations , op ) : <EOL> u1 , c1 , p1 = s1 <EOL> u2 , c2 , p2 = s2 <EOL> if u1 == None and u2 != None : <EOL> return False <EOL> c1 = and_clauses ( c1 , axioms , diff_frame ( u1 , u2 , relations , op ) ) <EOL> if isinstance ( c2 , Clauses ) : <EOL> if not c2 . is_universal_first_order ( ) or not p2 . is_universal_first_order ( ) : <EOL> return False <EOL> c2 = and_clauses ( c2 , diff_frame ( u2 , u1 , relations , op ) ) <EOL> return clauses_imply ( p1 , p2 ) and clauses_imply ( c1 , c2 ) <EOL> else : <EOL> if not is_prenex_universal ( c2 ) or not is_prenex_universal ( p2 ) : <EOL> return False <EOL> c2 = And ( c2 , clauses_to_formula ( diff_frame ( u2 , u1 , relations , op ) ) ) <EOL> return clauses_imply_formula_cex ( p1 , p2 ) and clauses_imply_formula_cex ( c1 , c2 ) <EOL> def implies_state ( s1 , s2 , axioms , relations ) : <EOL> return implies ( s1 , s2 , axioms , relations , old ) <EOL> def implies_action ( s1 , s2 , axioms , relations ) : <EOL> return implies ( s1 , s2 , axioms , relations , new ) <EOL> def join_state ( s1 , s2 , relations ) : <EOL> return join ( clausify_state ( s1 ) , clausify_state ( s2 ) , relations , old ) <EOL> def join_action ( s1 , s2 , relations ) : <EOL> return join ( s1 , s2 , relations , new ) <EOL> def condition_update_on_fmla ( update , fmla , relations ) : <EOL> """<STR_LIT>""" <EOL> updated , if_clauses , if_pre = update <EOL> else_clauses = update_frame_constraint ( update , relations ) <EOL> if_clauses = condition_clauses ( if_clauses , fmla ) <EOL> else_clauses = condition_clauses ( else_clauses , Not ( fmla ) ) <EOL> return updated , ( and_clauses ( if_clauses , else_clauses ) ) , if_pre <EOL> def rename_distinct ( clauses1 , clauses2 ) : <EOL> """<STR_LIT>""" <EOL> used1 = used_symbols_clauses ( clauses1 ) <EOL> used2 = used_symbols_clauses ( clauses2 ) <EOL> rn = UniqueRenamer ( '<STR_LIT>' , used2 ) <EOL> map1 = dict ( ) <EOL> for s in used1 : <EOL> if is_skolem ( s ) : <EOL> map1 [ s ] = rename ( s , rn ) <EOL> return rename_clauses ( clauses1 , map1 ) <EOL> def compose_updates ( update1 , axioms , update2 ) : <EOL> updated1 , clauses1 , pre1 = update1 <EOL> updated2 , clauses2 , pre2 = update2 <EOL> clauses2 = rename_distinct ( clauses2 , clauses1 ) <EOL> pre2 = rename_distinct ( pre2 , clauses1 ) <EOL> us1 = set ( updated1 ) <EOL> us2 = set ( updated2 ) <EOL> mid = us1 . intersection ( us2 ) <EOL> mid_ax = clauses_using_symbols ( mid , axioms ) <EOL> used = used_symbols_clauses ( and_clauses ( clauses1 , clauses2 ) ) <EOL> rn = UniqueRenamer ( '<STR_LIT>' , used ) <EOL> map1 = dict ( ) <EOL> map2 = dict ( ) <EOL> for v in updated1 : <EOL> map2 [ v ] = new ( v ) <EOL> for mv in mid : <EOL> mvf = rename ( mv , rn ) <EOL> map1 [ new ( mv ) ] = mvf <EOL> map2 [ mv ] = mvf <EOL> clauses1 = rename_clauses ( clauses1 , map1 ) <EOL> new_clauses = and_clauses ( clauses1 , rename_clauses ( and_clauses ( clauses2 , mid_ax ) , map2 ) ) <EOL> new_updated = list ( us1 . union ( us2 ) ) <EOL> pre1 = and_clauses ( pre1 , diff_frame ( updated1 , updated2 , None , new ) ) <EOL> new_pre = or_clauses ( pre1 , and_clauses ( clauses1 , rename_clauses ( and_clauses ( pre2 , mid_ax ) , map2 ) ) ) <EOL> return ( new_updated , new_clauses , new_pre ) <EOL> def exist_quant_map ( syms , clauses ) : <EOL> used = used_symbols_clauses ( clauses ) <EOL> rn = UniqueRenamer ( '<STR_LIT>' , used ) <EOL> map1 = dict ( ) <EOL> for s in syms : <EOL> map1 [ s ] = rename ( s , rn ) <EOL> return map1 , rename_clauses ( clauses , map1 ) <EOL> def exist_quant ( syms , clauses ) : <EOL> map1 , res = exist_quant_map ( syms , clauses ) <EOL> return res <EOL> def conjoin ( clauses1 , clauses2 ) : <EOL> """<STR_LIT>""" <EOL> return and_clauses ( clauses1 , rename_distinct ( clauses2 , clauses1 ) ) <EOL> def constrain_state ( upd , fmla ) : <EOL> return ( upd [ <NUM_LIT:0> ] , and_clauses ( upd [ <NUM_LIT:1> ] , formula_to_clauses ( fmla ) ) , upd [ <NUM_LIT:2> ] ) <EOL> def hide ( syms , update ) : <EOL> syms = set ( syms ) <EOL> syms . update ( new ( s ) for s in update [ <NUM_LIT:0> ] if s in syms ) <EOL> new_updated = [ s for s in update [ <NUM_LIT:0> ] if s not in syms ] <EOL> new_tr = exist_quant ( syms , update [ <NUM_LIT:1> ] ) <EOL> new_pre = exist_quant ( syms , update [ <NUM_LIT:2> ] ) <EOL> return ( new_updated , new_tr , new_pre ) <EOL> def hide_state ( syms , update ) : <EOL> syms = set ( syms ) <EOL> if update [ <NUM_LIT:0> ] != None : <EOL> syms . update ( old ( s ) for s in update [ <NUM_LIT:0> ] if s in syms ) <EOL> new_updated = [ s for s in update [ <NUM_LIT:0> ] if s not in syms ] <EOL> else : <EOL> new_updated = None <EOL> new_tr = exist_quant ( syms , update [ <NUM_LIT:1> ] ) <EOL> new_pre = exist_quant ( syms , update [ <NUM_LIT:2> ] ) <EOL> return ( new_updated , new_tr , new_pre ) <EOL> def hide_state_map ( syms , update ) : <EOL> syms = set ( syms ) <EOL> if update [ <NUM_LIT:0> ] != None : <EOL> syms . update ( old ( s ) for s in update [ <NUM_LIT:0> ] if s in syms ) <EOL> new_updated = [ s for s in update [ <NUM_LIT:0> ] if s not in syms ] <EOL> else : <EOL> new_updated = None <EOL> trmap , new_tr = exist_quant_map ( syms , update [ <NUM_LIT:1> ] ) <EOL> new_pre = exist_quant ( syms , update [ <NUM_LIT:2> ] ) <EOL> return trmap , ( new_updated , new_tr , new_pre ) <EOL> def subst_action ( update , subst ) : <EOL> print subst <EOL> syms = dict ( subst . iteritems ( ) ) <EOL> syms . update ( ( new ( s ) , new ( syms [ s ] ) ) for s in update [ <NUM_LIT:0> ] if s in syms ) <EOL> print syms <EOL> new_updated = [ subst . get ( s , s ) for s in update [ <NUM_LIT:0> ] ] <EOL> new_tr = rename_clauses ( update [ <NUM_LIT:1> ] , syms ) <EOL> new_pre = rename_clauses ( update [ <NUM_LIT:2> ] , syms ) <EOL> return ( new_updated , new_tr , new_pre ) <EOL> def forward_image_map ( pre_state , axioms , update ) : <EOL> updated , clauses , _precond = update <EOL> pre_ax = clauses_using_symbols ( updated , axioms ) <EOL> pre = conjoin ( pre_state , pre_ax ) <EOL> map1 , res = exist_quant_map ( updated , conjoin ( pre , clauses ) ) <EOL> res = rename_clauses ( res , dict ( ( new ( x ) , x ) for x in updated ) ) <EOL> return map1 , res <EOL> def forward_image ( pre_state , axioms , update ) : <EOL> map1 , res = forward_image_map ( pre_state , axioms , update ) <EOL> return res <EOL> def action_failure ( action ) : <EOL> upd , tr , pre = action <EOL> return upd , pre , true_clauses ( ) <EOL> class ActionFailed ( Exception ) : <EOL> def __init__ ( self , clauses , trans ) : <EOL> self . clauses = clauses <EOL> self . trans = trans <EOL> def clausify ( f ) : <EOL> return f if isinstance ( f , Clauses ) else formula_to_clauses ( f ) <EOL> def clausify_state ( s ) : <EOL> upd , tr , pre = s <EOL> return ( upd , clausify ( tr ) , clausify ( pre ) ) <EOL> def remove_taut_eqs_clauses ( clauses ) : <EOL> return Clauses ( <EOL> [ f for f in clauses . fmlas if not is_tautology_equality ( f ) ] , <EOL> clauses . defs <EOL> ) <EOL> def extract_pre_post_model ( clauses , model , updated ) : <EOL> renaming = dict ( ( v , new ( v ) ) for v in updated ) <EOL> ignore = lambda s : s . is_skolem ( ) or is_new ( s ) <EOL> pre_clauses = clauses_model_to_clauses ( clauses , ignore = ignore , model = model , numerals = use_numerals ( ) ) <EOL> ignore = lambda s : s . is_skolem ( ) or ( not is_new ( s ) and s in renaming ) <EOL> post_clauses = clauses_model_to_clauses ( clauses , ignore = ignore , model = model , numerals = use_numerals ( ) ) <EOL> post_clauses = rename_clauses ( post_clauses , inverse_map ( renaming ) ) <EOL> return map ( remove_taut_eqs_clauses , ( pre_clauses , post_clauses ) ) <EOL> def compose_state_action ( state , axioms , action , check = True ) : <EOL> """<STR_LIT>""" <EOL> su , sc , sp = state <EOL> au , ac , ap = action <EOL> sc , sp = clausify ( sc ) , clausify ( sp ) <EOL> if check : <EOL> pre_test = and_clauses ( and_clauses ( sc , ap ) , axioms ) <EOL> model = small_model_clauses ( pre_test ) <EOL> if model != None : <EOL> trans = extract_pre_post_model ( pre_test , model , au ) <EOL> post_updated = [ new ( s ) for s in au ] <EOL> pre_test = exist_quant ( post_updated , pre_test ) <EOL> raise ActionFailed ( pre_test , trans ) <EOL> if su != None : <EOL> ssu = set ( su ) <EOL> rn = dict ( ( x , old ( x ) ) for x in au if x not in ssu ) <EOL> sc = rename_clauses ( sc , rn ) <EOL> ac = rename_clauses ( ac , rn ) <EOL> su = list ( su ) <EOL> union_to_list ( su , au ) <EOL> img = forward_image ( sc , axioms , action ) <EOL> return ( su , img , sp ) <EOL> def reverse_image ( post_state , axioms , update ) : <EOL> updated , clauses , _precond = update <EOL> post_ax = clauses_using_symbols ( updated , axioms ) <EOL> post_clauses = conjoin ( post_state , post_ax ) <EOL> post_clauses = rename_clauses ( post_clauses , dict ( ( x , new ( x ) ) for x in updated ) ) <EOL> post_updated = [ new ( s ) for s in updated ] <EOL> res = exist_quant ( post_updated , conjoin ( clauses , post_clauses ) ) <EOL> return res <EOL> def interpolant ( clauses1 , clauses2 , axioms , interpreted ) : <EOL> foo = and_clauses ( clauses1 , axioms ) <EOL> clauses2 = simplify_clauses ( clauses2 ) <EOL> core = unsat_core ( clauses2 , foo ) <EOL> if core == None : <EOL> return None <EOL> return core , interp_from_unsat_core ( clauses2 , foo , core , interpreted ) <EOL> def forward_interpolant ( pre_state , update , post_state , axioms , interpreted ) : <EOL> return interpolant ( forward_image ( pre_state , axioms , update ) , post_state , axioms , interpreted ) <EOL> def reverse_interpolant_case ( post_state , update , pre_state , axioms , interpreted ) : <EOL> pre = reverse_image ( post_state , axioms , update ) <EOL> pre_case = clauses_case ( pre ) <EOL> pre_case = [ cl for cl in pre_case if len ( cl ) <= <NUM_LIT:1> <EOL> and is_ground_clause ( cl ) <EOL> and not any ( is_skolem ( r ) for r , n in relations_clause ( cl ) ) ] <EOL> return interpolant ( pre_state , pre_case , axioms , interpreted ) <EOL> def interpolant_case ( pre_state , post , axioms , interpreted ) : <EOL> post_case = clauses_case ( post ) <EOL> post_case = Clauses ( [ cl for cl in post_case . clauses <EOL> if len ( cl ) <= <NUM_LIT:1> <EOL> and is_ground_clause ( cl ) <EOL> and not any ( is_skolem ( r ) for r , n in relations_clause ( cl ) ) ] ) <EOL> return interpolant ( pre_state , post_case , axioms , interpreted ) <EOL> def interp_from_unsat_core ( clauses1 , clauses2 , core , interpreted ) : <EOL> used_syms = used_symbols_clauses ( core ) <EOL> vars = used_variables_clauses ( core ) <EOL> if vars : <EOL> return None <EOL> core_consts = used_constants_clauses ( core ) <EOL> clauses2_consts = used_constants_clauses ( clauses2 ) <EOL> renaming = dict ( ) <EOL> i = <NUM_LIT:0> <EOL> for v in core_consts : <EOL> if v not in clauses2_consts or v . is_skolem ( ) : <EOL> renaming [ v ] = Variable ( '<STR_LIT>' + str ( i ) , Constant ( v ) . get_sort ( ) ) <EOL> i += <NUM_LIT:1> <EOL> renamed_core = substitute_constants_clauses ( core , renaming ) <EOL> res = simplify_clauses ( Clauses ( [ Or ( * [ negate ( c ) for c in renamed_core . fmlas ] ) ] ) ) <EOL> return res <EOL> def small_model_clauses ( cls ) : <EOL> return get_small_model ( cls , ivy_logic . uninterpreted_sorts ( ) , [ ] ) <EOL> class History ( object ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , state , maps = [ ] ) : <EOL> """<STR_LIT>""" <EOL> update , clauses , pre = state <EOL> assert update == None and pre . is_false ( ) <EOL> self . maps = maps <EOL> self . post = clauses <EOL> def forward_step ( self , axioms , update ) : <EOL> """<STR_LIT>""" <EOL> map1 , res = forward_image_map ( self . post , axioms , update ) <EOL> return History ( pure_state ( res ) , self . maps + [ map1 ] ) <EOL> def assume ( self , clauses ) : <EOL> """<STR_LIT>""" <EOL> if isinstance ( clauses , tuple ) : <EOL> assert is_pure_state ( clauses ) <EOL> clauses = clauses [ <NUM_LIT:1> ] <EOL> clauses = rename_distinct ( clauses , self . post ) <EOL> return History ( pure_state ( and_clauses ( self . post , clauses ) ) , self . maps ) <EOL> def ignore ( self , s , img , renaming ) : <EOL> res = not ( s in img or not s . is_skolem ( ) and s not in renaming ) <EOL> return res <EOL> def satisfy ( self , axioms , _get_model_clauses = None ) : <EOL> """<STR_LIT>""" <EOL> if _get_model_clauses is None : <EOL> _get_model_clauses = small_model_clauses <EOL> post = and_clauses ( self . post , axioms ) <EOL> print "<STR_LIT>" <EOL> model = _get_model_clauses ( post ) <EOL> print "<STR_LIT>" <EOL> if model == None : <EOL> return None <EOL> renaming , states , maps = { } , [ ] , reversed ( self . maps ) <EOL> while True : <EOL> img = set ( renaming [ s ] for s in renaming if not s . is_skolem ( ) ) <EOL> ignore = lambda s : self . ignore ( s , img , renaming ) <EOL> clauses = clauses_model_to_clauses ( post , ignore = ignore , model = model , numerals = use_numerals ( ) ) <EOL> clauses = rename_clauses ( clauses , inverse_map ( renaming ) ) <EOL> clauses = Clauses ( <EOL> [ f for f in clauses . fmlas if not is_tautology_equality ( f ) ] , <EOL> clauses . defs <EOL> ) <EOL> states . append ( clauses ) <EOL> try : <EOL> renaming = compose_maps ( next ( maps ) , renaming ) <EOL> except StopIteration : <EOL> break <EOL> uvs = model . universes ( numerals = use_numerals ( ) ) <EOL> return uvs , [ pure_state ( clauses ) for clauses in reversed ( states ) ] <EOL> def use_numerals ( ) : <EOL> return iu . use_numerals . get ( ) </s>
