Created
October 24, 2012 11:59
-
-
Save jonnybest/3945693 to your computer and use it in GitHub Desktop.
Revisions
-
jbxf created this gist
Oct 24, 2012 .There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -0,0 +1,68 @@ (set-option :macro-finder true) (set-option :ematching true) (set-option :mbqi false) ;; sorts (declare-sort Atom) (declare-sort Rel1) (declare-sort Rel2) (declare-sort Rel3) ;; --end sorts ;; functions (declare-const 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-const A Rel1) (declare-const B 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 ) ) (check-sat) (get-model) This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -0,0 +1,68 @@ (set-option :macro-finder true) (set-option :ematching false) (set-option :mbqi true) ;; sorts (declare-sort Atom) (declare-sort Rel1) (declare-sort Rel2) (declare-sort Rel3) ;; --end sorts ;; functions (declare-const 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-const A Rel1) (declare-const B 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 ) ) (check-sat) (get-model) This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -0,0 +1,61 @@ (set-option :macro-finder true) (set-option :ematching false) (set-option :mbqi true) ;; sorts (declare-sort Atom) (declare-sort Rel1) (declare-sort Rel2) (declare-sort Rel3) ;; --end sorts ;; functions (declare-const 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-const A Rel1) (declare-const B 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 ) ) (check-sat) (get-model)
jbxf
created
this gist