text: # -*- coding: utf-8 -*-
  
  """This is rule-based deduction system for SymPy
  
  The whole thing is split into two parts
  
   - rules compilation and preparation of tables
   - runtime inference
  
  For rule-based inference engines, the classical work is RETE algorithm [1], [2]
  Although we are not implementing it in full or even in some significant part,
  it's still worth to read about it to get the ideas behind.
  
  In short, every rule in a system of rules is one of two forms:
  
   - atom                     -> ...      (alpha rule)
   - And(atom1, atom2, ...)   -> ...      (beta rule)
  
  
  The major complexity is in efficient beta-rules processing and usually for an
  expert system a lot of effort goes into code that operates on beta-rules.
  
  
  Here we take minimalistic approach to get something usable first.
  
   - (preparation)    of alpha- and beta- networks, everything except
   - (runtime)        FactRules.deduce_all_facts
  
               _____________________________________
              ( Kirr: I've never thought that doing )
              ( logic stuff is that difficult...    )
               -------------------------------------
                      o   ^__^
                       o  (oo)\_______
                          (__)\       )\/\
                              ||----w |
                              ||     ||
  
  
  Some references on the topic
  ----------------------------
  
  [1] http://en.wikipedia.org/wiki/Rete_algorithm
  [2] http://reports-archive.adm.cs.cmu.edu/anon/1995/CMU-CS-95-113.pdf
  
  http://en.wikipedia.org/wiki/Propositional_formula
  http://en.wikipedia.org/wiki/Inference_rule
  http://en.wikipedia.org/wiki/List_of_rules_of_inference
  """
  
  
  
  from logic import fuzzy_not, name_not, Logic, And, Not
  
  def list_populate(l, item, skipif=None):
      """update list with an item, but only if it is not already there"""
      if item != skipif and (item not in l):
          l.append(item)
  
  
  
  # XXX this prepares forward-chaining rules for alpha-network
  
  # XXX better words?
  # NB: this procedure does not 'know' about not-relations
  # i.e. it treats 'a' and '!a' as independent variables while deriving implications.
  #
  # only in the end, we check that the whole result is consitent
  def deduce_alpha_implications(implications):
      """deduce all implications
  
         Description by example
         ----------------------
  
         given set of logic rules:
  
           a -> b
           b -> c
  
         we deduce all possible rules:
  
           a -> b, c
           b -> c
  
  
         implications: [] of (a,b)
         return:       {} of a -> [b, c, ...]
      """
  
      res = {} # a -> [] of implications(a)
  
      # NOTE: this could be optimized with e.g. toposort (?), but we need this
      # only at FactRules creation time (i.e. only once), so there is no demand
      # in further optimising this.
      for a,b in implications:
          if a==b:
              continue    # skip a->a cyclic input
  
          I = res.setdefault(a,[])
          list_populate(I,b)
  
          # UC:  -------------------------
          #     |                         |
          #     v                         |
          # a='rat' -> b='real' ==> (a_='int') -> 'real'
          for a_ in res:
              ra_ = res[a_]
              if a in ra_:
                  list_populate(ra_, b, skipif=a_)
  
  
          # UC:
          # a='pos' -> b='real' && (already have b='real' -> 'complex')
          #                   ||
          #                   vv
          # a='pos' -> 'complex'
          if b in res:
              ra = res[a]
              for b_ in res[b]:
                  list_populate(ra, b_, skipif=a)
  
      #print 'D:', res
  
      # let's see if the result is consistent
      for a, impl in res.iteritems():
          na = name_not(a)
          if na in impl:
              raise ValueError('implications are inconsistent: %s -> %s %s' % (a, na, impl))
  
      return res
  
  
  
  def apply_beta_to_alpha_route(alpha_implications, beta_rules):
      """apply additional beta-rules (And conditions) to already-built alpha implication tables
  
         TODO: write about
  
         - static extension of alpha-chains
         - attaching refs to beta-nodes to alpha chains
  
  
         e.g.
  
         alpha_implications:
  
         a  ->  [b, !c, d]
         b  ->  [d]
         ...
  
  
         beta_rules:
  
         &(b,d) -> e
  
  
         then we'll extend a's rule to the following
  
         a  ->  [b, !c, d, e]
      """
  
      x_impl = {}
  
      for x in alpha_implications.keys():
          x_impl[x] = (alpha_implications[x][:], [])
  
      # let's ensure that every beta-rule has appropriate entry (maybe even
      # empty) in the table.
      for bidx, (bcond,bimpl) in enumerate(beta_rules):
          for bk in bcond.args:
              if x_impl.has_key(bk):
                  continue
  
              x_impl[bk] = ([], [])
  
  
      # XXX maybe simplify passes logic?
  
      # we do it in 2 phases:
      #
      # 1st phase -- only do static extensions to alpha rules
      # 2nd phase -- attach beta-nodes which can be possibly triggered by an
      #              alpha-chain
      phase=1
      while True:
          seen_static_extension=False
  
          for bidx, (bcond,bimpl) in enumerate(beta_rules):
              assert isinstance(bcond, And)
  
              for x, (ximpls, bb) in x_impl.iteritems():
                  # A: x -> a     B: &(...) -> x      (non-informative)
                  if x == bimpl:  # XXX bimpl may become a list
                      continue
  
                  # A: ... -> a   B: &(...) -> a      (non-informative)
                  if bimpl in ximpls:
                      continue
  
                  # A: x -> a     B: &(a,!x) -> ...   (will never trigger)
                  if Not(x) in bcond.args:
                      continue
  
                  # A: x -> a...  B: &(!a,...) -> ... (will never trigger)
                  # A: x -> a...  B: &(...) -> !a     (will never trigger)
                  maytrigger=True
                  for xi in ximpls:
                      if (Not(xi) in bcond.args)  or  (Not(xi) == bimpl):
                          maytrigger=False
                          break
  
                  if not maytrigger:
                      continue
  
                  # A: x -> a,b   B: &(a,b) -> c      (static extension)
                  #                                       |
                  # A: x -> a,b,c <-----------------------+
                  for barg in bcond.args:
                      if not ( (barg == x) or (barg in ximpls) ):
                          break
                  else:
                      assert phase==1
                      list_populate(ximpls, bimpl)    # XXX bimpl may become a list
  
                      # we introduced new implication - now we have to restore
                      # completness of the whole set.
                      bimpl_impl = x_impl.get(bimpl)
                      if bimpl_impl is not None:
                          for _ in bimpl_impl[0]:
                              list_populate(ximpls, _)
  
                      seen_static_extension=True
                      continue
  
  
                  # does this beta-rule even has a chance to be triggered ?
                  if phase == 2:
                      for barg in bcond.args:
                          if (barg == x) or (barg in ximpls):
                              bb.append( bidx )
                              break
  
          # no static extensions was seen at this pass -- lets move to phase2
          if phase==1 and (not seen_static_extension):
              phase = 2
              continue
  
          # let's finish at the end of phase2
          if phase==2:
              break
  
  
      return x_impl
  
  
  
  # XXX this is something related to backward-chaining for alpha-network (?)
  # TODO adapt to handle beta nodes ?
  
  # TODO we need to sort prerequisites somehow, so that more closer prerequisites
  # would be tried first. e.g.
  #
  # nonzero <- [zero, integer, ..., prime], but not
  # nonzero <- [prime, ...]
  #
  # this could be done in other place...
  def rules_2prereq(rules):
      """build prerequisites table from rules
  
         Description by example
         ----------------------
  
         given set of logic rules:
  
           a -> b, c
           b -> c
  
         we build prerequisites (from what points something can be deduced):
  
           b <- a
           c <- a, b
  
         rules:   {} of a -> [b, c, ...]
         return:  {} of c <- [a, b, ...]
  
         Note however, that this prerequisites may be *not* enough to prove a
         fact. An example is 'a -> b' rule, where prereq(a) is b, and prereq(b)
         is a. That's because a=T -> b=T, and b=F -> a=F, but a=F -> b=?
      """
  
      prereq = {}
      for a, impl in rules.iteritems():
          for i in impl:
              pa = prereq.setdefault(i,[])
              pa.append(a)
  
      return prereq
  
  
  
  def split_rules_tt_tf_ft_ff(rules):
      """split alpha-rules into T->T & T->F & F->T & F->F chains
  
         and also rewrite them to be free of not-names
  
         Example
         -------
  
         'a' -> ['b', '!c']
  
         will be split into
  
         'a' -> ['b'] # tt: a -> b
         'a' -> ['c'] # tf: a -> !c
  
         and
         '!a' -> ['b']
  
         will become
  
         'b' -> ['a'] # ft: !b -> a
      """
  
  #   print 'split_rules_tt_tf_ft_ff'
  #   print rules
  
      tt = {}
      tf = {}
      ft = {}
  
      for k,impl in rules.iteritems():
          # k is not not-name
          if k[:1] != '!':
              for i in impl:
                  if i[:1] != '!':
                      dd = tt
                  else:
                      dd = tf
                      i  = i[1:]
  
                  I = dd.setdefault(k,[])
                  list_populate(I, i)
  
          # k is not-name
          else:
              k = k[1:]
  
              for i in impl:
                  if i[:1] != '!':
                      dd = ft
                  else:
                      dd = tt
                      i  = i[1:]
  
                  I = dd.setdefault(i,[])
                  list_populate(I, k)
  
  
      # FF is related to TT
      ff = {}
      for k,impl in tt.iteritems():
          for i in impl:
              I = ff.setdefault(i,[])
              I.append(k)
  
      return tt, tf, ft, ff
  
  
  
  
  
  ################
  # RULES PROVER #
  ################
  
  # XXX only for debugging -- kill me ?
  dbg_level = 0
  
  
  class TautologyDetected(Exception):
      """(internal) Prover uses it for reporting detected tautology"""
      pass
  
  
  class Prover(object):
      """ai - prover of logic rules
  
         given a set of initial rules, Prover tries to prove all possible rules
         which follow from given premises.
  
         As a result proved_rules are always either in one of two forms: alpha or
         beta:
  
         Alpha rules
         -----------
  
         This are rules of the form::
  
           a -> b & c & d & ...
  
  
         Beta rules
         ----------
  
         This are rules of the form::
  
           &(a,b,...) -> c & d & ...
  
  
         i.e. beta rules are join conditions that say that something follows when
         *several* facts are true at the same time.
      """
  
      __slots__ = ['proved_rules',    # [] of a,b     (a -> b  rule)
                   '_rules_seen',     # setof all seen rules
                  ]
  
  
      def __init__(self):
          self.proved_rules = []
          self._rules_seen  = set()
  
      def print_proved(self, title='proved rules'):
          print '\n--- %s ---' % title
          for a,b in self.proved_rules:
              print '%s\t->  %s' % (a,b)
  
          print '   - - - - -   '
          print
  
  
      def print_beta(self, title='proved rules (beta)'):
          print '\n --- %s ---' % title
  
          for n, (a,b) in enumerate(self.rules_beta):
              print '[#%i]  %s\t->  %s' % (n,a,b)
  
          print '   - - - - -   '
          print
  
  
      def split_alpha_beta(self):
          """split proved rules into alpha and beta chains"""
          rules_alpha = []    # a      -> b
          rules_beta  = []    # &(...) -> b
  
          for a,b in self.proved_rules:
              if isinstance(a, And):
                  rules_beta.append( (a,b) )
              else:
                  rules_alpha.append((a,b) )
  
          return rules_alpha, rules_beta
  
  
      @property
      def rules_alpha(self):
          return self.split_alpha_beta()[0]
  
      @property
      def rules_beta(self):
          return self.split_alpha_beta()[1]
  
  
  
      # XXX rename?
      def process_rule(self, a, b):
          """process a -> b rule"""   # TODO write more?
  
          # XXX this seems to be needed, but I can't get it to work without cycles
          # XXX sigh ...
          #if isinstance(a, And):
          #    a = a.expand()
          #if isinstance(b, And):
          #    b = b.expand()
  
  #       print ' -- %s\t->  %s' % (a,b)
  
          # we don't want rules whose premise is F, or who are trivial
          # skip:  F -> ...
          # skip:  ... -> F
          # skip:  ... -> T
          if (not a) or isinstance(b, bool):
              return
  
          # XXX can't we perform without this?
          # skip:  T -> ...
          if isinstance(a, bool):
              return
  
  
          # cycle detection: we don't want to process already seen rules
          if (a,b) in self._rules_seen:
              # already seen rule
              # XXX is it possible to design process_rule so we don't need
              # XXX this recursion detector? For me current answer is 'no'
              #                                                   -- kirr
              return
          else:
              self._rules_seen.add((a,b))
  
          # this is the core of processing
          try:
              self._process_rule(a, b)
          except TautologyDetected, t:
              #print 'Tautology:  %s -> %s   (%s)' % (t.args[0], t.args[1], t.args[2])
              pass
  
          else:
              # XXX negating here seems like the way to go. However we do
              # XXX *not* do it -- read below about why ...
              #
              # if not tautology, process negative rule as well
              # a -> b  -->  !b -> !a
          #   self.process_rule(Not(b), Not(a))
  
  
              # Unfortunately we can't handle the above negation -- in the
              # end our cycles detector is unable to catch all cycles,
              # especially ones where noise is mixed to already-known-facts,
              # e.g.
              #
              # say
              #
              #   a -> b
              #
              # is known fact, and at some point we get
              #
              #   a -> |(....., b)
              #
              # At present we are unable to detect this situation.
              #
              # I'm sorry -- I have no deep understanding of this logic
              # processing stuff and I'm very short on time ...
              #                                                  -- kirr
              pass
  
  
      # --- processing ---
  
      def _process_rule(self, a, b):
  
          # right part first
          if isinstance(b, Logic):
              # a -> b & c    -->  a -> b  ;  a -> c
              # (?) FIXME this is only correct when b & c != null !
              if   b.op == '&':
                  for barg in b.args:
                      self.process_rule(a, barg)
  
              # a -> b | c    -->  !b & !c -> !a
              #               -->   a & !b -> c & !b
              #               -->   a & !c -> b & !c
              #
              # NB: the last two rewrites add 1 term, so the rule *grows* in size.
              # NB: without catching terminating conditions this could continue infinitely
              elif b.op == '|':
                  # detect tautology first
                  if not isinstance(a, Logic):    # Atom
                      # tautology:  a -> a|c|...
                      if a in b.args:
                          raise TautologyDetected(a,b, 'a -> a|c|...')
  
                  self.process_rule(
                      And( *[Not(barg) for barg in b.args] ),
                      Not(a)
                  )
  
                  for bidx in range(len(b.args)):
                      barg = b.args[bidx]
                      brest= b.args[:bidx] + b.args[bidx+1:]
  
                      self.process_rule(
                          And( a, Not(barg) ),
                          And( b.__class__(*brest), Not(barg) )
                      )
  
              else:
                  raise ValueError('unknown b.op %r' % b.op)
  
  
          # left part
          elif isinstance(a, Logic):
              # a & b -> c    -->  IRREDUCIBLE CASE -- WE STORE IT AS IS
              #                    (this will be the basis of beta-network)
              if   a.op == '&':
                  # at this stage we should have right part alredy in simple form
                  assert not isinstance(b, Logic)
  
                  # tautology:  a & b -> a
                  if b in a.args:
                      raise TautologyDetected(a,b, 'a & b -> a')
  
                  self.proved_rules.append((a,b))
                  # XXX NOTE at present we ignore  !c -> !a | !b
  
              # a | b -> c    -->  a -> c  ;  b -> c
              elif a.op == '|':
  
                  # tautology:  a | b -> a
                  if b in a.args:
                      raise TautologyDetected(a,b, 'a | b -> a')
  
                  for aarg in a.args:
                      self.process_rule(aarg, b)
  
              else:
                  raise ValueError('unknown a.op %r' % a.op)
  
          else:
              # now this is the case where both `a` and `b` are atoms
              na, nb = name_not(a), name_not(b)
  
              self.proved_rules.append((a,b))     # a  -> b
  
              # XXX one day we may not need this -- read comments about
              # XXX negation close to the end of `process_rule`
              self.proved_rules.append((nb,na))   # !b -> !a
  
  
      def dbg_process_rule_2(a, b):
          global dbg_level
          print '%s%s\t->  %s' % (' '*(2*dbg_level), a, b)
          dbg_level += 1
  
          try:
              old_process_rule_2(a, b)
          finally:
              dbg_level -= 1
  
      #old_process_rule_2 = process_rule_2
      #process_rule_2 = dbg_process_rule_2
  
  
  
  ########################################
  
  
  # TODO link to RETE ?
  # TODO link to proposition logic ?
  class FactRules:
      """Rules that describe how to deduce facts in logic space
  
         When defined, this rules allow to quickly determine implications for a
         set of facts. For this precomputed deduction tables are used. see
         `deduce_all_facts`   (forward-chaining)
  
         Also it is possible to gather prerequisites for a fact, which is tried
         to be proven.    (backward-chaining)
  
  
         Definition Syntax
         -----------------
  
         a -> b       -- a=T -> b=T  (and automatically b=F -> a=F)
         a -> !b      -- a=T -> b=F
         a == b       -- a -> b & b -> a
         a -> b & c   -- a=T -> b=T & c=T
         # TODO b | c
  
  
         Internals
         ---------
  
         {} k -> [] of implications:
  
           .rel_tt      k=T -> k2=T
           .rel_tf      k=T -> k2=F
           .rel_ff      k=F -> k2=F
           .rel_ft      k=F -> k2=T
  
         .rel_tbeta     k=T -> [] of possibly triggering # of beta-rules
         .rel_fbeta     k=F -> ------------------//---------------------
  
         .rels    -- {} k -> tt, tf, ff, ft   (list of implications for k)
         .prereq  -- {} k <- [] of k's prerequisites
  
         .defined_facts -- set of defined fact names
      """
  
      def __init__(self, rules):
          """Compile rules into internal lookup tables"""
  
          if isinstance(rules, basestring):
              rules = rules.splitlines()
  
          # --- parse and process rules ---
          P = Prover()
  
          for rule in rules:
              # XXX `a` is hardcoded to be always atom
              a, op, b = rule.split(None, 2)
  
              a = Logic.fromstring(a)
              b = Logic.fromstring(b)
  
              if   op == '->':
                  P.process_rule(a, b)
              elif op == '==':
                  P.process_rule(a, b)
                  P.process_rule(b, a)
              else:
                  raise ValueError('unknown op %r' % op)
  
  
          #P.print_proved('RULES')
          #P.print_beta('BETA-RULES')
  
  
          # --- build deduction networks ---
  
          # deduce alpha implications
          impl_a = deduce_alpha_implications(P.rules_alpha)
  
          # now:
          # - apply beta rules to alpha chains  (static extension), and
          # - further associate beta rules to alpha chain (for inference at runtime)
          impl_ab = apply_beta_to_alpha_route(impl_a, P.rules_beta)
  
          if 0:
              print '\n --- ALPHA-CHAINS (I) ---'
  
              for a,b in impl_a.iteritems():
                  print '%s\t->  α(%2i):%s' % (a,len(b),b)
  
              print '   - - - - -   '
              print
  
          if 0:
              print '\n --- ALPHA-CHAINS (II) ---'
  
              for a,(b,bb) in impl_ab.iteritems():
                  print '%s\t->  α(%2i):%s  β(%s)' % (a,len(b),b, ' '.join(str(x) for x in bb))
  
              print '   - - - - -   '
              print
  
  
          # extract defined fact names
          self.defined_facts = set()
  
          for k in impl_ab.keys():
              if k[:1] == '!':
                  k = k[1:]
  
              self.defined_facts.add(k)
  
          #print 'defined facts:  (%2i)  %s' % (len(self.defined_facts), self.defined_facts)
  
  
          # now split each rule into four logic chains
          # (removing betaidxs from impl_ab view) (XXX is this needed?)
          impl_ab_ = dict( (k,impl)  for k, (impl,betaidxs) in impl_ab.iteritems())
          rel_tt, rel_tf, rel_ft, rel_ff = split_rules_tt_tf_ft_ff(impl_ab_)
  
          # XXX merge me with split_rules_tt_tf_ft_ff ?
          rel_tbeta = {}
          rel_fbeta = {}
  
          for k, (impl,betaidxs) in impl_ab.iteritems():
              if k[:1] == '!':
                  rel_xbeta = rel_fbeta
                  k         = name_not(k)
              else:
                  rel_xbeta = rel_tbeta
  
              rel_xbeta[k] = betaidxs
  
  
  
          self.rel_tt = rel_tt
          self.rel_tf = rel_tf
          self.rel_tbeta  = rel_tbeta
          self.rel_ff = rel_ff
          self.rel_ft = rel_ft
          self.rel_fbeta  = rel_fbeta
  
          self.beta_rules = P.rules_beta
  
          # build rels (forward chains)
          K = set (rel_tt.keys())
          K.update(rel_tf.keys())
          K.update(rel_ff.keys())
          K.update(rel_ft.keys())
  
          rels = {}
          empty= ()
          for k in K:
              tt = rel_tt.get(k,empty)
              tf = rel_tf.get(k,empty)
              ft = rel_ft.get(k,empty)
              ff = rel_ff.get(k,empty)
  
              tbeta = rel_tbeta.get(k,empty)
              fbeta = rel_fbeta.get(k,empty)
  
              rels[k] = tt, tf, tbeta,  ft, ff, fbeta
  
  
          self.rels = rels
  
          # build prereq (backward chains)
          prereq = {}
          for rel in [rel_tt, rel_tf, rel_ff, rel_ft]:
              rel_prereq = rules_2prereq(rel)
              for k,pitems in rel_prereq.iteritems():
                  kp = prereq.setdefault(k,[])
                  for p in pitems:
                      list_populate(kp, p)
  
          self.prereq = prereq
  
  
  
      # --- DEDUCTION ENGINE: RUNTIME CORE ---
  
      # TODO: add proper support for U (None), i.e.
      #       integer=U  -> rational=U  ??? (XXX i'm not sure)
  
  
      def deduce_all_facts(self, facts, base=None):
          """Deduce all facts from known facts ({} or [] of (k,v))
  
             *********************************************
             * This is the workhorse, so keep it *fast*. *
             *********************************************
  
             base  --  previously known facts (must be: fully deduced set)
                       attention: base is modified *inplace*  /optional/
  
             providing `base` could be needed for performance reasons -- we don't
             want to spend most of the time just re-deducing base from base
             (e.g. #base=50, #facts=2)
          """
  
          # keep frequently used attributes locally, so we'll avoid extra
          # attribute access overhead
          rels = self.rels
          beta_rules = self.beta_rules
  
          if base is not None:
              new_facts = base
          else:
              new_facts = {}
  
  
          # XXX better name ?
          def x_new_facts(keys, v):
              #print 'x_new_facts(%r,%r)' % (keys, v)
              for k in keys:
                  if k in new_facts:
                      #print 'seen_fact  %s:\t %s' % (k,v)
                      assert new_facts[k] == v, ('inconsitency between facts',new_facts,k,v)
                      continue
  
                  else:
                      #print 'new_fact   %s:\t %s' % (k,v)
                      new_facts[k] = v
  
  
          if type(facts) is dict:
              fseq = facts.iteritems()
          else:
              fseq = facts
  
  
          while True:
              beta_maytrigger = set()
  
              # --- alpha chains ---
              #print '**'
              for k,v in fseq:
                  #print '--'
  
                  # first, convert name to be not a not-name
                  if k[:1] == '!':
                      k = name_not(k)
                      v = fuzzy_not(v)
  
                  #new_fact(k, v)
                  if k in new_facts:
                      assert new_facts[k] == v, ('inconsitency between facts',new_facts,k,v)
  
                      # performance-wise it is important not to fire implied rules
                      # for already-seen fact -- we already did them all.
                      continue
  
                  else:
                      new_facts[k] = v
  
  
                  # some known fact -- let's follow it's implications
                  if v is not None:
  
                      # lookup routing tables
                      try:
                          tt, tf, tbeta,  ft, ff, fbeta = rels[k]
                      except KeyError:
                          pass
                      else:
                          # Now we have routing tables with *all* the needed
                          # implications for this k. This means we do not have to
                          # process each implications recursively!
                          # XXX this ^^^ is true only for alpha chains
  
                          # k=T
                          if v:
                              x_new_facts(tt, True)   # k -> i
                              x_new_facts(tf, False)  # k -> !i
  
                              beta_maytrigger.update(tbeta)
  
                          # k=F
                          else:
                              x_new_facts(ft, True)   # !k -> i
                              x_new_facts(ff, False)  # !k -> !i
  
                              beta_maytrigger.update(fbeta)
  
  
  
  
              # --- beta chains ---
  
              # if no beta-rules may trigger -- it's an end-of-story
              if not beta_maytrigger:
                  break
  
  
              #print '(β) MayTrigger: %s' % beta_maytrigger
  
              fseq = []
  
              # XXX this is dumb proof-of-concept trigger -- we'll need to optimize it
              # let's see which beta-rules to trigger
              for bidx in beta_maytrigger:
                  bcond,bimpl = beta_rules[bidx]
  
                  # let's see whether bcond is satisfied
                  for bk in bcond.args:
                      try:
                          if bk[:1] == '!':
                              bv = fuzzy_not(new_facts[bk[1:]])
                          else:
                              bv = new_facts[bk]
                      except KeyError:
                          break   # fact not found -- bcond not satisfied
  
                      # one of bcond's condition does not hold
                      if not bv:
                          break
  
                  else:
                      # all of bcond's condition hold -- let's fire this beta rule
                      #print '(β) Trigger #%i  (%s)' % (bidx, bimpl)
  
                      if bimpl[:1] == '!':
                          bimpl = bimpl[1:]
                          v = False
                      else:
                          v = True
  
                      fseq.append( (bimpl,v) )
  
  
          return new_facts
  
  
  
  
  ########################################
  
  
  
  # this was neeeded for testing -- feel free to remove this when everything
  # settles.
  #                                                               -- kirr
  if 0:
  
      FF = FactRules([
  
          'integer        ->  rational',
          'rational       ->  real',
          'real           ->  complex',
          'imaginary      ->  complex',
          'complex        ->  commutative',
  
          'odd            ==  integer & !even',
          'even           ==  integer & !odd',
  
          'real           ==  negative | zero | positive',
  
          'positive       ->  real & !negative & !zero',
          'negative       ->  real & !positive & !zero',
  
          'nonpositive    ==  real & !positive',
          'nonnegative    ==  real & !negative',
  
          'zero           ->  infinitesimal & even',
  
          'prime          ->  integer & positive',
          'composite      ==  integer & positive & !prime',
  
          'irrational     ==  real & !rational',
  
          'imaginary      ->  !real',     # XXX new ?
  
  
          '!bounded     ==  unbounded',
          '!commutative ==  noncommutative',
          '!complex     ==  noncomplex',
      #   '!integer     ==  noninteger',
          'noninteger     ==  real & !integer',   # XXX ok?
          '!zero        ==  nonzero',
          '!homogeneous ==  inhomogeneous',
  
          # XXX do we need this ?
          'finite     ->  bounded',       # XXX do we need this?
          'finite     ->  !zero',         # XXX wrong?
          'infinitesimal ->  !finite',    # XXX is this ok?
  
          # TODO we should remove this (very seldomly used, but affect performance):
          'nni    ==  integer & nonnegative',
          'npi    ==  integer & nonpositive',
          'pi     ==  integer & positive',
          'ni     ==  integer & negative',
      ])
  
      """
      FF = FactRules([
          'real   == pos | npos',
  
          'pos    -> real & !npos',
          'npos   -> real & !pos'
      ])
      """
  
      """
      ff = FactRules([
          'real   ->  complex',
          'real   ==  neg | zero | pos',
  
          'neg    ->  real & !pos & !zero',
          'zero   ->  real & !neg & !pos',
          'pos    ->  real & !neg & !zero',
  
          'npos   ==  real & !pos',
          'real   ==  pos | npos' # XXX this is a workaround for bug in process_rule
      ])
  
      FF = ff
      """
  