Proving the Strict Weak Ordering property

comparator.cc

    bool operator()(const InternalExtractorEdge &lhs, const InternalExtractorEdge &rhs) const
    {
        return (lhs.result.source <  rhs.result.source) ||
              ((lhs.result.source == rhs.result.source) &&
               (lhs.result.target <  rhs.result.target));
    }

prove.smt2

(declare-datatypes (SourceT TargetT) ((EdgeT (makeEdge (source SourceT) (target TargetT)))))
(define-sort Edge () (EdgeT Int Int))

(define-fun cmp ((lhs Edge) (rhs Edge)) (Bool)
  (or
    (< (source lhs) (source rhs))
    (and (= (source lhs) (source rhs)) (< (target lhs) (target rhs)))))
    
(define-fun eq ((lhs Edge) (rhs Edge)) (Bool)
  (and (not (cmp lhs rhs)) (not (cmp rhs lhs))))


;; some fresh variables
(declare-const e0 Edge)
(declare-const e1 Edge)
(declare-const e2 Edge)
(declare-const e3 Edge)
(declare-const e4 Edge)
(declare-const e5 Edge)
(declare-const e6 Edge)
(declare-const e7 Edge)
(declare-const e8 Edge)
(declare-const e9 Edge)
(declare-const e10 Edge)
(declare-const e11 Edge)
(declare-const e12 Edge)
(declare-const e13 Edge)
(declare-const e14 Edge)

;; strict weak ordering properties: irreflexivity, asymmetry, transitivity, incomparability
(assert (not (not (cmp e0 e0))))
(assert (not (implies (cmp e1 e2) (not (cmp e2 e1)))))
(assert (not (implies (and (cmp e3 e4) (cmp e4 e5)) (cmp e3 e5))))
(assert (not (implies (and (not (cmp e6 e7)) (not (cmp e7 e6)) (not (cmp e7 e8)) (not (cmp e8 e7))) (and (not (cmp e6 e8)) (not (cmp e8 e6))))))

;; equivalence relationship properties: reflexitivity, symmetry, transitivity
(assert (not (eq e9 e9)))
(assert (not (implies (eq e10 e11) (eq e11 e10))))
(assert (not (implies (and (eq e12 e13) (eq e13 e14)) (eq e12 e14))))

(check-sat)
;; unsat