|
>>> d = dexpr('([x],[A(c), ([y],[B(x,y,z,a)])->([z],[C(x,y,z,a)])])')
>>> print(d)
([x],[A(c), (([y],[B(x,y,z,a)]) -> ([z],[C(x,y,z,a)]))])
>>> d.pprint()
____________________________________
| x |
|------------------------------------|
| A(c) |
| ____________ ____________ |
| | y | | z | |
| (|------------| -> |------------|) |
| | B(x,y,z,a) | | C(x,y,z,a) | |
| |____________| |____________| |
|____________________________________|
>>> print(str(d))
([x],[A(c), (([y],[B(x,y,z,a)]) -> ([z],[C(x,y,z,a)]))])
>>> print(d.fol())
exists x.(A(c) & all y.(B(x,y,z,a) -> exists z.C(x,y,z,a)))
>>> print(d.replace(Variable('a'), DrtVariableExpression(Variable('r'))))
([x],[A(c), (([y],[B(x,y,z,r)]) -> ([z],[C(x,y,z,r)]))])
>>> print(d.replace(Variable('x'), DrtVariableExpression(Variable('r'))))
([x],[A(c), (([y],[B(x,y,z,a)]) -> ([z],[C(x,y,z,a)]))])
>>> print(d.replace(Variable('y'), DrtVariableExpression(Variable('r'))))
([x],[A(c), (([y],[B(x,y,z,a)]) -> ([z],[C(x,y,z,a)]))])
>>> print(d.replace(Variable('z'), DrtVariableExpression(Variable('r'))))
([x],[A(c), (([y],[B(x,y,r,a)]) -> ([z],[C(x,y,z,a)]))])
>>> print(d.replace(Variable('x'), DrtVariableExpression(Variable('r')), True))
([r],[A(c), (([y],[B(r,y,z,a)]) -> ([z],[C(r,y,z,a)]))])
>>> print(d.replace(Variable('y'), DrtVariableExpression(Variable('r')), True))
([x],[A(c), (([r],[B(x,r,z,a)]) -> ([z],[C(x,r,z,a)]))])
>>> print(d.replace(Variable('z'), DrtVariableExpression(Variable('r')), True))
([x],[A(c), (([y],[B(x,y,r,a)]) -> ([r],[C(x,y,r,a)]))])
>>> print(d == dexpr('([l],[A(c), ([m],[B(l,m,z,a)])->([n],[C(l,m,n,a)])])'))
True
>>> d = dexpr('([],[([x,y],[B(x,y,h), ([a,b],[dee(x,a,g)])])->([z,w],[cee(x,y,f), ([c,d],[E(x,c,d,e)])])])')
>>> sorted(d.free())
[Variable('B'), Variable('E'), Variable('e'), Variable('f'), Variable('g'), Variable('h')]
>>> sorted(d.variables())
[Variable('B'), Variable('E'), Variable('e'), Variable('f'), Variable('g'), Variable('h')]
>>> sorted(d.get_refs(True))
[Variable('a'), Variable('b'), Variable('c'), Variable('d'), Variable('w'), Variable('x'), Variable('y'), Variable('z')]
>>> sorted(d.conds[0].get_refs(False))
[Variable('x'), Variable('y')]
>>> print(dexpr('([x,y],[A(x,y), (x=y), ([],[B(x,y)])->([],[C(x,y)]), ([x,y],[D(x,y)])->([],[E(x,y)]), ([],[F(x,y)])->([x,y],[G(x,y)])])').eliminate_equality())
([x],[A(x,x), (([],[B(x,x)]) -> ([],[C(x,x)])), (([x,y],[D(x,y)]) -> ([],[E(x,y)])), (([],[F(x,x)]) -> ([x,y],[G(x,y)]))])
>>> print(dexpr('([x,y],[A(x,y), (x=y)]) -> ([],[B(x,y)])').eliminate_equality())
(([x],[A(x,x)]) -> ([],[B(x,x)]))
>>> print(dexpr('([x,y],[A(x,y)]) -> ([],[B(x,y), (x=y)])').eliminate_equality())
(([x,y],[A(x,y)]) -> ([],[B(x,x)]))
>>> print(dexpr('([x,y],[A(x,y), (x=y), ([],[B(x,y)])])').eliminate_equality())
([x],[A(x,x), ([],[B(x,x)])])
>>> print(dexpr('([x,y],[A(x,y), ([],[B(x,y), (x=y)])])').eliminate_equality())
([x,y],[A(x,y), ([],[B(x,x)])])
>>> print(dexpr('([z8 z9 z10],[A(z8), z8=z10, z9=z10, B(z9), C(z10), D(z10)])').eliminate_equality())
([z9],[A(z9), B(z9), C(z9), D(z9)])
|