def find_unit_clause_int_repr(clauses, model):
 bound = (set(model) | set(((- sym) for sym in model)))
 for clause in clauses:
  unbound = (clause - bound)
  if (len(unbound) == 1):
   p = unbound.pop()
   if (p < 0):
    return ((- p), False)
   else:
    return (p, True)
 return (None, None)

def find_unit_clause_int_repr ( clauses , model ) : bound = ( set ( model ) | set ( ( ( - sym ) for sym in model ) ) ) for clause in clauses : unbound = ( clause - bound ) if ( len ( unbound ) == 1 ) : p = unbound . pop ( ) if ( p < 0 ) : return ( ( - p ) , False ) else : return ( p , True ) return ( None , None )
same as find_unit_clause .