<s> from ivy_resolution import mgu_eq <EOL> from ivy_logic import * <EOL> from ivy_logic_utils import * <EOL> import ivy_congclos as congclos <EOL> from collections import defaultdict <EOL> import ivy_logic <EOL> def verbose ( ) : <EOL> return False <EOL> literals = [ ] <EOL> lit_hash = dict ( ) <EOL> def lit_id ( lit ) : <EOL> """<STR_LIT>""" <EOL> key = ( lit . polarity , lit . atom . relname , tuple ( [ t . rep for t in lit . atom . args ] ) ) <EOL> if key in lit_hash : <EOL> return lit_hash [ key ] <EOL> id = len ( literals ) <EOL> literals . append ( lit ) <EOL> lit_hash [ key ] = id <EOL> return id <EOL> def canonize_literal ( lit ) : <EOL> """<STR_LIT>""" <EOL> subs = dict ( ) <EOL> terms = [ ] <EOL> for i , t in enumerate ( lit . atom . args ) : <EOL> if isinstance ( t , Variable ) : <EOL> if t . rep not in subs : <EOL> subs [ t . rep ] = Constant ( "<STR_LIT>" + str ( i ) ) <EOL> terms . append ( subs [ t . rep ] ) <EOL> else : <EOL> terms . append ( t ) <EOL> return ( Literal ( lit . polarity , Atom ( lit . atom . relname , terms ) ) , subs ) <EOL> def canonize_literal_vars ( lit ) : <EOL> """<STR_LIT>""" <EOL> subs = dict ( ) <EOL> terms = [ ] <EOL> for i , t in enumerate ( lit . atom . args ) : <EOL> if isinstance ( t , Variable ) : <EOL> if t . rep not in subs : <EOL> subs [ t . rep ] = Variable ( "<STR_LIT>" + str ( i ) , t . sort ) <EOL> terms . append ( subs [ t . rep ] ) <EOL> else : <EOL> terms . append ( t ) <EOL> return Literal ( lit . polarity , Atom ( lit . atom . relname , terms ) ) <EOL> def canonize_literal_unique ( lit ) : <EOL> """<STR_LIT>""" <EOL> subs = dict ( ) <EOL> terms = [ ] <EOL> for i , t in enumerate ( lit . atom . args ) : <EOL> if isinstance ( t , Variable ) : <EOL> if t . rep not in subs : <EOL> subs [ t . rep ] = Variable ( "<STR_LIT>" + str ( i ) , t . sort ) <EOL> terms . append ( subs [ t . rep ] ) <EOL> else : <EOL> terms . append ( t ) <EOL> return Literal ( lit . polarity , Atom ( lit . atom . relname , terms ) ) <EOL> def lit_is_specialization ( lit ) : <EOL> return ( lit . polarity == <NUM_LIT:0> <EOL> and lit . atom . relname == "<STR_LIT:=>" <EOL> and lit . atom . args [ <NUM_LIT:0> ] . rep . startswith ( '<STR_LIT>' ) <EOL> and isinstance ( lit . atom . args [ <NUM_LIT:0> ] , Constant ) ) <EOL> def get_specializations ( cl , specs ) : <EOL> clspecs = [ lit for lit in cl if lit_is_specialization ( lit ) ] <EOL> if len ( cl ) - len ( clspecs ) <= <NUM_LIT:1> : <EOL> for lit in clspecs : <EOL> specs [ lit . atom . args [ <NUM_LIT:0> ] . rep ] . add ( lit . atom . args [ <NUM_LIT:1> ] . rep ) <EOL> def make_index ( ) : <EOL> return [ [ ] , [ ] , defaultdict ( make_index ) ] <EOL> def index_lookup ( index , lit ) : <EOL> index = index [ lit . polarity ] [ lit . atom . relname ] <EOL> for t in lit . atom . args : <EOL> index = index [ <NUM_LIT:2> ] [ "<STR_LIT>" if isinstance ( t , Variable ) else t . rep ] <EOL> return index <EOL> equational_theory = None <EOL> class EqualityTheory ( object ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , et ) : <EOL> self . equational_theory = et <EOL> def __enter__ ( self ) : <EOL> global equational_theory <EOL> self . old_theory = equational_theory <EOL> equational_theory = self . equational_theory <EOL> return self <EOL> def __exit__ ( self , exc_type , exc_val , exc_tb ) : <EOL> global equational_theory <EOL> equational_theory = self . old_theory <EOL> return False <EOL> def find_term ( term ) : <EOL> if equational_theory == None : <EOL> return term <EOL> return equational_theory . find ( term ) <EOL> def ground_match ( term , index ) : <EOL> if equational_theory == None : <EOL> yield term . rep <EOL> else : <EOL> trep = equational_theory . find ( term ) <EOL> for t2 in index : <EOL> if equational_theory . find_by_name ( t2 ) is trep : <EOL> yield t2 <EOL> def find_subsumed_rec ( index , terms , idx ) : <EOL> if idx >= len ( terms ) : <EOL> yield index <EOL> return <EOL> t = terms [ idx ] <EOL> if isinstance ( t , Variable ) : <EOL> for x , sub_index in index [ <NUM_LIT:2> ] . iteritems ( ) : <EOL> for y in find_subsumed_rec ( sub_index , terms , idx + <NUM_LIT:1> ) : <EOL> yield y <EOL> else : <EOL> for t2 in ground_match ( t , index [ <NUM_LIT:2> ] ) : <EOL> for y in find_subsumed_rec ( index [ <NUM_LIT:2> ] [ t2 ] , terms , idx + <NUM_LIT:1> ) : <EOL> yield y <EOL> def find_subsuming_rec ( index , terms , idx ) : <EOL> if idx >= len ( terms ) : <EOL> yield index <EOL> return <EOL> t = terms [ idx ] <EOL> if "<STR_LIT>" in index [ <NUM_LIT:2> ] : <EOL> for y in find_subsuming_rec ( index [ <NUM_LIT:2> ] [ "<STR_LIT>" ] , terms , idx + <NUM_LIT:1> ) : <EOL> yield y <EOL> if not isinstance ( t , Variable ) : <EOL> for t2 in ground_match ( t , index [ <NUM_LIT:2> ] ) : <EOL> for y in find_subsuming_rec ( index [ <NUM_LIT:2> ] [ t2 ] , terms , idx + <NUM_LIT:1> ) : <EOL> yield y <EOL> def find_unifying_rec ( index , terms , idx ) : <EOL> if idx >= len ( terms ) : <EOL> yield index <EOL> return <EOL> t = terms [ idx ] <EOL> if isinstance ( t , Variable ) or t . rep . startswith ( '<STR_LIT>' ) : <EOL> for x , sub_index in index [ <NUM_LIT:2> ] . iteritems ( ) : <EOL> for y in find_unifying_rec ( sub_index , terms , idx + <NUM_LIT:1> ) : <EOL> yield y <EOL> else : <EOL> if "<STR_LIT>" in index [ <NUM_LIT:2> ] : <EOL> for y in find_unifying_rec ( index [ <NUM_LIT:2> ] [ "<STR_LIT>" ] , terms , idx + <NUM_LIT:1> ) : <EOL> yield y <EOL> for t2 in ground_match ( t , index [ <NUM_LIT:2> ] ) : <EOL> for y in find_unifying_rec ( index [ <NUM_LIT:2> ] [ t2 ] , terms , idx + <NUM_LIT:1> ) : <EOL> yield y <EOL> def find_subsumed ( index , lit ) : <EOL> index = index [ lit . polarity ] [ lit . atom . relname ] <EOL> return find_subsumed_rec ( index , lit . atom . args , <NUM_LIT:0> ) <EOL> def find_subsuming ( index , lit ) : <EOL> index = index [ lit . polarity ] [ lit . atom . relname ] <EOL> return find_subsuming_rec ( index , lit . atom . args , <NUM_LIT:0> ) <EOL> def find_unifying ( index , lit ) : <EOL> index = index [ lit . polarity ] [ lit . atom . relname ] <EOL> return find_unifying_rec ( index , lit . atom . args , <NUM_LIT:0> ) <EOL> def lit_rep ( lit ) : <EOL> if equational_theory == None : <EOL> return lit <EOL> terms = [ ( a if isinstance ( a , Variable ) else equational_theory . find ( a ) ) for a in lit . atom . args ] <EOL> return Literal ( lit . polarity , Atom ( lit . atom . relname , terms ) ) <EOL> def clause_rep ( clause ) : <EOL> if equational_theory == None : <EOL> return clause <EOL> return [ lit_rep ( l ) for l in clause ] <EOL> def lit_subsume_mod_eq ( lit1 , lit2 , env ) : <EOL> return lit_subsume ( lit_rep ( lit1 ) , lit_rep ( lit2 ) , env ) <EOL> new_specialization = True <EOL> class UnitRes ( object ) : <EOL> """<STR_LIT>""" <EOL> def __init__ ( self , clauses ) : <EOL> self . clauses = [ ] <EOL> self . index = [ defaultdict ( make_index ) , defaultdict ( make_index ) ] <EOL> self . unit_queue = [ ] <EOL> self . subsumed = [ ] <EOL> self . unsat = False <EOL> self . used_units = <NUM_LIT:0> <EOL> self . stack = [ ] <EOL> self . clauses_gen = [ ] <EOL> self . unit_queue_gen = [ ] <EOL> self . unit_ids = set ( ) <EOL> self . detected_specializations = [ ] <EOL> self . equational_theory = congclos . CongClos ( ) <EOL> self . unit_term_index = defaultdict ( list ) <EOL> with UnsortedContext ( ) : <EOL> with self . context ( ) : <EOL> for cl in clauses : <EOL> self . add_clause ( cl ) <EOL> def context ( self ) : <EOL> return EqualityTheory ( self . equational_theory ) <EOL> def unit_subsumed_basic ( self , lit ) : <EOL> subsuming = find_subsuming ( self . index , lit ) <EOL> for index in subsuming : <EOL> for lit2_idx in index [ <NUM_LIT:0> ] : <EOL> lit2 = self . unit_queue [ lit2_idx ] <EOL> if lit_subsume_mod_eq ( lit2 , lit , dict ( ) ) : <EOL> return True <EOL> return False <EOL> def unit_subsumed ( self , lit ) : <EOL> return ( self . unit_subsumed_basic ( lit ) <EOL> or ( is_disequality_lit ( lit ) and self . unit_subsumed_basic ( swap_args_lit ( lit ) ) ) ) <EOL> def add_clause_basic ( self , cl , gen = <NUM_LIT:0> ) : <EOL> n = len ( cl ) <EOL> if n == <NUM_LIT:0> : <EOL> self . unsat = True <EOL> self . used_units = len ( self . unit_queue ) <EOL> elif n == <NUM_LIT:1> : <EOL> lit = lit_rep ( canonize_literal_vars ( cl [ <NUM_LIT:0> ] ) ) <EOL> if not is_taut_lit ( lit ) and not self . unit_subsumed ( lit ) : <EOL> litid = lit_id ( lit ) <EOL> index_lookup ( self . index , lit ) [ <NUM_LIT:0> ] . append ( len ( self . unit_queue ) ) <EOL> self . unit_queue . append ( lit ) <EOL> self . unit_queue_gen . append ( gen ) <EOL> self . unit_ids . add ( litid ) <EOL> if verbose ( ) : <EOL> print "<STR_LIT>" % ( lit , litid ) <EOL> else : <EOL> i = len ( self . clauses ) <EOL> self . clauses . append ( cl ) <EOL> self . clauses_gen . append ( gen ) <EOL> self . reindex ( i ) <EOL> def add_clause ( self , cl , gen = <NUM_LIT:0> ) : <EOL> self . add_clause_basic ( cl , gen ) <EOL> if len ( cl ) == <NUM_LIT:2> and is_ground_clause ( cl ) : <EOL> for i in [ <NUM_LIT:0> , <NUM_LIT:1> ] : <EOL> lhs , rhs = cl [ i ] , cl [ <NUM_LIT:1> - i ] <EOL> if is_disequality_lit ( lhs ) and is_equality_lit ( rhs ) : <EOL> for j in [ <NUM_LIT:0> , <NUM_LIT:1> ] : <EOL> subs = { lhs . atom . args [ j ] . rep : lhs . atom . args [ <NUM_LIT:1> - j ] } <EOL> new_rhs = substitute_constants_lit ( rhs , subs ) <EOL> if not lit_eq ( rhs , new_rhs ) : <EOL> new_cl = [ lhs , new_rhs ] <EOL> print "<STR_LIT>" % cl <EOL> self . add_clause_basic ( new_cl , gen ) <EOL> def update_equational_theory ( self , lit ) : <EOL> if lit . polarity == <NUM_LIT:1> and lit . atom . relname == '<STR_LIT:=>' : <EOL> t0 , t1 = lit . atom . args [ <NUM_LIT:0> ] , lit . atom . args [ <NUM_LIT:1> ] <EOL> if isinstance ( t0 , Constant ) and isinstance ( t1 , Constant ) : <EOL> equational_theory . union ( t0 , t1 ) <EOL> if verbose ( ) : <EOL> print "<STR_LIT>" % ( t0 , t1 ) <EOL> def get_watching ( self , lit ) : <EOL> return index_lookup ( self . index , lit ) [ <NUM_LIT:1> ] <EOL> def deindex ( self , i ) : <EOL> for j in range ( <NUM_LIT:0> , len ( self . clauses [ i ] ) ) : <EOL> lit = self . clauses [ i ] [ j ] <EOL> wl = self . get_watching ( lit ) <EOL> wl . remove ( ( i , j ) ) <EOL> def reindex ( self , i ) : <EOL> for j , lit in enumerate ( self . clauses [ i ] ) : <EOL> self . get_watching ( lit ) . append ( ( i , j ) ) <EOL> def index_unit_terms ( self , i ) : <EOL> used = set ( ) <EOL> for t in self . unit_queue [ i ] . atom . args : <EOL> if not isinstance ( t , Variable ) and t . rep not in used : <EOL> used . add ( t . rep ) <EOL> if any ( lit_eq ( self . unit_queue [ j ] , self . unit_queue [ i ] ) for j in self . unit_term_index [ t . rep ] ) : <EOL> print "<STR_LIT>" % ( self . unit_queue [ i ] , i , self . unit_term_index [ t . rep ] ) <EOL> exit ( <NUM_LIT:1> ) <EOL> self . unit_term_index [ t . rep ] . append ( i ) <EOL> self . unit_term_index [ self . unit_queue [ i ] . atom . relname ] . append ( i ) <EOL> def deindex_unit_terms ( self , i ) : <EOL> used = set ( ) <EOL> for t in self . unit_queue [ i ] . atom . args : <EOL> if not isinstance ( t , Variable ) and t . rep not in used : <EOL> used . add ( t . rep ) <EOL> self . unit_term_index [ t . rep ] . remove ( i ) <EOL> self . unit_term_index [ self . unit_queue [ i ] . atom . relname ] . remove ( i ) <EOL> def unit_subsumed_by_used ( self , lit ) : <EOL> subsuming = find_subsuming ( self . index , lit ) <EOL> for index in subsuming : <EOL> for lit2_idx in index [ <NUM_LIT:0> ] : <EOL> if lit2_idx < self . used_units : <EOL> lit2 = self . unit_queue [ lit2_idx ] <EOL> if lit_subsume_mod_eq ( lit2 , lit , dict ( ) ) : <EOL> return True <EOL> return False <EOL> def subsumed_by_used_lit ( self , a1 , a2 , clause ) : <EOL> for lit in clause : <EOL> if self . unit_subsumed_by_used ( lit ) or self . unit_subsumed_by_used ( Literal ( <NUM_LIT:1> - lit . polarity , lit . atom ) ) : <EOL> return True <EOL> return False <EOL> def allow_eqs ( self , lit , eqs , is_unit = False , other = None ) : <EOL> if lit . atom . relname == '<STR_LIT:=>' : <EOL> return not eqs <EOL> if all ( atom . args [ <NUM_LIT:0> ] . rep . startswith ( '<STR_LIT>' ) and not atom . args [ <NUM_LIT:1> ] . rep . startswith ( '<STR_LIT>' ) for atom in eqs ) : <EOL> if not new_specialization or is_unit : <EOL> return True <EOL> if eqs and verbose ( ) : <EOL> print "<STR_LIT>" % ( lit , other , eqs ) <EOL> self . detected_specializations . extend ( eqs ) <EOL> return not eqs <EOL> def propagate_equality ( self , lit , gen ) : <EOL> lit = lit_rep ( lit ) <EOL> if is_taut_lit ( lit ) : <EOL> return <EOL> t0 , t1 = lit . atom . args [ <NUM_LIT:0> ] , lit . atom . args [ <NUM_LIT:1> ] <EOL> if t0 . rep < t1 . rep : <EOL> t0 , t1 = t1 , t0 <EOL> for lit_idx in self . unit_term_index [ t0 . rep ] : <EOL> lit2 = self . unit_queue [ lit_idx ] <EOL> lit3 = substitute_constants_lit ( lit2 , { t0 . rep : t1 } ) <EOL> if not lit_eq ( lit2 , lit3 ) : <EOL> new_cl = [ lit3 ] <EOL> if verbose ( ) : <EOL> print "<STR_LIT>" % ( lit , lit2 , new_cl ) <EOL> new_gen = max ( gen + <NUM_LIT:1> , self . unit_queue_gen [ lit_idx ] ) <EOL> self . add_clause ( new_cl , new_gen ) <EOL> if self . unsat : <EOL> return <EOL> self . update_equational_theory ( lit ) <EOL> for lit_idx in self . unit_term_index [ t1 . rep ] : <EOL> lit2 = self . unit_queue [ lit_idx ] <EOL> if verbose ( ) : <EOL> print "<STR_LIT>" % lit2 <EOL> self . propagate_lit ( lit2 , max ( gen + <NUM_LIT:1> , self . unit_queue_gen [ lit_idx ] ) ) <EOL> if self . unsat : <EOL> return <EOL> def propagate_lit ( self , lit , gen = <NUM_LIT:0> , specs = None ) : <EOL> """<STR_LIT>""" <EOL> if self . equational_theory != None and is_ground_equality_lit ( lit ) : <EOL> self . propagate_equality ( lit , gen ) <EOL> return <EOL> lits = [ lit , Literal ( lit . polarity , Atom ( '<STR_LIT:=>' , [ lit . atom . args [ <NUM_LIT:1> ] , lit . atom . args [ <NUM_LIT:0> ] ] ) ) ] if lit . atom . relname == '<STR_LIT:=>' else [ lit ] <EOL> for lit in lits : <EOL> keep = keep_lit ( lit ) <EOL> indices = list ( find_unifying ( self . index , Literal ( <NUM_LIT:1> - lit . polarity , lit . atom ) ) ) <EOL> lit = lit_rep ( canonize_literal_unique ( lit ) ) <EOL> for index in indices : <EOL> wl = index [ <NUM_LIT:1> ] <EOL> for i , j in list ( wl ) : <EOL> cl = self . clauses [ i ] <EOL> lit2 = lit_rep ( cl [ j ] ) <EOL> if lit2 . polarity != <NUM_LIT:1> - lit . polarity or lit2 . atom . relname != lit . atom . relname : <EOL> print "<STR_LIT>" % ( i , j , lit , lit2 , cl ) <EOL> exit ( <NUM_LIT:1> ) <EOL> if is_equality_lit ( lit2 ) and all ( isinstance ( t , Variable ) for t in lit2 . atom . args ) : <EOL> continue <EOL> match , subs , eqs = mgu_eq ( lit . atom , lit2 . atom ) <EOL> if match and self . allow_eqs ( lit , eqs , False , cl ) : <EOL> if atom_subsume ( lit . atom , lit2 . atom ) : <EOL> self . deindex ( i ) <EOL> self . subsumed . append ( i ) <EOL> new_cl = [ substitute_lit ( lit1 , subs ) for k , lit1 in enumerate ( cl ) if k != j ] + [ Literal ( <NUM_LIT:0> , eq ) for eq in eqs ] <EOL> if not new_specialization and not ( specs == None ) : <EOL> if verbose ( ) : <EOL> print "<STR_LIT>" % specs <EOL> new_cl = substitute_constants_clause ( new_cl , specs ) <EOL> new_cl = simplify_clause ( new_cl ) <EOL> if not is_tautology ( new_cl ) and not self . subsumed_by_used_lit ( lit , cl , new_cl ) : <EOL> if verbose ( ) : <EOL> print "<STR_LIT>" % ( lit , cl , new_cl ) <EOL> new_gen = max ( gen + <NUM_LIT:1> , self . clauses_gen [ i ] ) <EOL> self . add_clause ( new_cl , new_gen ) <EOL> if self . unsat : <EOL> return <EOL> if keep : <EOL> self . resolve_units ( lit , index [ <NUM_LIT:0> ] , gen , False ) <EOL> if self . unsat : <EOL> return <EOL> if keep == False : <EOL> others = [ x for x in self . unit_term_index [ lit . atom . relname ] if self . unit_queue [ x ] . polarity != lit . polarity ] <EOL> self . resolve_units ( lit , others , gen , True ) <EOL> if self . unsat : <EOL> return <EOL> def resolve_units ( self , lit , units , gen , allow_unit_diseqs ) : <EOL> for lit_idx in list ( units ) : <EOL> lit2 = lit_rep ( self . unit_queue [ lit_idx ] ) <EOL> match , subs , eqs = mgu_eq ( lit . atom , lit2 . atom ) <EOL> if match and ( self . allow_eqs ( lit , eqs , True ) or ( allow_unit_diseqs and len ( eqs ) == <NUM_LIT:1> and keep_atom ( eqs [ <NUM_LIT:0> ] ) ) ) : <EOL> new_cl = [ Literal ( <NUM_LIT:0> , eq ) for eq in eqs ] <EOL> if not self . subsumed_by_used_lit ( lit , lit2 , new_cl ) : <EOL> if verbose ( ) : <EOL> print "<STR_LIT>" % ( lit , lit2 , new_cl ) <EOL> new_gen = max ( gen + <NUM_LIT:1> , self . unit_queue_gen [ lit_idx ] ) <EOL> self . add_clause ( new_cl , new_gen ) <EOL> if self . unsat : <EOL> return <EOL> def propagate ( self , specs = None ) : <EOL> """<STR_LIT>""" <EOL> save_thing = ivy_logic . allow_unsorted <EOL> ivy_logic . allow_unsorted = True <EOL> while self . used_units < len ( self . unit_queue ) : <EOL> lit_num = self . used_units <EOL> lit = self . unit_queue [ lit_num ] <EOL> gen = self . unit_queue_gen [ lit_num ] <EOL> self . propagate_lit ( lit , gen , specs ) <EOL> if self . used_units < lit_num + <NUM_LIT:1> : <EOL> self . used_units = lit_num + <NUM_LIT:1> <EOL> for j in range ( lit_num , self . used_units ) : <EOL> self . index_unit_terms ( j ) <EOL> ivy_logic . allow_unsorted = save_thing <EOL> def keep_atom ( atom ) : <EOL> name = atom . relname <EOL> if name . is_skolem ( ) : <EOL> return False <EOL> for term in atom . args : <EOL> if is_constant ( term ) and term . rep . is_skolem ( ) : <EOL> return False <EOL> return True <EOL> def keep_lit ( lit ) : <EOL> return keep_atom ( lit . atom ) <EOL> if __name__ == "<STR_LIT:__main__>" : <EOL> r = UnitRes ( to_clauses ( "<STR_LIT>" ) ) <EOL> with r . context ( ) : <EOL> r . propagate ( ) <EOL> print r . unit_queue </s>
