Method test_implies

tests/test_z3_ported.py:490–493

(self)

        assert is_not(Not(p))

    def test_implies(self):
        p, q = Bools("p q")
        imp = Implies(p, q)
        assert is_implies(imp)

    def test_demorgan_proof(self, kernel):
        """Guide: De Morgan's law: Not(And(p,q)) == Or(Not(p), Not(q))"""