mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
32 lines
827 B
Text
32 lines
827 B
Text
(set-logic QF_UF)
|
|
(set-info :source |
|
|
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
|
|
Ofer Strichman and Mirron Rozanov,
|
|
SMT Workshop 2005.
|
|
|
|
Translator: Leonardo de Moura. |)
|
|
(set-info :smt-lib-version 2.0)
|
|
(set-info :category "crafted")
|
|
(set-info :status unsat)
|
|
(declare-sort U 0)
|
|
(declare-fun x0 () U)
|
|
(declare-fun y0 () U)
|
|
(declare-fun z0 () U)
|
|
(declare-fun x1 () U)
|
|
(declare-fun y1 () U)
|
|
(declare-fun z1 () U)
|
|
(declare-fun x2 () U)
|
|
(declare-fun y2 () U)
|
|
(declare-fun z2 () U)
|
|
(declare-fun x3 () U)
|
|
(declare-fun y3 () U)
|
|
(declare-fun z3 () U)
|
|
(assert
|
|
(and
|
|
(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
|
|
(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
|
|
(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
|
|
(not (= x0 x3))))
|
|
(check-sat)
|
|
(exit)
|
|
; :status unsat
|