Relational Reasoning via SMT Solving, Encode Alloy example, Filesystem in Z3
ferhaterata opened this issue · 8 comments
ferhaterata commented
Encode FileSystem Abstraction in Alloy and SMTLIB (using Z3) based on the rules defined in the following papers:
Relational Reasoning via SMT Solving - paper.pdf
Relational Reasoning via SMT Solving - slide.pdf
ferhaterata commented
iremfidandan commented
iremfidandan commented
The following detects an unsat core:
https://rise4fun.com/Z3/6CslM
The same result is obtained using the following program that uses JAVA API of Z3:
The following code is the output of the above Java calls:
(declare-sort FSObject)
(declare-sort Name)
(declare-fun oneParent (FSObject) FSObject)
(declare-fun content (FSObject FSObject) Bool)
(declare-fun isFSObject (FSObject) Bool)
(declare-fun isDir (FSObject) Bool)
(declare-fun isFile (FSObject) Bool)
(declare-fun isLink (FSObject) Bool)
(declare-fun isRoot (FSObject) Bool)
(declare-fun isName (Name) Bool)
(declare-fun name (FSObject Name) Bool)
(declare-fun oneName (FSObject) Name)
(declare-fun link (FSObject FSObject) Bool)
(declare-fun oneLink (FSObject) FSObject)
(declare-fun trContent (Int FSObject FSObject) Bool)
(declare-fun trLink (Int FSObject FSObject) Bool)
(declare-fun link0 () FSObject)
(declare-fun file0 () FSObject)
(declare-fun root0 () FSObject)
(declare-fun name1 () Name)
(declare-fun name0 () Name)
(declare-fun axiom1 () Bool)
(declare-fun axiom2 () Bool)
(declare-fun axiom3 () Bool)
(declare-fun axiom4 () Bool)
(declare-fun axiom5 () Bool)
(declare-fun axiom6 () Bool)
(declare-fun axiom7 () Bool)
(declare-fun axiom8 () Bool)
(declare-fun axiom9 () Bool)
(assert (forall ((f FSObject) (g FSObject)) (=> (content f g) (= (oneParent g) f))))
(assert (forall ((f FSObject)) (=> (isDir f) (isFSObject f))))
(assert (forall ((f FSObject)) (=> (isFile f) (isFSObject f))))
(assert (forall ((f FSObject)) (=> (isLink f) (isFSObject f))))
(assert (forall ((f FSObject)) (or (isDir f) (isFile f) (isLink f))))
(assert (forall ((f FSObject)) (not (and (isDir f) (isFile f) (isLink f)))))
(assert (forall ((f FSObject)) (=> (isRoot f) (isDir f))))
(assert (exists ((f FSObject)) (isRoot f)))
(assert (forall ((f FSObject) (g FSObject)) (=> (and (isRoot f) (isRoot g)) (= f g))))
(assert (forall ((f FSObject) (n Name)) (=> (name f n) (and (isName n) (isFSObject f)))))
(assert (forall ((f FSObject) (n Name)) (=> (name f n) (= (oneName f) n))))
(assert (forall ((f FSObject)) (=> (isFSObject f) (name f (oneName f)))))
(assert (forall ((f FSObject) (g FSObject))
(=> (content f g) (and (isDir f) (isFSObject g)))))
(assert (forall ((f FSObject) (g FSObject))
(=> (link f g) (and (isLink f) (isFSObject g)))))
(assert (forall ((f FSObject) (g FSObject)) (=> (link f g) (= (oneLink f) g))))
(assert (forall ((f FSObject) (g FSObject)) (=> (isLink f) (link f (oneLink f)))))
(assert (forall ((i Int) (f FSObject) (g FSObject))
(=> (< i 1) (not (trContent i f g)))))
(assert (forall ((f FSObject) (g FSObject)) (= (trContent 1 f g) (content f g))))
(assert (forall ((i Int) (f FSObject) (g FSObject))
(let ((a!1 (exists ((h FSObject)) (and (trContent (- i 1) f h) (content h g)))))
(let ((a!2 (= (trContent i f g) (or (trContent (- i 1) f g) a!1))))
(=> (> i 1) a!2)))))
(assert (forall ((f FSObject))
(=> (isDir f) (not (exists ((i Int)) (trContent i f f))))))
(assert (forall ((i Int) (f FSObject) (g FSObject)) (=> (< i 1) (not (trLink i f g)))))
(assert (forall ((f FSObject) (g FSObject)) (= (trLink 1 f g) (link f g))))
(assert (forall ((i Int) (f FSObject) (g FSObject))
(let ((a!1 (exists ((h FSObject)) (and (trLink (- i 1) f h) (link h g)))))
(let ((a!2 (= (trLink i f g) (or (trLink (- i 1) f g) a!1))))
(=> (> i 1) a!2)))))
(assert (forall ((f FSObject)) (=> (isLink f) (not (exists ((i Int)) (trLink i f f))))))
(assert (forall ((f FSObject))
(=> (isRoot f) (not (exists ((g FSObject)) (content g f))))))
(assert (forall ((f FSObject) (g FSObject))
(let ((a!1 (and (exists ((h FSObject)) (and (content h f) (content h g)))
(not (= f g)))))
(=> a!1 (not (= (oneName f) (oneName g)))))))
(assert (distinct root0 file0 link0))
(assert (distinct name0 name1))
(assert (=> axiom1 (isRoot root0)))
(assert (=> axiom2 (isFile file0)))
(assert (=> axiom3 (isLink link0)))
(assert (=> axiom4 (name root0 name1)))
(assert (=> axiom5 (name file0 name0)))
(assert (=> axiom6 (name link0 name0)))
(assert (=> axiom7 (link link0 file0)))
(assert (=> axiom8 (content root0 file0)))
(assert (=> axiom9 (content root0 link0)))
-----------------------------------------
unsat
core:
axiom5
axiom6
axiom8
axiom9
ferhaterata commented
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(set-option :produce-unsat-cores true)
; partitions of the universe, disjoint sets
; no (Name & FSObject)
(declare-sort FSObject)
(declare-sort Name)
; Using below is more convenient; it also generates distict constraint
;(declare-datatypes () ((FSO dir_1 dir_2 dir_3 dir_4)))
;(declare-datatypes () ((Name n_0 n_1)))
; subtypes inherited from the root types
(declare-fun isFSObject (FSObject) Bool)
(declare-fun isDir (FSObject) Bool)
(declare-fun isFile (FSObject) Bool)
(declare-fun isLink (FSObject) Bool)
(declare-fun isRoot (FSObject) Bool)
(declare-fun isName (Name) Bool)
; definition of binary relations, that uses root types
(declare-fun oneParent (FSObject) FSObject)
(declare-fun content (FSObject FSObject) Bool)
(declare-fun name (FSObject Name) Bool)
(declare-fun oneName (FSObject) Name)
(declare-fun link (FSObject FSObject) Bool)
(declare-fun oneLink (FSObject) FSObject)
; acyclic relations requires the use of transitive closure
(declare-fun trContent (Int FSObject FSObject) Bool)
(declare-fun trLink (Int FSObject FSObject) Bool)
;content relation is injective
; all a,a′:A | all b:B | (a,b) in R and (a′,b) in R implies a = a'
(assert (forall ((f FSObject) (g FSObject)) (=> (content f g) (= (oneParent g) f))))
;TYPE SYSTEM begins
; Dir in FSObject
(assert (forall ((f FSObject)) (=> (isDir f) (isFSObject f))))
; File in FSObject
(assert (forall ((f FSObject)) (=> (isFile f) (isFSObject f))))
; Link in FSObject
(assert (forall ((f FSObject)) (=> (isLink f) (isFSObject f))))
; FSObject = Link + Dir + File
(assert (forall ((f FSObject)) (or (isDir f) (isFile f) (isLink f))))
; no (Link & Dir)
; no (Link & File)
; no (Dir & File)
(assert (forall ((f FSObject)) (not (and (isDir f) (isFile f) (isLink f)))))
;Root in Dir
(assert (forall ((f FSObject)) (=> (isRoot f) (isDir f))))
; one Root
; one r:Root | r in Root
(assert (exists ((f FSObject)) (isRoot f))) ;some Root (existence)
(assert (forall ((f FSObject) (g FSObject)) (=> (and (isRoot f) (isRoot g)) (= f g)))) ; (uniqueness)
; name in (FSObject -> Name)
(assert (forall ((f FSObject) (n Name)) (=> (name f n) (and (isName n) (isFSObject f)))))
; (all f: FSObject | one (f.name))
(assert (forall ((f FSObject) (n Name)) (=> (name f n) (= (oneName f) n))))
(assert (forall ((f FSObject)) (=> (isFSObject f) (name f (oneName f)))))
; content in (Dir -> FSObject)
(assert (forall ((f FSObject) (g FSObject)) (=> (content f g) (and (isDir f) (isFSObject g)))))
; link in (Link -> FSObject)
(assert (forall ((f FSObject) (g FSObject)) (=> (link f g) (and (isLink f) (isFSObject g)))))
; (all l: Link | one (l.link))
(assert (forall ((f FSObject) (g FSObject)) (=> (link f g) (= (oneLink f) g))))
(assert (forall ((f FSObject) (g FSObject)) (=> (isLink f) (link f (oneLink f)))))
(assert (forall ((i Int) (f FSObject) (g FSObject))
(=> (< i 1) (not (trContent i f g)))))
(assert (forall ((f FSObject) (g FSObject)) (= (trContent 1 f g) (content f g))))
(assert (forall ((i Int) (f FSObject) (g FSObject))
(let ((a!1 (exists ((h FSObject)) (and (trContent (- i 1) f h) (content h g)))))
(let ((a!2 (= (trContent i f g) (or (trContent (- i 1) f g) a!1))))
(=> (> i 1) a!2)))))
(assert (forall ((f FSObject))
(=> (isDir f) (not (exists ((i Int)) (trContent i f f))))))
(assert (forall ((i Int) (f FSObject) (g FSObject)) (=> (< i 1) (not (trLink i f g)))))
(assert (forall ((f FSObject) (g FSObject)) (= (trLink 1 f g) (link f g))))
(assert (forall ((i Int) (f FSObject) (g FSObject))
(let ((a!1 (exists ((h FSObject)) (and (trLink (- i 1) f h) (link h g)))))
(let ((a!2 (= (trLink i f g) (or (trLink (- i 1) f g) a!1))))
(=> (> i 1) a!2)))))
(assert (forall ((f FSObject)) (=> (isLink f) (not (exists ((i Int)) (trLink i f f))))))
(assert (forall ((f FSObject))
(=> (isRoot f) (not (exists ((g FSObject)) (content g f))))))
(assert (forall ((f FSObject) (g FSObject))
(let ((a!1 (and (exists ((h FSObject)) (and (content h f) (content h g)))
(not (= f g)))))
(=> a!1 (not (= (oneName f) (oneName g)))))))
; The partial instance
; (link0 + file0 + root0) in FSObject
(declare-const link0 FSObject)
(declare-const file0 FSObject)
(declare-const root0 FSObject)
(assert (distinct root0 file0 link0))
(declare-const name1 Name)
(declare-const name0 Name)
(assert (distinct name0 name1))
(assert (!(isRoot root0) :named axiom1))
(assert (!(isFile file0) :named axiom2))
(assert (!(isLink link0) :named axiom3))
(assert (!(name root0 name1) :named axiom4))
(assert (!(name file0 name0) :named axiom5))
(assert (!(name link0 name0) :named axiom6))
(assert (!(link link0 file0) :named axiom7))
(assert (!(content root0 file0) :named axiom8))
(assert (!(content root0 link0) :named axiom9))
(check-sat)
(get-unsat-core)
iremfidandan commented
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(set-option :produce-unsat-cores true)
; partitions of the universe, disjoint sets
; topmost EClass at the type hierarchy, this corresponds to top-level signatures in Alloy
; no (Name & FSObject)
(declare-sort FSObject)
(declare-sort Name)
; Using below is more convenient; it also generates distict constraint
;(declare-datatypes () ((FSO dir_1 dir_2 dir_3 dir_4)))
;(declare-datatypes () ((Name n_0 n_1)))
; subtypes inherited from the root types
(declare-fun isFSObject (FSObject) Bool)
(declare-fun isDir (FSObject) Bool)
(declare-fun isFile (FSObject) Bool)
(declare-fun isLink (FSObject) Bool)
(declare-fun isRoot (FSObject) Bool)
(declare-fun isName (Name) Bool)
; definition of binary relations, that uses root types
(declare-fun oneParent (FSObject) FSObject)
(declare-fun content (FSObject FSObject) Bool)
(declare-fun name (FSObject Name) Bool)
(declare-fun oneName (FSObject) Name)
(declare-fun link (FSObject FSObject) Bool)
(declare-fun oneLink (FSObject) FSObject)
; acyclic relations requires the use of transitive closure
(declare-fun trContent (Int FSObject FSObject) Bool)
(declare-fun trLink (Int FSObject FSObject) Bool)
;content relation is injective
; all a,a′:A | all b:B | (a,b) in R and (a′,b) in R implies a = a'
(assert (forall ((f FSObject) (g FSObject)) (=> (content f g) (= (oneParent g) f))))
;TYPE SYSTEM begins
; Dir in FSObject
(assert (forall ((f FSObject)) (=> (isDir f) (isFSObject f))))
; File in FSObject
(assert (forall ((f FSObject)) (=> (isFile f) (isFSObject f))))
; Link in FSObject
(assert (forall ((f FSObject)) (=> (isLink f) (isFSObject f))))
; FSObject = Link + Dir + File
(assert (forall ((f FSObject)) (or (isDir f) (isFile f) (isLink f))))
; no (Link & Dir)
; no (Link & File)
; no (Dir & File)
(assert (forall ((f FSObject)) (not (and (isDir f) (isFile f)))))
(assert (forall ((f FSObject)) (not (and (isDir f) (isLink f)))))
(assert (forall ((f FSObject)) (not (and (isFile f) (isLink f)))))
;Root in Dir
(assert (forall ((f FSObject)) (=> (isRoot f) (isDir f))))
; one Root
; one r:Root | r in Root
(assert (exists ((f FSObject)) (isRoot f))) ;some Root (existence)
(assert (forall ((f FSObject) (g FSObject)) (=> (and (isRoot f) (isRoot g)) (= f g)))) ; (uniqueness)
; name in (FSObject -> Name)
(assert (forall ((f FSObject) (n Name)) (=> (name f n) (and (isName n) (isFSObject f)))))
; (all f: FSObject | one (f.name))
(assert (forall ((f FSObject) (n Name)) (=> (name f n) (= (oneName f) n))))
(assert (forall ((f FSObject)) (=> (isFSObject f) (name f (oneName f)))))
; content in (Dir -> FSObject)
(assert (forall ((f FSObject) (g FSObject)) (=> (content f g) (and (isDir f) (isFSObject g)))))
; link in (Link -> FSObject)
(assert (forall ((f FSObject) (g FSObject)) (=> (link f g) (and (isLink f) (isFSObject g)))))
; (all l: Link | one (l.link))
(assert (forall ((f FSObject) (g FSObject)) (=> (link f g) (= (oneLink f) g))))
(assert (forall ((f FSObject) (g FSObject)) (=> (isLink f) (link f (oneLink f)))))
(assert (forall ((i Int) (f FSObject) (g FSObject))
(=> (< i 1) (not (trContent i f g)))))
(assert (forall ((f FSObject) (g FSObject)) (= (trContent 1 f g) (content f g))))
(assert (forall ((i Int) (f FSObject) (g FSObject))
(let ((a!1 (exists ((h FSObject)) (and (trContent (- i 1) f h) (content h g)))))
(let ((a!2 (= (trContent i f g) (or (trContent (- i 1) f g) a!1))))
(=> (> i 1) a!2)))))
(assert (forall ((f FSObject))
(=> (isDir f) (not (exists ((i Int)) (trContent i f f))))))
(assert (forall ((i Int) (f FSObject) (g FSObject)) (=> (< i 1) (not (trLink i f g)))))
(assert (forall ((f FSObject) (g FSObject)) (= (trLink 1 f g) (link f g))))
(assert (forall ((i Int) (f FSObject) (g FSObject))
(let ((a!1 (exists ((h FSObject)) (and (trLink (- i 1) f h) (link h g)))))
(let ((a!2 (= (trLink i f g) (or (trLink (- i 1) f g) a!1))))
(=> (> i 1) a!2)))))
(assert (forall ((f FSObject)) (=> (isLink f) (not (exists ((i Int)) (trLink i f f))))))
(assert (forall ((f FSObject))
(=> (isRoot f) (not (exists ((g FSObject)) (content g f))))))
(assert (forall ((f FSObject) (g FSObject))
(let ((a!1 (and (exists ((h FSObject)) (and (content h f) (content h g)))
(not (= f g)))))
(=> a!1 (not (= (oneName f) (oneName g)))))))
; The partial instance
; (link0 + file0 + root0) in FSObject
(declare-const link0 FSObject)
(declare-const file0 FSObject)
(declare-const root0 FSObject)
(assert (distinct root0 file0 link0))
(declare-const name1 Name)
(declare-const name0 Name)
(assert (distinct name0 name1))
(assert (!(isRoot root0) :named axiom1))
(assert (!(isFile file0) :named axiom2))
(assert (!(isLink link0) :named axiom3))
(assert (!(name root0 name1) :named axiom4))
(assert (!(name file0 name0) :named axiom5))
(assert (!(name link0 name0) :named axiom6))
(assert (!(link link0 file0) :named axiom7))
(assert (!(content root0 file0) :named axiom8))
(assert (!(content root0 link0) :named axiom9))
(check-sat)
(get-unsat-core)
iremfidandan commented
ferhaterata commented
https://rise4fun.com/Z3/NEu?frame=1&menu=0&course=1
(set-option :smt.mbqi true)
(set-option :model.compact true)
;(set-logic UF)
(declare-datatypes () ((FSObject File227 Root133 FSObject_2)))
(declare-datatypes () ((Name Name79 Name94)))
;(declare-sort FSObject)
;(declare-sort Name)
(declare-fun content (FSObject FSObject) Bool)
(declare-fun name (FSObject Name) Bool)
(declare-fun isFSObject (FSObject) Bool)
(declare-fun isName (Name) Bool)
(declare-fun isDir (FSObject) Bool)
(declare-fun isFile (FSObject) Bool)
(declare-fun isRoot (FSObject) Bool)
;(declare-fun FSObject_2 () FSObject)
;(declare-fun File227 () FSObject)
;(declare-fun Root133 () FSObject)
;(declare-fun Name79 () Name)
;(declare-fun Name94 () Name)
(assert (forall ((f!1 FSObject) (f!2 FSObject) (f!3 FSObject))
(=> (and (content f!1 f!3) (content f!2 f!3)) (= f!1 f!2))))
(assert (forall ((f FSObject) (n!1 Name) (n!2 Name))
(=> (and (name f n!1) (name f n!2)) (= n!1 n!2))))
;(assert (forall ((f FSObject)) (isFSObject f)))
;(assert (forall ((n Name)) (isName n)))
(assert (forall ((f FSObject)) (=> (isDir f) (isFSObject f))))
(assert (forall ((f FSObject)) (=> (isFile f) (isFSObject f))))
(assert (forall ((f FSObject)) (or (isDir f) (isFile f))))
(assert (forall ((f FSObject)) (not (and (isDir f) (isFile f)))))
(assert (forall ((f FSObject)) (=> (isRoot f) (isDir f))))
(assert (exists ((f FSObject)) (isRoot f)))
(assert (forall ((f!1 FSObject) (f!2 FSObject))
(=> (and (isRoot f!1) (isRoot f!2)) (= f!1 f!2))))
;(assert (forall ((f FSObject)) (=> (isFSObject f) (exists ((n Name)) (name f n)))))
(assert (forall ((f FSObject)) (exists ((n Name)) (name f n))))
(assert (forall ((f FSObject) (n Name)) (=> (name f n) (and (isName n) (isFSObject f)))))
(assert (forall ((f!1 FSObject) (f!2 FSObject))
(=> (content f!1 f!2) (and (isDir f!1) (isFSObject f!2)))))
(assert (forall ((f!1 FSObject))
(=> (not (isRoot f!1))
(exists ((f!2 FSObject)) (and (isDir f!2) (content f!2 f!1))))))
(assert (forall ((f!1 FSObject))
(= (isRoot f!1) (not (exists ((f!2 FSObject)) (content f!2 f!1))))))
(assert (distinct Root133 File227 FSObject_2))
;(assert (distinct Name94 Name79))
(assert (isRoot Root133))
(assert (isDir Root133))
(assert (isFile File227))
(assert (isFSObject FSObject_2))
(assert (isFSObject Root133))
(assert (isFSObject File227))
(assert (name Root133 Name79))
(assert (name File227 Name79))
(assert (content Root133 File227))
(assert (or (name Root133 Name94)
(name Root133 Name79)
(name File227 Name94)
(name File227 Name79)
(name FSObject_2 Name94)
(name FSObject_2 Name79)))
(assert (or (content Root133 Root133)
(content Root133 File227)
(content Root133 FSObject_2)
(content FSObject_2 Root133)
(content FSObject_2 File227)
(content FSObject_2 FSObject_2)))
(check-sat)
(echo "(isFile FSObject_2)")
(eval (isFile FSObject_2))
(echo "(isDir FSObject_2)")
(eval (isDir FSObject_2))
(echo "(isRoot FSObject_2)")
(eval (isRoot FSObject_2))
(echo "(isFSObject FSObject_2)")
(eval (isFSObject FSObject_2))
(echo "(name Root133 Name94)")
(eval (name Root133 Name94))
(echo "(name Root133 Name79)")
(eval (name Root133 Name79))
(echo "(name File227 Name94)")
(eval (name File227 Name94))
(echo "(name File227 Name79)")
(eval (name File227 Name79))
(echo "(name FSObject_2 Name94)")
(eval (name FSObject_2 Name94))
(echo "(name FSObject_2 Name79)")
(eval (name FSObject_2 Name79))
(echo "(content Root133 Root133)")
(eval (content Root133 Root133))
(echo "(content Root133 File227)")
(eval (content Root133 File227))
(echo "(content Root133 FSObject_2)")
(eval (content Root133 FSObject_2))
(echo "(content FSObject_2 Root133)")
(eval (content FSObject_2 Root133))
(echo "(content FSObject_2 File227)")
(eval (content FSObject_2 File227))
(echo "(content FSObject_2 FSObject_2)")
(eval (content FSObject_2 FSObject_2))
(get-model)
ferhaterata commented
(set-option :smt.mbqi true)
(set-option :model.compact true)
;(set-logic UF)
(declare-datatypes () ((FSObject File227 Root133 FSObject_2)))
(declare-datatypes () ((Name Name79 Name94)))
(declare-fun content (FSObject FSObject) Bool)
(declare-fun name (FSObject Name) Bool)
(declare-fun isFSObject (FSObject) Bool)
(declare-fun isDir (FSObject) Bool)
(declare-fun isFile (FSObject) Bool)
(declare-fun isRoot (FSObject) Bool)
(declare-fun isName (Name) Bool)
(assert (forall ((f!1 FSObject) (f!2 FSObject) (f!3 FSObject))
(=> (and (content f!1 f!3) (content f!2 f!3)) (= f!1 f!2))))
(assert (forall ((f FSObject) (n!1 Name) (n!2 Name))
(=> (and (name f n!1) (name f n!2)) (= n!1 n!2))))
(assert (forall ((f FSObject)) (=> (isDir f) (isFSObject f))))
(assert (forall ((f FSObject)) (=> (isFile f) (isFSObject f))))
(assert (forall ((f FSObject)) (or (isDir f) (isFile f))))
(assert (forall ((f FSObject)) (not (and (isDir f) (isFile f)))))
(assert (forall ((f FSObject)) (=> (isRoot f) (isDir f))))
(assert (exists ((f FSObject)) (isRoot f)))
(assert (forall ((f!1 FSObject) (f!2 FSObject))
(=> (and (isRoot f!1) (isRoot f!2)) (= f!1 f!2))))
(assert (forall ((f FSObject)) (=> (isFSObject f) (exists ((n Name)) (name f n)))))
(assert (forall ((f FSObject) (n Name)) (=> (name f n) (and (isName n) (isFSObject f)))))
(assert (forall ((f!1 FSObject) (f!2 FSObject))
(=> (content f!1 f!2) (and (isDir f!1) (isFSObject f!2)))))
(assert (forall ((f!1 FSObject))
(=> (not (isRoot f!1))
(exists ((f!2 FSObject)) (and (isDir f!2) (content f!2 f!1))))))
(assert (forall ((f!1 FSObject))
(= (isRoot f!1) (not (exists ((f!2 FSObject)) (content f!2 f!1))))))
(assert (forall ((f!1 FSObject) (f!2 FSObject))
(let ((a!1 (exists ((f!3 FSObject))
(let ((a!1 (not (exists ((n Name)) (= (name f!1 n) (name f!2 n))))))
(=> (= (content f!3 f!1) (content f!3 f!2)) a!1)))))
(=> (not (= f!1 f!2)) a!1))))
(assert (forall ((f!1 FSObject) (f!2 FSObject))
(=> (content f!1 f!2) (not (= f!1 f!2)))))
(assert (isRoot Root133))
(assert (isDir Root133))
(assert (isFile File227))
(assert (isFSObject FSObject_2))
(assert (isFSObject Root133))
(assert (isFSObject File227))
(assert (name Root133 Name79))
(assert (name File227 Name79))
(assert (content Root133 File227))
(assert (or (name Root133 Name94)
(name Root133 Name79)
(name File227 Name94)
(name File227 Name79)
(name FSObject_2 Name94)
(name FSObject_2 Name79)))
(assert (or (content Root133 Root133)
(content Root133 File227)
(content Root133 FSObject_2)
(content FSObject_2 Root133)
(content FSObject_2 File227)
(content FSObject_2 FSObject_2)))
(check-sat)
(echo "(isFile FSObject_2)")
(eval (isFile FSObject_2))
(echo "(isDir FSObject_2)")
(eval (isDir FSObject_2))
(echo "(isRoot FSObject_2)")
(eval (isRoot FSObject_2))
(echo "(isFSObject FSObject_2)")
(eval (isFSObject FSObject_2))
(echo "(name Root133 Name94)")
(eval (name Root133 Name94))
(echo "(name Root133 Name79)")
(eval (name Root133 Name79))
(echo "(name File227 Name94)")
(eval (name File227 Name94))
(echo "(name File227 Name79)")
(eval (name File227 Name79))
(echo "(name FSObject_2 Name94)")
(eval (name FSObject_2 Name94))
(echo "(name FSObject_2 Name79)")
(eval (name FSObject_2 Name79))
(echo "(content Root133 Root133)")
(eval (content Root133 Root133))
(echo "(content Root133 File227)")
(eval (content Root133 File227))
(echo "(content Root133 FSObject_2)")
(eval (content Root133 FSObject_2))
(echo "(content FSObject_2 Root133)")
(eval (content FSObject_2 Root133))
(echo "(content FSObject_2 File227)")
(eval (content FSObject_2 File227))
(echo "(content FSObject_2 FSObject_2)")
(eval (content FSObject_2 FSObject_2))
(get-model)