Skip to content

Instantly share code, notes, and snippets.

@jonnybest
Created October 23, 2012 06:30
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jonnybest/3937226 to your computer and use it in GitHub Desktop.
Save jonnybest/3937226 to your computer and use it in GitHub Desktop.
A simple Alloy problem with Counterexample with translation to SMT2 (to be used at (http://stackoverflow.com/questions/13025127/getting-sat-for-large-problems)
sig A {}
sig B {
fn : A -> lone B
}
fact {
no (A ->fn->A)
}
assert notempty {
some B
}
check notempty for 10
(set-logic AUFLIA)
(set-option :macro-finder true)
;; sorts
(declare-sort Atom)
(declare-sort Rel1)
(declare-sort Rel2)
(declare-sort Rel3)
(declare-sort Rel4)
(declare-sort Rel5)
;; --end sorts
;; functions
(declare-fun fn () Rel3)
(declare-fun in_1 (Atom Rel1) Bool)
(declare-fun in_2 (Atom Atom Rel2) Bool)
(declare-fun prod_1x1 (Rel1 Rel1) Rel2)
(declare-fun in_3 (Atom Atom Atom Rel3) Bool)
(declare-fun prod_2x1 (Rel2 Rel1) Rel3)
(declare-fun subset_3 (Rel3 Rel3) Bool)
(declare-fun subset_2 (Rel2 Rel2) Bool)
(declare-fun join_1x3 (Rel1 Rel3) Rel2)
(declare-fun a2r_1 (Atom) Rel1)
(declare-fun lone_1 (Rel1) Bool)
(declare-fun join_1x2 (Rel1 Rel2) Rel1)
(declare-fun disjoint_1 (Rel1 Rel1) Bool)
(declare-fun in_4 (Atom Atom Atom Atom Rel4) Bool)
(declare-fun prod_3x1 (Rel3 Rel1) Rel4)
(declare-fun in_5 (Atom Atom Atom Atom Atom Rel5) Bool)
(declare-fun prod_1x4 (Rel1 Rel4) Rel5)
(declare-fun no_5 (Rel5) Bool)
(declare-fun some_1 (Rel1) Bool)
(declare-fun B () Rel1)
(declare-fun A () Rel1)
;; --end functions
;; axioms
(assert
(!
(forall ((A Rel1)(B Rel1)(x0 Atom)(y0 Atom)) (= (in_2 x0 y0 (prod_1x1 A B)) (and (in_1 x0 A) (in_1 y0 B))))
:named ax0
)
)
(assert
(!
(forall ((A Rel2)(B Rel1)(x0 Atom)(x1 Atom)(y0 Atom)) (= (in_3 x0 x1 y0 (prod_2x1 A B)) (and (in_2 x0 x1 A) (in_1 y0 B))))
:named ax1
)
)
(assert
(!
; subset axiom for Rel3
(forall ((x Rel3)(y Rel3)) (= (subset_3 x y) (forall ((a0 Atom)(a1 Atom)(a2 Atom)) (=> (in_3 a0 a1 a2 x) (in_3 a0 a1 a2 y)))))
:named ax2
)
)
(assert
(!
; subset axiom for Rel2
(forall ((x Rel2)(y Rel2)) (= (subset_2 x y) (forall ((a0 Atom)(a1 Atom)) (=> (in_2 a0 a1 x) (in_2 a0 a1 y)))))
:named ax3
)
)
(assert
(!
; axiom for join_1x3
(forall ((A Rel1)(B Rel3)(y0 Atom)(y1 Atom)) (= (in_2 y0 y1 (join_1x3 A B)) (exists ((x Atom)) (and (in_1 x A) (in_3 x y0 y1 B)))))
:named ax4
)
)
(assert
(!
; axiom for the conversion function Atom -> Relation
(forall ((x0 Atom)) (and (in_1 x0 (a2r_1 x0)) (forall ((y0 Atom)) (=> (in_1 y0 (a2r_1 x0)) (= x0 y0)))))
:named ax5
)
)
(assert
(!
(forall ((X Rel1)) (= (lone_1 X) (forall ((a0 Atom)(b0 Atom)) (=> (and (in_1 a0 X) (in_1 b0 X)) (= a0 b0)))))
:named ax6
)
)
(assert
(!
; axiom for join_1x2
(forall ((A Rel1)(B Rel2)(y0 Atom)) (= (in_1 y0 (join_1x2 A B)) (exists ((x Atom)) (and (in_1 x A) (in_2 x y0 B)))))
:named ax7
)
)
(assert
(!
; (forall ((A Rel1)(B Rel1)) (= (disjoint_1 A B) (forall ((a0 Atom)) (=> (in_1 a0 A) (not (in_1 a0 B)))))); alternative
(forall ((A Rel1)(B Rel1)) (= (disjoint_1 A B) (forall ((a0 Atom)) (not (and (in_1 a0 A) (in_1 a0 B))))))
:named ax8
)
)
(assert
(!
(forall ((A Rel3)(B Rel1)(x0 Atom)(x1 Atom)(x2 Atom)(y0 Atom)) (= (in_4 x0 x1 x2 y0 (prod_3x1 A B)) (and (in_3 x0 x1 x2 A) (in_1 y0 B))))
:named ax9
)
)
(assert
(!
(forall ((A Rel1)(B Rel4)(x0 Atom)(y0 Atom)(y1 Atom)(y2 Atom)(y3 Atom)) (= (in_5 x0 y0 y1 y2 y3 (prod_1x4 A B)) (and (in_1 x0 A) (in_4 y0 y1 y2 y3 B))))
:named ax10
)
)
(assert
(!
; axiom for 'the expression is empty'
(forall ((a0 Atom)(a1 Atom)(a2 Atom)(a3 Atom)(a4 Atom)(R Rel5)) (=> (no_5 R) (not (in_5 a0 a1 a2 a3 a4 R))))
:named ax11
)
)
(assert
(!
(forall ((A Rel1)) (= (some_1 A) (exists ((a0 Atom)) (in_1 a0 A))))
:named ax12
)
)
;; --end axioms
;; assertions
(assert
(!
(subset_3 fn (prod_2x1 (prod_1x1 B A) B))
:named a0
)
)
(assert
(!
(forall ((this Atom)) (=> (in_1 this B) (forall ((x0 Atom)) (=> (in_1 x0 A) (lone_1 (join_1x2 (a2r_1 x0) (join_1x3 (a2r_1 this) fn)))))))
:named a1
)
)
(assert
(!
(disjoint_1 B A)
:named a2
)
)
(assert
(!
(no_5 (prod_1x4 A (prod_3x1 fn A)))
:named a3
)
)
;; --end assertions
;; command
(assert
(!
(not (some_1 B))
:named c0
)
)
;; --end command
;; lemmas
(assert
(!
; 1. lemma for join_1x3. direction: join to in
(forall ((a2 Atom)(a1 Atom)(a0 Atom)(r Rel3)) (=> (in_2 a1 a0 (join_1x3 ; (swapped)
(a2r_1 a2) r)) (in_3 a2 a1 a0 r)))
:named l0
)
)
(assert
(!
; 2. lemma for join_1x3. direction: in to join
(forall ((a2 Atom)(a1 Atom)(a0 Atom)(r Rel3)) (=> (in_3 a2 a1 a0 r) (in_2 a1 a0 (join_1x3 ; (swapped)
(a2r_1 a2) r))))
:named l1
)
)
(assert
(!
; 1. lemma for join_1x2. direction: join to in
(forall ((a1 Atom)(a0 Atom)(r Rel2)) (=> (in_1 a0 (join_1x2 ; (swapped)
(a2r_1 a1) r)) (in_2 a1 a0 r)))
:named l2
)
)
(assert
(!
; 2. lemma for join_1x2. direction: in to join
(forall ((a1 Atom)(a0 Atom)(r Rel2)) (=> (in_2 a1 a0 r) (in_1 a0 (join_1x2 ; (swapped)
(a2r_1 a1) r))))
:named l3
)
)
;; --end lemmas
(check-sat)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment