Method test_xor_definition

tests/test_z3_ported.py:519–523

Xor(p,q) == And(Or(p,q), Not(And(p,q)))

(self, kernel)

        assert prove(claim)

    def test_xor_definition(self, kernel):
        """Xor(p,q) == And(Or(p,q), Not(And(p,q)))"""
        p, q = Bools("p q")
        claim = ForAll([p, q], Xor(p, q) == And(Or(p, q), Not(And(p, q))))
        assert prove(claim)

    def test_bool_biimplication(self, kernel):
        """(p == q) == And(Implies(p,q), Implies(q,p))"""