parameters: (self,lit,gen=0,specs = None)
docstring: Perform unit resolution using a literal.
  
          >>> r = UnitRes(to_clauses("[[a(),b()]]"))
          >>> r.propagate_lit(to_literal('~a()'))
          >>> r.unit_queue
          [b()]
          >>> r.watching
          [{}, {'a': [], 'b': []}]
          >>> r.subsumed
          [0]
          >>> r.clauses
          [[a(), b()]]
docstring_summary: Perform unit resolution using a literal.
docstring_tokens: Perform unit resolution using a literal .
function: def propagate_lit(self,lit,gen=0,specs = None):
          """
          Perform unit resolution using a literal.
  
          >>> r = UnitRes(to_clauses("[[a(),b()]]"))
          >>> r.propagate_lit(to_literal('~a()'))
          >>> r.unit_queue
          [b()]
          >>> r.watching
          [{}, {'a': [], 'b': []}]
          >>> r.subsumed
          [0]
          >>> r.clauses
          [[a(), b()]]
          """
  
  #        print self.index
          if self.equational_theory != None and is_ground_equality_lit(lit):
              self.propagate_equality(lit,gen)
              return
  #        if lit.atom.relname == '=' and lit.polarity == 0:
  #            return
          lits = [lit,Literal(lit.polarity,Atom('=',[lit.atom.args[1],lit.atom.args[0]]))] if lit.atom.relname == '=' else [lit]
          for lit in lits:
              keep = keep_lit(lit)
              indices = list(find_unifying(self.index,Literal(1 - lit.polarity,lit.atom))) # save this in cas index changes
              lit = lit_rep(canonize_literal_unique(lit))
              for index in indices:
                  wl = index[1]
      #        print "%s -- %s" % (lit,wl)
                  for i,j in list(wl): # copy the list in case we modify it
                      cl = self.clauses[i]
          #            print "cl: %s lit: %s" % (cl,lit)
                      lit2 = lit_rep(cl[j])
                      if lit2.polarity != 1-lit.polarity or lit2.atom.relname != lit.atom.relname:
                          print "!!! %s %s %s %s %s" % (i,j,lit,lit2,cl)
                          exit(1)
                      if is_equality_lit(lit2) and all(isinstance(t,Variable) for t in lit2.atom.args):
                          continue
                      match, subs, eqs = mgu_eq(lit.atom, lit2.atom)
          #            print "lit: %s" % lit
                      if match and self.allow_eqs(lit,eqs,False,cl):
                          if atom_subsume(lit.atom,lit2.atom):
                              self.deindex(i)
                              self.subsumed.append(i)
          #                print "lit: %s" % lit
                          new_cl = [substitute_lit(lit1, subs) for k,lit1 in enumerate(cl) if k != j] + [Literal(0,eq) for eq in eqs]
                          if not new_specialization and not (specs == None):
                              if verbose():
                                  print "using specs: %s" % specs
                              new_cl = substitute_constants_clause(new_cl,specs)
                          new_cl = simplify_clause(new_cl)
                          if not is_tautology(new_cl) and not self.subsumed_by_used_lit(lit,cl,new_cl):
                              if verbose():
                                  print "%s,%s -> %s" % (lit,cl,new_cl)
                              new_gen = max(gen+1,self.clauses_gen[i])
                              self.add_clause(new_cl,new_gen)
                              if self.unsat:
                                  return
                  
                  if keep:
                      self.resolve_units(lit,index[0],gen,False) # have to unify against units too!
                      if self.unsat:
                          return
              # if we are not keeping this unit as a consequence,
              # resolve it against all of the the units that might match
              # under equality, so that we can infer disequalities
              if keep == False:
                  others = [x for x in self.unit_term_index[lit.atom.relname] if self.unit_queue[x].polarity != lit.polarity]
                  self.resolve_units(lit,others,gen,True) # 
                  if self.unsat:
                      return
function_tokens: def propagate_lit ( self , lit , gen = 0 , specs = None ) : #        print self.index if self . equational_theory != None and is_ground_equality_lit ( lit ) : self . propagate_equality ( lit , gen ) return #        if lit.atom.relname == '=' and lit.polarity == 0: #            return lits = [ lit , Literal ( lit . polarity , Atom ( '=' , [ lit . atom . args [ 1 ] , lit . atom . args [ 0 ] ] ) ) ] if lit . atom . relname == '=' else [ lit ] for lit in lits : keep = keep_lit ( lit ) indices = list ( find_unifying ( self . index , Literal ( 1 - lit . polarity , lit . atom ) ) ) # save this in cas index changes lit = lit_rep ( canonize_literal_unique ( lit ) ) for index in indices : wl = index [ 1 ] #        print "%s -- %s" % (lit,wl) for i , j in list ( wl ) : # copy the list in case we modify it cl = self . clauses [ i ] #            print "cl: %s lit: %s" % (cl,lit) lit2 = lit_rep ( cl [ j ] ) if lit2 . polarity != 1 - lit . polarity or lit2 . atom . relname != lit . atom . relname : print "!!! %s %s %s %s %s" % ( i , j , lit , lit2 , cl ) exit ( 1 ) if is_equality_lit ( lit2 ) and all ( isinstance ( t , Variable ) for t in lit2 . atom . args ) : continue match , subs , eqs = mgu_eq ( lit . atom , lit2 . atom ) #            print "lit: %s" % lit if match and self . allow_eqs ( lit , eqs , False , cl ) : if atom_subsume ( lit . atom , lit2 . atom ) : self . deindex ( i ) self . subsumed . append ( i ) #                print "lit: %s" % lit new_cl = [ substitute_lit ( lit1 , subs ) for k , lit1 in enumerate ( cl ) if k != j ] + [ Literal ( 0 , eq ) for eq in eqs ] if not new_specialization and not ( specs == None ) : if verbose ( ) : print "using specs: %s" % specs new_cl = substitute_constants_clause ( new_cl , specs ) new_cl = simplify_clause ( new_cl ) if not is_tautology ( new_cl ) and not self . subsumed_by_used_lit ( lit , cl , new_cl ) : if verbose ( ) : print "%s,%s -> %s" % ( lit , cl , new_cl ) new_gen = max ( gen + 1 , self . clauses_gen [ i ] ) self . add_clause ( new_cl , new_gen ) if self . unsat : return if keep : self . resolve_units ( lit , index [ 0 ] , gen , False ) # have to unify against units too! if self . unsat : return # if we are not keeping this unit as a consequence, # resolve it against all of the the units that might match # under equality, so that we can infer disequalities if keep == False : others = [ x for x in self . unit_term_index [ lit . atom . relname ] if self . unit_queue [ x ] . polarity != lit . polarity ] self . resolve_units ( lit , others , gen , True ) #  if self . unsat : return