| 1234567891011121314151617181920212223 |
- (set-option :produce-unsat-cores true)
- (declare-sort C)
- (declare-const x C)
- (declare-const y C)
- (declare-const z C)
- (declare-fun P (C C) Bool)
- (declare-fun Q (C C) Bool)
- ; we assert the premise (and name it premise)
- (assert (! (= y z) :named premise))
- ; we assert the negation of the conclusion
- (assert (! (not (=> (and (Q z x) (P x z)) (and (P x y) (Q x y)))) :named conclusion))
- (check-sat)
- ;(get-model)
- ; now we assert this quantified formula (for commutativity) to add an additional axiom to the theory
- (assert (! (forall ((x C)) (forall ((y C)) (=> (Q x y) (Q y x)))) :named commutativity))
- ; this time it turns out to be valid (there exists no counterexample)
- (check-sat)
- ; the unsat core tells us that all assertions are needed for the unsat (validity) result
- ;(get-unsat-core)
|
