sympy/core/tests/test_facts.py

   1 from sympy.core.facts import deduce_alpha_implications, apply_beta_to_alpha_route, \
   2         rules_2prereq, split_rules_tt_tf_ft_ff, FactRules
   3 from sympy.core.logic import And
   4 from sympy.utilities.pytest import XFAIL
   5 import py
   6
   7 T = True
   8 F = False
   9 U = None
  10
  11
  12 def test_deduce_alpha_implications():
  13     def D(i):
  14         I = deduce_alpha_implications(i)
  15         P = rules_2prereq(I)
  16         return I,P
  17
  18     # transitivity
  19     I,P = D([('a','b'), ('b','c')])
  20     assert I == {'a': ['b','c'], 'b': ['c']}
  21     assert P == {'b': ['a'], 'c': ['a', 'b']}   # XXX a,b order unstable
  22
  23     # see if the output does not contain repeated implications
  24     I,P = D([('a','b'), ('b','c'), ('b','c')])
  25     assert I == {'a': ['b','c'], 'b': ['c']}
  26     assert P == {'b': ['a'], 'c': ['a', 'b']}   # XXX a,b order unstable
  27
  28     # see if it is tolerant to cycles
  29     assert D([('a','a'), ('a','a')]) == ({}, {})
  30     assert D([('a','b'), ('b','a')]) == ({'a': ['b'], 'b': ['a']},  {'a': ['b'], 'b': ['a']})
  31
  32     # see if it catches inconsistency
  33     py.test.raises(ValueError, "D([('a','!a')])")
  34     py.test.raises(ValueError, "D([('a','b'), ('b','!a')])")
  35     py.test.raises(ValueError, "D([('a','b'), ('b','c'), ('b','na'), ('na','!a')])")
  36
  37
  38     # something related to real-world
  39     I,P = D([('rat','real'), ('int','rat')])
  40
  41     assert I == {'int': ['rat', 'real'],  'rat': ['real']}
  42     assert P == {'rat': ['int'], 'real': ['int', 'rat']}    # XXX int,rat order unstable
  43
  44
  45 # TODO move me to appropriate place
  46 def test_apply_beta_to_alpha_route():
  47     APPLY = apply_beta_to_alpha_route
  48
  49     # indicates empty alpha-chain with attached beta-rule #bidx
  50     def Q(bidx):
  51         return ([],[bidx])
  52
  53     # x -> a        &(a,b) -> x     --  x -> a
  54     A = {'x': ['a']};       B = [ (And('a','b'), 'x') ]
  55     assert APPLY(A, B) == {'x': (['a'], []),    'a':Q(0), 'b':Q(0)}
  56
  57     # x -> a        &(a,!x) -> b    --  x -> a
  58     A = {'x': ['a']};       B = [ (And('a','!x'), 'b') ]
  59     assert APPLY(A, B) == {'x': (['a'], []),    '!x':Q(0), 'a':Q(0)}
  60
  61     # x -> a b      &(a,b) -> c     --  x -> a b c
  62     A = {'x': ['a','b']};   B = [ (And('a','b'), 'c') ]
  63     assert APPLY(A, B) == {'x': (['a','b','c'], []),    'a':Q(0), 'b':Q(0)}
  64
  65     # x -> a        &(a,b) -> y     --  x -> a [#0]
  66     A = {'x': ['a']};   B = [ (And('a','b'), 'y') ]
  67     assert APPLY(A, B) == {'x': (['a'], [0]),    'a':Q(0), 'b':Q(0)}
  68
  69     # x -> a b c    &(a,b) -> c     --  x -> a b c
  70     A = {'x': ['a','b','c']}
  71     B = [ (And('a','b'), 'c') ]
  72     assert APPLY(A, B) == {'x': (['a','b','c'], []),    'a':Q(0), 'b':Q(0)}
  73
  74     # x -> a b      &(a,b,c) -> y   --  x -> a b [#0]
  75     A = {'x': ['a','b']};   B = [ (And('a','b','c'), 'y') ]
  76     assert APPLY(A, B) == {'x': (['a','b'], [0]),    'a':Q(0), 'b':Q(0), 'c':Q(0)}
  77
  78     # x -> a b      &(a,b) -> c     --  x -> a b c d
  79     # c -> d                            c -> d
  80     A = {'x': ['a','b'], 'c': ['d']}
  81     B = [ (And('a','b'), 'c') ]
  82     assert APPLY(A, B) == {'x': (['a','b','c','d'], []), 'c': (['d'], []),    'a':Q(0), 'b':Q(0)}
  83
  84     # x -> a b      &(a,b) -> c     --  x -> a b c d e
  85     # c -> d        &(c,d) -> e         c -> d e
  86     A = {'x': ['a','b'], 'c': ['d']}
  87     B = [ (And('a','b'), 'c'), (And('c','d'), 'e') ]
  88     assert APPLY(A, B) == {'x': (['a','b','c','d','e'], []), 'c': (['d','e'], []),    'a':Q(0), 'b':Q(0), 'd':Q(1)}
  89
  90     # x -> a b      &(a,y) -> z     --  x -> a b y z
  91     #               &(a,b) -> y
  92     A = {'x': ['a','b']}
  93     B = [ (And('a','y'), 'z'),
  94           (And('a','b'), 'y') ]
  95     assert APPLY(A,B)  == {'x': (['a','b','y','z'], []),    'a':([],[0,1]), 'y':Q(0), 'b':Q(1)}
  96
  97     # x -> a b      &(a,!b) -> c    --  x -> a b
  98     A = {'x': ['a', 'b']}
  99     B = [ (And('a','!b'), 'c') ]
 100     assert APPLY(A,B)  == {'x': (['a', 'b'], []),    'a':Q(0), '!b':Q(0)}
 101
 102     # !x -> !a !b   &(!a,b) -> c    --  !x -> !a !b
 103     A = {'!x': ['!a', '!b']}
 104     B = [ (And('!a','b'), 'c') ]
 105     assert APPLY(A,B)  == {'!x': (['!a', '!b'], []),    '!a':Q(0), 'b':Q(0)}
 106
 107     # x -> a b      &(b,c) -> !a    --  x -> a b
 108     A = {'x': ['a','b']}
 109     B = [ (And('b','c'), '!a') ]
 110     assert APPLY(A,B)  == {'x': (['a','b'], []),    'b':Q(0), 'c':Q(0)}
 111
 112     # x -> a b      &(a, b) -> c    --  x -> a b c p
 113     # c -> p a
 114     A = {'x': ['a','b'], 'c': ['p','a']}
 115     B = [ (And('a','b'), 'c') ]
 116     assert APPLY(A,B)  == {'x': (['a','b','c','p'], []), 'c': (['p','a'], []),    'a':Q(0), 'b':Q(0)}
 117
 118     # TODO more tests?
 119
 120
 121 def test_split_rules_tf():
 122     S = split_rules_tt_tf_ft_ff
 123
 124     r = {'a': ['b', '!c', 'd'],
 125          'b': ['e', '!f'] }
 126
 127     tt, tf, ft, ff = S(r)
 128     assert tt == {'a': ['b', 'd'], 'b': ['e']}
 129     assert tf == {'a': ['c'],      'b': ['f']}
 130     assert ft == {}
 131     assert ff == {'b': ['a'], 'd': ['a'], 'e': ['b']}
 132
 133     r = {'!a': ['b', '!c'],
 134          'b' : ['e', '!f'] }
 135
 136     tt, tf, ft, ff = S(r)
 137     assert tt == {'b': ['e'], 'c': ['a']    }
 138     assert tf == {'b': ['f']    }
 139     assert ft == {'b': ['a']    }   # XXX ok? maybe vice versa?
 140     assert ff == {'e': ['b'], 'a': ['c']    }
 141
 142
 143 def test_FactRules_parse():
 144     f = FactRules('a -> b')
 145 #   assert f.negs       == {}
 146     assert f.rel_tt     == {'a': ['b']}
 147     assert f.rel_tf     == {}
 148     assert f.rel_ff     == {'b': ['a']}
 149     assert f.rel_ft     == {}
 150     assert f.prereq     == {'b': ['a'], 'a': ['b']}
 151
 152     f = FactRules('a -> !b')
 153     assert f.rel_tt     == {}
 154     assert f.rel_tf     == {'a': ['b'], 'b': ['a']}
 155     assert f.rel_ff     == {}
 156     assert f.rel_ft     == {}
 157     assert f.prereq     == {'b': ['a'], 'a': ['b']}
 158
 159     f = FactRules('!a -> b')
 160     assert f.rel_tt     == {}
 161     assert f.rel_tf     == {}
 162     assert f.rel_ff     == {}
 163     assert f.rel_ft     == {'a': ['b'], 'b': ['a']}
 164     assert f.prereq     == {'b': ['a'], 'a': ['b']}
 165
 166     f = FactRules('!a -> !b')
 167     assert f.rel_tt     == {'b': ['a']}
 168     assert f.rel_tf     == {}
 169     assert f.rel_ff     == {'a': ['b']}
 170     assert f.rel_ft     == {}
 171     assert f.prereq     == {'b': ['a'], 'a': ['b']}
 172
 173     f = FactRules('!z == nz')
 174     assert f.rel_tt     == {}
 175     assert f.rel_tf     == {'nz': ['z'], 'z': ['nz']}
 176     assert f.rel_ff     == {}
 177     assert f.rel_ft     == {'nz': ['z'], 'z': ['nz']}
 178     assert f.prereq     == {'z': ['nz'], 'nz': ['z']}
 179
 180     # TODO add parsing with | and & ?
 181
 182
 183 def test_FactRules_parse2():
 184     py.test.raises(ValueError, "FactRules('a -> !a')")
 185
 186
 187 def test_FactRules_deduce():
 188     f = FactRules(['a -> b', 'b -> c', 'b -> d', 'c -> e'])
 189     D = f.deduce_all_facts
 190
 191     assert D({'a': T})  == {'a': T, 'b': T, 'c': T, 'd': T, 'e': T}
 192     assert D({'b': T})  == {        'b': T, 'c': T, 'd': T, 'e': T}
 193     assert D({'c': T})  == {                'c': T,         'e': T}
 194     assert D({'d': T})  == {                        'd': T        }
 195     assert D({'e': T})  == {                                'e': T}
 196
 197     assert D({'a': F})  == {'a': F                                }
 198     assert D({'b': F})  == {'a': F, 'b': F                        }
 199     assert D({'c': F})  == {'a': F, 'b': F, 'c': F                }
 200     assert D({'d': F})  == {'a': F, 'b': F,         'd': F        }
 201
 202     assert D({'a': U})  == {'a': U} # XXX ok?
 203
 204
 205 def test_FactRules_deduce2():
 206     # pos/neg/zero, but the rules are not sufficient to derive all relations
 207     f = FactRules(['pos -> !neg', 'pos -> !z'])
 208     D = f.deduce_all_facts
 209
 210     assert D({'pos':T}) == {'pos': T, 'neg': F, 'z': F}
 211     assert D({'pos':F}) == {'pos': F                  }
 212     assert D({'neg':T}) == {'pos': F, 'neg': T        }
 213     assert D({'neg':F}) == {          'neg': F        }
 214     assert D({'z': T})  == {'pos': F,           'z': T}
 215     assert D({'z': F})  == {                    'z': F}
 216
 217     # pos/neg/zero. rules are sufficient to derive all relations
 218     f = FactRules(['pos -> !neg', 'neg -> !pos', 'pos -> !z', 'neg -> !z'])
 219     D = f.deduce_all_facts
 220
 221     assert D({'pos':T}) == {'pos': T, 'neg': F, 'z': F}
 222     assert D({'pos':F}) == {'pos': F                  }
 223     assert D({'neg':T}) == {'pos': F, 'neg': T, 'z': F}
 224     assert D({'neg':F}) == {          'neg': F        }
 225     assert D({'z': T})  == {'pos': F, 'neg': F, 'z': T}
 226     assert D({'z': F})  == {                    'z': F}
 227
 228
 229 def test_FactRules_deduce_multiple():
 230     # deduction that involves _several_ starting points
 231
 232     # TODO add the same check for 'npos == real & !pos' ?
 233     f = FactRules(['real == pos | npos'])
 234     D = f.deduce_all_facts
 235
 236     assert D({'real': T})   == {'real': T}
 237     assert D({'real': F})   == {'real': F, 'pos': F, 'npos': F}
 238     assert D({'pos' : T})   == {'real': T, 'pos': T}
 239     assert D({'npos': T})   == {'real': T, 'npos': T}
 240
 241     # --- key tests below ---
 242     assert D({'pos': F, 'npos': F}) == {'real': F, 'pos': F, 'npos': F}
 243     assert D({'real': T, 'pos': F}) == {'real': T, 'pos': F, 'npos': T}
 244     assert D({'real': T, 'npos':F}) == {'real': T, 'pos': T, 'npos': F}
 245
 246     assert D({'pos': T, 'npos': F}) == {'real': T, 'pos': T, 'npos': F}
 247     assert D({'pos': F, 'npos': T}) == {'real': T, 'pos': F, 'npos': T}
 248
 249
 250 def test_FactRules_deduce_multiple2():
 251
 252     f = FactRules(['real == neg | zero | pos'])
 253     D = f.deduce_all_facts
 254
 255     assert D({'real': T})   == {'real': T}
 256     assert D({'real': F})   == {'real': F, 'neg': F, 'zero': F, 'pos': F}
 257     assert D({'neg' : T})   == {'real': T, 'neg': T}
 258     assert D({'zero': T})   == {'real': T, 'zero': T}
 259     assert D({'pos' : T})   == {'real': T, 'pos': T}
 260
 261     # --- key tests below ---
 262     assert D({'neg': F, 'zero': F, 'pos': F})   ==  {'real': F, 'neg': F, 'zero': F, 'pos': F}
 263     assert D({'real':T, 'neg': F})              ==  {'real': T, 'neg': F}
 264     assert D({'real':T, 'zero':F})              ==  {'real': T, 'zero':F}
 265     assert D({'real':T, 'pos': F})              ==  {'real': T, 'pos': F}
 266
 267     assert D({'real':T,           'zero': F, 'pos': F}) == {'real': T, 'neg': T, 'zero': F, 'pos': F}
 268     assert D({'real':T, 'neg': F,            'pos': F}) == {'real': T, 'neg': F, 'zero': T, 'pos': F}
 269     assert D({'real':T, 'neg': F, 'zero': F          }) == {'real': T, 'neg': F, 'zero': F, 'pos': T}
 270
 271
 272     assert D({'neg': T, 'zero': F, 'pos': F})   ==  {'real': T, 'neg': T, 'zero': F, 'pos': F}
 273     assert D({'neg': F, 'zero': T, 'pos': F})   ==  {'real': T, 'neg': F, 'zero': T, 'pos': F}
 274     assert D({'neg': F, 'zero': F, 'pos': T})   ==  {'real': T, 'neg': F, 'zero': F, 'pos': T}
 275
 276
 277 def test_FactRules_deduce_base():
 278     # deduction that starts from base
 279
 280     f = FactRules(['real  == neg | zero | pos',
 281                    'neg   -> real & !zero & !pos',
 282                    'pos   -> real & !zero & !neg'])
 283     D = f.deduce_all_facts
 284
 285     base = D({'real': T, 'neg': F})
 286     assert base == {'real': T, 'neg': F}
 287
 288     X = D({'zero': F}, base=base)
 289
 290     assert X is base    # base is modified inplace
 291     assert base == {'real': T, 'neg': F, 'zero': F, 'pos': T}
 292
 293
 294 def test_FactRules_deduce_staticext():
 295     # verify that static beta-extensions deduction takes place
 296     f = FactRules(['real  == neg | zero | pos',
 297                    'neg   -> real & !zero & !pos',
 298                    'pos   -> real & !zero & !neg',
 299                    'nneg  == real & !neg',
 300                    'npos  == real & !pos'])
 301
 302     assert 'npos' in f.rel_tt['neg']
 303     assert 'nneg' in f.rel_tt['pos']
 304     assert 'nneg' in f.rel_tt['zero']
 305     assert 'npos' in f.rel_tt['zero']
 306
 307
 308 # NOTE: once upon a time there was an idea to intoruce copy-on-write (COW) mode
 309 # in deduce_all_facts, and also teach it to return list of newly derived knowledge.
 310 #
 311 # it turned out not to be better performance wise (or was i wrong ?), so this
 312 # mode was removed.
 313 #
 314 # However disabled test stays here just in case (maybe we'll return to this
 315 # idea some day)
 316 def X_test_FactRules_deduce_cow():
 317     f = FactRules(['real  == neg | zero | pos',
 318                    'neg   -> real & !zero & !pos',
 319                    'pos   -> real & !zero & !neg'])
 320     D = f.deduce_all_facts
 321
 322     base0 = D({'real': T, 'neg': F})
 323     assert base0 == {'real': T, 'neg': F}
 324
 325     base = base0.copy()
 326     X = D({'zero': F}, base=base, cow=False)
 327
 328     assert X is base    # base is modified inplace
 329     assert base == {'real': T, 'neg': F, 'zero': F, 'pos': T}
 330
 331     base = base0.copy()
 332     X, new_knowledge = D({'zero': F}, base=base, cow=True)
 333
 334     assert X is not base    # base should be copied
 335     assert base == {'real': T, 'neg': F}
 336
 337     assert X == {'real': T, 'neg': F, 'zero': F, 'pos': T}
 338     #assert set(new_knowledge) == set([ ('zero',F), ('pos',T) ])    # XXX disabled