| 123456789101112131415161718192021222324252627282930 |
- (set-option :produce-proofs true)
- (declare-const x Bool)
- (declare-const y Bool)
- (declare-const z Bool)
- ; we define our conjecture
- (define-fun conjecture () Bool
- (=> (and (xor x y) (= y z))
- (and x z)))
- ; subsequently we assert the negation to check for validity
- (assert (not conjecture))
- ; check validity of conjecture by checking whether not conjecture is sat, which would mean there exists a counterexample
- (check-sat)
- ;(get-model)
- ; we assert a different value for x as a blocking clause to find additional solutions
- (assert (not (and (not x) y z)))
- (check-sat)
- ;(get-model)
- ; we assert a different value for y as a blocking clause to find additional solutions
- (assert (not (and x (not y) (not z))))
- (check-sat)
- ; as this formula has become unsat, we retrieve a proof
- ;(get-proof)
|
