Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Relational Reasoning via SMT Solving, Encode Alloy example, Filesystem in Z3 #96

Open
ferhaterata opened this issue May 26, 2017 · 8 comments
Open

Relational Reasoning via SMT Solving, Encode Alloy example, Filesystem in Z3 #96

ferhaterata opened this issue May 26, 2017 · 8 comments
Assignees
@ferhaterata @iremfidandan
Labels
Alloy completed SMT Translation

Comments

@ferhaterata
Copy link
Member

ferhaterata commented May 26, 2017 •
edited

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

@harunuyar
@ferhaterata ferhaterata changed the title Relational Reasoning visa SMT Solving Relational Reasoning via SMT Solving May 26, 2017
@ferhaterata ferhaterata mentioned this issue May 26, 2017
Open
@ferhaterata ferhaterata mentioned this issue May 29, 2017
Open
@ferhaterata ferhaterata self-assigned this May 29, 2017
This was referenced May 29, 2017
Open
Open
@ferhaterata
Copy link
Member Author

http://rise4fun.com/Z3/77sld

@iremfidandan
Copy link
Member

https://rise4fun.com/Z3/LS7

@iremfidandan
Copy link
Member

iremfidandan commented Dec 18, 2017 •
edited

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:

https://github.com/ModelWriter/z3/blob/4f89ab31cfc8c3221a850cf7c4d641b160aa838c/src/eu/modelwriter/Z3JavaInterfaceDemo/Main.java

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 ferhaterata changed the title Relational Reasoning via SMT Solving Relational Reasoning via SMT Solving, Encode Alloy example, Filesystem in Z3 Dec 19, 2017
@ferhaterata
Copy link
Member Author

ferhaterata commented Dec 19, 2017 •
edited

https://rise4fun.com/Z3/ipl7T

(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
Copy link
Member

iremfidandan commented Dec 20, 2017 •
edited by ferhaterata

https://rise4fun.com/Z3/pJJg

(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
Copy link
Member

https://rise4fun.com/Z3/pA7

@ferhaterata
Copy link
Member Author

ferhaterata commented Dec 28, 2017 •
edited

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
Copy link
Member Author

https://rise4fun.com/Z3/Eie

(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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ferhaterata ferhaterata

@iremfidandan iremfidandan

Labels
Alloy completed SMT Translation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@ferhaterata @iremfidandan