C#でもUbuntu+Docker+Jenkins+GitBucket+MonoでCIしたい（環境構築編）
はじめに
今回はLinuxサーバ環境で半ば無理やりCI環境を構築して.NETプラットフォームのアプリケーションをCIするという誰が得をするのだろうという内容の話です。
具体的に言うと、GitBucketでソースコードをホストして、GitBucketにプッシュされたときにJenkinsでビルド+テスト実行を行うというごくありふれた内容です。 こいつらをDocker上に構築します。
+-------------------+ +-------------------+
| GitBucket | -- (2)web hook --> | Jenkins |-----
-->| 192.168.0.10:8080 | | 192.168.0.10:8090 | |
| +-------------------+ ---------- +-------------------+<-- |
| | | |
| (1)push | (4)pull | | (3)order
| | (6)return result | |
| | | |
| +-------------------+ | +-------------------+ | |
---| Windows Client | --------->| Jenkins Slave |--- |
+-------------------+ | 192.168.0.10:9000 | |
+-------------------+<----
(5)build & test
余談ですが、最初はいつも通り『VB.NETでも〜』という内容にしようと思ったのですが、xbuildがvbprojをどうしてもビルドしたくないと言うので急遽C#殿にお越しいただきました。
環境
とりあえず以下の環境を使用しました。
- Ubuntu 16.04
- Docker 1.12.1
- docker-compose 1.8.1
- Jenkins 2.19.1
- GitBucket 4.5.0
- Mono 4.6.1
- Visual Studio 2015 Community update 3
- .NET Framework 4.5.2
- ReSharper 2016.02
- NUnit 3.5.0
- Nuit.ConsoleRunner 3.4.1
セットアップ
Docker・docker-compose
公式マニュアルを以下略。
Jenkins・GitBucket・Jenkinsビルドスレーブ環境構築
まずはGitBuckt環境を構築しましょう。
こちらは特に変わったことはしてません。openjdk-8-jre-alpineをベースにGitBucketのバイナリをダウンロードして実行しているだけです。
FROM java:openjdk-8-jre-alpine ADD https://github.com/gitbucket/gitbucket/releases/download/4.5/gitbucket.war /opt/gitbucket/gitbucket.war VOLUME /srv/gitbucket EXPOSE 8080 CMD ["java", "-jar", "/opt/gitbucket/gitbucket.war", "--gitbucket.home=/srv/gitbucket"]
Jenkinsは公式イメージを使用しています。
ただ、公式イメージにはMonoの環境が入っておらず、途中でユーザを切り替えてるせいで公式イメージをベースにMono環境を追加するという手法も使えなかったので、別途Monoをインストールしたコンテナをスレーブとして使用しています。（クソポイントその１）
ubuntu:16.04をベースにビルド及びテスト実行のためのMono、Jenkinsスレーブデーモンを動かすためのJava、Jenkinsのスレーブとして動作させるためにDockerでは禁忌とされているSSHサーバをインストールしています。（クソポイントその２）
何処かで見たことがあると思ったあなた。素晴らしいです。先頭部分はbuildpack-deps:jessie-scmからパクって拝借してきました。
あとはNuGetにパッケージの復元を許可するためにEnableNuGetPackageRestoreをTRUEに設定しています。
FROM ubuntu:16.04
RUN apt-get update && apt-get install -y --no-install-recommends \
ca-certificates \
curl \
wget \
&& rm -rf /var/lib/apt/lists/*
RUN apt-get update && apt-get install -y --no-install-recommends \
bzr \
git \
mercurial \
openssh-client \
subversion \
\
procps \
&& rm -rf /var/lib/apt/lists/*
RUN set -x \
&& apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF \
&& echo "deb http://download.mono-project.com/repo/debian wheezy main" | tee /etc/apt/sources.list.d/mono-xamarin.list \
# && echo "deb http://download.mono-project.com/repo/debian wheezy-libjpeg62-compat main" | tee -a /etc/apt/sources.list.d/mono-xamarin.list \
&& echo "deb http://download.mono-project.com/repo/debian wheezy-apache24-compat main" | tee -a /etc/apt/sources.list.d/mono-xamarin.list \
&& apt-get update \
&& apt-get -y install mono-complete openjdk-8-jdk \
&& rm -rf /var/lib/apt/lists/*
RUN set -x \
&& apt-get update \
&& apt-get install -y openssh-server \
&& rm -rf /var/lib/apt/lists/*
RUN mkdir /var/run/sshd
RUN echo 'root:screencast' | chpasswd
RUN sed -i 's/PermitRootLogin prohibit-password/PermitRootLogin yes/' /etc/ssh/sshd_config
# SSH login fix. Otherwise user is kicked off after login
RUN sed 's@session\s*required\s*pam_loginuid.so@session optional pam_loginuid.so@g' -i /etc/pam.d/sshd
ENV NOTVISIBLE "in users profile"
RUN echo "export VISIBLE=now" >> /etc/profile
ENV EnableNuGetPackageRestore TRUE
EXPOSE 22
CMD ["/usr/sbin/sshd", "-D"]
あとはこれらのコンテナを上げたり下げたりビルドする為のdocker-compose.ymlをでっち上げれば構築は完了です。
version: '2'
services:
gitbucket-websrv:
build: './gitbucket'
ports:
- '8080:8080'
volumes:
- '/srv/mono-ci/gitbucket:/srv/gitbucket'
jenkins:
image: 'jenkins:2.19.1'
ports:
- '8090:8080'
- '50000:50000'
volumes:
- '/srv/mono-ci/jenkins:/var/jenkins_home'
jenkins-slave-mono:
build: './jenkins-slave-mono'
ports:
- '9000:22'
ちなみにこれらの環境を構築するだけなら10秒*1で終わります。
git clone https://github.com/jyuch/mono-ci.git cd mono-ci docker-compose up
Jenkins・GitBucket初期設定
GitBucket
GitBucketにroot:rootでログインし、自身の作業用アカウントとJenkins用のアカウントを作成しましょう。
Jenkinsアカウントはコントリビューターになれれば良いので管理者でなくても大丈夫です。
Jenkins
アカウント登録後のプラグイン選択画面ではとりあえずおすすめをインストールしておきましよう。
その後、管理画面より以下のプラグインをインストールします。
- GitBucket Plugin
- NUnit plugin
その後はJenkinsの管理 > ノードの管理よりスレーブノードを登録します。
今回の構成ですとSSHポートは9000なのでそこだけは注意が必要です。
最後にCSRF対策のチェックボックスを外します。セキュリティを切るのはいささか気が引けますがこの作業をしないとGitBucketからのweb hookが通らないのでまぁ仕方ないのかなと自分の中で折り合いを付けながらチェックボックスを外すか別のいい感じの方法を探して下さい。いい感じの方法がありましたら教えてください。
ここまでで初期セットアップは完了です。お疲れ様でした。
*1:イメージのプル・ビルド時間を除く
VB.NETでも制約ソルバーを用いて数独を解きたい その２
はじめに
前回は地獄のSMT-LIBコピペ祭りを経て、z3で数独を解くことに成功しました。 今回はVBから制約を発行してz3に数独を解かせてみましょう。
.NETバインディング
z3には.NETのバインディングが用意されており、P/Invoke祭りやCOM祭りをやらなくともz3の機能が利用できます。やったね
まぁ、CodeDOMからコードを生成するのによく似たつらみが待ち構えているので結局アレですけど。
z3のGitHubページからライブラリをダウンロードして、Microsoft.Z3.dllを参照に加えましょう。
また、Microsft.Z3.dllは単なるバインディングなので、libz3.dllも一緒にコピーしておく必要があります。
あと、libz3は（たぶん）ネイティブなので、ダウンロードしたアーキテクチャに合わせて.NETのアーキテクチャを合わせておく必要があります。 WOW64の加護により64bitOSでも32bitアプリケーションが動くので今回はx86を使用しています。 アプリケーションに割り当て可能なメモリ量の制約や若干のオーバーヘッドなどがありますが、今回は目をつぶりましょう。
余談ですが、x86のネイティブライブラリを使用しているプロジェクトで、Debugビルドはx86に直してあるのにReleaseはAnyCPUのままになっていてReleaseすると無事に64bitOSで死ぬみたいな間抜けな事があったので気を付けましょう。
数独
正直なことを申しますと、z3の公式サンプルに数独を解くコードがあるのでそちらを参考にしました。
Dim opt = New Dictionary(Of String, String) opt("proof") = "true" Using c = New Context(opt) Dim solver = c.MkSolver() Dim cells(8)() As IntExpr ' x_1_1 から x_9_9のシンボルを生成 For i = 0 To 8 Dim r(8) As IntExpr cells(i) = r For j = 0 To 8 cells(i)(j) = CType(c.MkConst(c.MkSymbol($"x_{i + 1}_{j + 1}"), c.IntSort), IntExpr) Next Next ' (assert (and (<= 1, x_?_?) (>= x_?_? 9))) For i = 0 To 8 For j = 0 To 8 solver.Assert( c.MkAnd( c.MkLe(c.MkInt(1), cells(i)(j)), c.MkLe(cells(i)(j), c.MkInt(9)))) Next Next ' (assert (distinct x_?_1 ... x_?_9)) For i = 0 To 8 solver.Assert(c.MkDistinct(cells(i))) Next ' (assert (distinct x_1_? ... x_9_?)) For j = 0 To 8 Dim col(8) As IntExpr For i = 0 To 8 col(i) = cells(i)(j) Next solver.Assert(c.MkDistinct(col)) Next ' (assert (distinct 3x3のあのマス)) For i0 = 0 To 2 For j0 = 0 To 2 Dim square(8) As IntExpr For i = 0 To 2 For j = 0 To 2 square(3 * i + j) = cells(3 * i0 + i)(3 * j0 + j) Next Next solver.Assert(c.MkDistinct(square)) Next Next Dim inst = { {0, 0, 5, 3, 0, 0, 0, 0, 0}, {8, 0, 0, 0, 0, 0, 0, 2, 0}, {0, 7, 0, 0, 1, 0, 5, 0, 0}, {4, 0, 0, 0, 0, 5, 3, 0, 0}, {0, 1, 0, 0, 7, 0, 0, 0, 6}, {0, 0, 3, 2, 0, 0, 0, 8, 0}, {0, 6, 0, 5, 0, 0, 0, 0, 9}, {0, 0, 4, 0, 0, 0, 0, 3, 0}, {0, 0, 0, 0, 0, 9, 7, 0, 0} } For i = 0 To 8 For j = 0 To 8 If inst(i, j) <> 0 Then solver.Assert(c.MkEq(c.MkInt(inst(i, j)), cells(i)(j))) End If Next Next If solver.Check() = Status.SATISFIABLE Then Dim m = solver.Model For Each i In cells For Each j In i Console.Write($"{m.Evaluate(j)} ") Next Console.WriteLine() Next Else Console.WriteLine("Failed to solve sudoku") End If End Using
おわりに
z3で数独を解くこと自体は前回の時点で出来てるので今回は特に感動もないのですが、まぁなるほどなといった感じです。 しかしまぁ、慣れは必要ですが問題を数式で表現さえ出来ればアルゴリズムを実装せずに解けるというのはかなり強力ですね。
公式サンプルではほとんどの制約を(and ...)で連結してAssertを2つにまで削減してました。
内部実装的にこうしたほうが早いというのがあるのかもしれませんが、今回は分かりやすさの為に条件一つ一つにAssertを適用しました。
おわり
VB.NETでも制約ソルバーを用いて数独を解きたい その１
はじめに
マイクロソフト・リサーチが開発しているz3定理証明器に興味を持ったのでそれについてです。
鶴亀算
まずはオンラインのコンソールで鶴亀算を解いてみましょう。
z3はSMT-LIB標準形式のバージョン2を解釈できるのでそれを用いて鶴亀算の各制約を記述します。 なお、SMT-LIBはS式で記述するみたいです。 LispやSchemeを使ったことがある人ならおなじみでしょう。 おなじんでないひとは・・・がんばってください。
;; シンボルの定義 (declare-const kame Int) (declare-const tsuru Int) ;; 制約を表現 (assert (= 8 (+ kame tsuru))) (assert (= 26 (+ (* kame 4) (* tsuru 2)))) ;; 検証 (check-sat) ;; 結果の取得 (get-model)
sat (model (define-fun tsuru () Int 3) (define-fun kame () Int 5) )
数独
なんとなくで鶴亀算を解いたので、次はノリと勢いで数独を解いて行きましょう。
まずは各要素は1から9の間という制約を表現してみます。
(declare-const x_1_1 Int) (assert (and (<= 1 x_1_1) (>= 9 x_1_1))) (push) ;; --------------------------- (assert (= x_1_1 1)) (check-sat) ;; --------------------------- (pop) (push) ;; --------------------------- (assert (= x_1_1 9)) (check-sat) ;; --------------------------- (pop) (push) ;; --------------------------- (assert (= x_1_1 10)) (check-sat) ;; ---------------------------
S式がなんとなくとっつきにくいかもしれませんが、やってるのは普通の条件式ですね。
sat sat unsat
ちなみに(pop)と(push)はその時点でのコンテキストをスタックへプッシュ・ポップする命令です。
3行目の(push)だったら(declare-const x_1_1 Int)と(assert (and (<= 0 x_1_1) (>= 9 x_1_1)))が評価された状態がスタックにプッシュされます。
次に各要素が異なるという制約を表現します。異なるという制約はdistinct演算子を使用します。
(declare-const x_1_1 Int) (declare-const x_1_2 Int) (declare-const x_1_3 Int) (assert (distinct x_1_1 x_1_2 x_1_3)) (push) ;; --------------------------- (assert (= x_1_1 1)) (assert (= x_1_2 2)) (assert (= x_1_3 3)) (check-sat) ;; --------------------------- (pop) (push) ;; --------------------------- (assert (= x_1_1 1)) (assert (= x_1_2 2)) (assert (= x_1_3 1)) (check-sat)
sat unsat
これで必要な制約をSMT-LIBで表現する準備が出来ました。 あとは心を無にしてひたすらエディタに放り込むだけです。*1
問題はテキトーにヤフーで『数独 最高難易度』でググって出てきた結果を使用しています。
;; 01 02 03 | 04 05 06 | 07 08 09 ;; 10 11 12 | 13 14 15 | 16 17 18 ;; 19 20 21 | 22 23 24 | 25 26 27 ;; ---------+----------+--------- ;; 28 29 30 | 31 32 33 | 34 35 36 ;; 37 38 39 | 40 41 42 | 43 44 45 ;; 46 47 48 | 49 50 51 | 52 53 54 ;; ---------+----------+--------- ;; 55 56 57 | 58 59 60 | 61 62 63 ;; 64 65 66 | 67 68 69 | 70 71 72 ;; 73 74 75 | 76 77 78 | 79 80 81 ;; ;; __ __ _5 | _3 __ __ | __ __ __ ;; _8 __ __ | __ __ __ | __ _2 __ ;; __ _7 __ | __ _1 __ | _5 __ __ ;; ---------+----------+--------- ;; _4 __ __ | __ __ _5 | _3 __ __ ;; __ _1 __ | __ _7 __ | __ __ _6 ;; __ __ _3 | _2 __ __ | __ _8 __ ;; ---------+----------+--------- ;; __ _6 __ | _5 __ __ | __ __ _9 ;; __ __ _4 | __ __ __ | __ _3 __ ;; __ __ __ | __ __ _9 | _7 __ __ ;; (declare-const x01 Int) (declare-const x02 Int) (declare-const x03 Int) (declare-const x04 Int) (declare-const x05 Int) (declare-const x06 Int) (declare-const x07 Int) (declare-const x08 Int) (declare-const x09 Int) (declare-const x10 Int) (declare-const x11 Int) (declare-const x12 Int) (declare-const x13 Int) (declare-const x14 Int) (declare-const x15 Int) (declare-const x16 Int) (declare-const x17 Int) (declare-const x18 Int) (declare-const x19 Int) (declare-const x20 Int) (declare-const x21 Int) (declare-const x22 Int) (declare-const x23 Int) (declare-const x24 Int) (declare-const x25 Int) (declare-const x26 Int) (declare-const x27 Int) (declare-const x28 Int) (declare-const x29 Int) (declare-const x30 Int) (declare-const x31 Int) (declare-const x32 Int) (declare-const x33 Int) (declare-const x34 Int) (declare-const x35 Int) (declare-const x36 Int) (declare-const x37 Int) (declare-const x38 Int) (declare-const x39 Int) (declare-const x40 Int) (declare-const x41 Int) (declare-const x42 Int) (declare-const x43 Int) (declare-const x44 Int) (declare-const x45 Int) (declare-const x46 Int) (declare-const x47 Int) (declare-const x48 Int) (declare-const x49 Int) (declare-const x50 Int) (declare-const x51 Int) (declare-const x52 Int) (declare-const x53 Int) (declare-const x54 Int) (declare-const x55 Int) (declare-const x56 Int) (declare-const x57 Int) (declare-const x58 Int) (declare-const x59 Int) (declare-const x60 Int) (declare-const x61 Int) (declare-const x62 Int) (declare-const x63 Int) (declare-const x64 Int) (declare-const x65 Int) (declare-const x66 Int) (declare-const x67 Int) (declare-const x68 Int) (declare-const x69 Int) (declare-const x70 Int) (declare-const x71 Int) (declare-const x72 Int) (declare-const x73 Int) (declare-const x74 Int) (declare-const x75 Int) (declare-const x76 Int) (declare-const x77 Int) (declare-const x78 Int) (declare-const x79 Int) (declare-const x80 Int) (declare-const x81 Int) (assert (and (<= 1 x01) (>= 9 x01))) (assert (and (<= 1 x02) (>= 9 x02))) (assert (and (<= 1 x03) (>= 9 x03))) (assert (and (<= 1 x04) (>= 9 x04))) (assert (and (<= 1 x05) (>= 9 x05))) (assert (and (<= 1 x06) (>= 9 x06))) (assert (and (<= 1 x07) (>= 9 x07))) (assert (and (<= 1 x08) (>= 9 x08))) (assert (and (<= 1 x09) (>= 9 x09))) (assert (and (<= 1 x10) (>= 9 x10))) (assert (and (<= 1 x11) (>= 9 x11))) (assert (and (<= 1 x12) (>= 9 x12))) (assert (and (<= 1 x13) (>= 9 x13))) (assert (and (<= 1 x14) (>= 9 x14))) (assert (and (<= 1 x15) (>= 9 x15))) (assert (and (<= 1 x16) (>= 9 x16))) (assert (and (<= 1 x17) (>= 9 x17))) (assert (and (<= 1 x18) (>= 9 x18))) (assert (and (<= 1 x19) (>= 9 x19))) (assert (and (<= 1 x20) (>= 9 x20))) (assert (and (<= 1 x21) (>= 9 x21))) (assert (and (<= 1 x22) (>= 9 x22))) (assert (and (<= 1 x23) (>= 9 x23))) (assert (and (<= 1 x24) (>= 9 x24))) (assert (and (<= 1 x25) (>= 9 x25))) (assert (and (<= 1 x26) (>= 9 x26))) (assert (and (<= 1 x27) (>= 9 x27))) (assert (and (<= 1 x28) (>= 9 x28))) (assert (and (<= 1 x29) (>= 9 x29))) (assert (and (<= 1 x30) (>= 9 x30))) (assert (and (<= 1 x31) (>= 9 x31))) (assert (and (<= 1 x32) (>= 9 x32))) (assert (and (<= 1 x33) (>= 9 x33))) (assert (and (<= 1 x34) (>= 9 x34))) (assert (and (<= 1 x35) (>= 9 x35))) (assert (and (<= 1 x36) (>= 9 x36))) (assert (and (<= 1 x37) (>= 9 x37))) (assert (and (<= 1 x38) (>= 9 x38))) (assert (and (<= 1 x39) (>= 9 x39))) (assert (and (<= 1 x40) (>= 9 x40))) (assert (and (<= 1 x41) (>= 9 x41))) (assert (and (<= 1 x42) (>= 9 x42))) (assert (and (<= 1 x43) (>= 9 x43))) (assert (and (<= 1 x44) (>= 9 x44))) (assert (and (<= 1 x45) (>= 9 x45))) (assert (and (<= 1 x46) (>= 9 x46))) (assert (and (<= 1 x47) (>= 9 x47))) (assert (and (<= 1 x48) (>= 9 x48))) (assert (and (<= 1 x49) (>= 9 x49))) (assert (and (<= 1 x50) (>= 9 x50))) (assert (and (<= 1 x51) (>= 9 x51))) (assert (and (<= 1 x52) (>= 9 x52))) (assert (and (<= 1 x53) (>= 9 x53))) (assert (and (<= 1 x54) (>= 9 x54))) (assert (and (<= 1 x55) (>= 9 x55))) (assert (and (<= 1 x56) (>= 9 x56))) (assert (and (<= 1 x57) (>= 9 x57))) (assert (and (<= 1 x58) (>= 9 x58))) (assert (and (<= 1 x59) (>= 9 x59))) (assert (and (<= 1 x60) (>= 9 x60))) (assert (and (<= 1 x61) (>= 9 x61))) (assert (and (<= 1 x62) (>= 9 x62))) (assert (and (<= 1 x63) (>= 9 x63))) (assert (and (<= 1 x64) (>= 9 x64))) (assert (and (<= 1 x65) (>= 9 x65))) (assert (and (<= 1 x66) (>= 9 x66))) (assert (and (<= 1 x67) (>= 9 x67))) (assert (and (<= 1 x68) (>= 9 x68))) (assert (and (<= 1 x69) (>= 9 x69))) (assert (and (<= 1 x70) (>= 9 x70))) (assert (and (<= 1 x71) (>= 9 x71))) (assert (and (<= 1 x72) (>= 9 x72))) (assert (and (<= 1 x73) (>= 9 x73))) (assert (and (<= 1 x74) (>= 9 x74))) (assert (and (<= 1 x75) (>= 9 x75))) (assert (and (<= 1 x76) (>= 9 x76))) (assert (and (<= 1 x77) (>= 9 x77))) (assert (and (<= 1 x78) (>= 9 x78))) (assert (and (<= 1 x79) (>= 9 x79))) (assert (and (<= 1 x80) (>= 9 x80))) (assert (and (<= 1 x81) (>= 9 x81))) (assert (distinct x01 x02 x03 x04 x05 x06 x07 x08 x09)) (assert (distinct x10 x11 x12 x13 x14 x15 x16 x17 x18)) (assert (distinct x19 x20 x21 x22 x23 x24 x25 x26 x27)) (assert (distinct x28 x29 x30 x31 x32 x33 x34 x35 x36)) (assert (distinct x37 x38 x39 x40 x41 x42 x43 x44 x45)) (assert (distinct x46 x47 x48 x49 x50 x51 x52 x53 x54)) (assert (distinct x55 x56 x57 x58 x59 x60 x61 x62 x63)) (assert (distinct x64 x65 x66 x67 x68 x69 x70 x71 x72)) (assert (distinct x73 x74 x75 x76 x77 x78 x79 x80 x81)) (assert (distinct x01 x10 x19 x28 x37 x46 x55 x64 x73)) (assert (distinct x02 x11 x20 x29 x38 x47 x56 x65 x74)) (assert (distinct x03 x12 x21 x30 x39 x48 x57 x66 x75)) (assert (distinct x04 x13 x22 x31 x40 x49 x58 x67 x76)) (assert (distinct x05 x14 x23 x32 x41 x50 x59 x68 x77)) (assert (distinct x06 x15 x24 x33 x42 x51 x60 x69 x78)) (assert (distinct x07 x16 x25 x34 x43 x52 x61 x70 x79)) (assert (distinct x08 x17 x26 x35 x44 x53 x62 x71 x80)) (assert (distinct x09 x18 x27 x36 x45 x54 x63 x72 x81)) (assert (distinct x01 x02 x03 x10 x11 x12 x19 x20 x21)) (assert (distinct x04 x05 x06 x13 x14 x15 x22 x23 x24)) (assert (distinct x07 x08 x09 x16 x17 x18 x25 x26 x27)) (assert (distinct x28 x29 x30 x37 x38 x39 x46 x47 x48)) (assert (distinct x31 x32 x33 x40 x41 x42 x49 x50 x51)) (assert (distinct x34 x35 x36 x43 x44 x45 x52 x53 x54)) (assert (distinct x55 x56 x57 x64 x65 x66 x73 x74 x75)) (assert (distinct x58 x59 x60 x67 x68 x69 x76 x77 x78)) (assert (distinct x61 x62 x63 x70 x71 x72 x79 x80 x81)) (assert (= x03 5)) (assert (= x04 3)) (assert (= x10 8)) (assert (= x17 2)) (assert (= x20 7)) (assert (= x23 1)) (assert (= x25 5)) (assert (= x28 4)) (assert (= x33 5)) (assert (= x34 3)) (assert (= x38 1)) (assert (= x41 7)) (assert (= x45 6)) (assert (= x48 3)) (assert (= x49 2)) (assert (= x53 8)) (assert (= x56 6)) (assert (= x58 5)) (assert (= x63 9)) (assert (= x66 4)) (assert (= x71 3)) (assert (= x78 9)) (assert (= x79 7)) (check-sat) (get-model)
sat
(model
(define-fun x01 () Int
1)
(define-fun x75 () Int
1)
(define-fun x65 () Int
8)
(define-fun x24 () Int
8)
(define-fun x50 () Int
9)
(define-fun x59 () Int
4)
(define-fun x69 () Int
1)
(define-fun x21 () Int
2)
(define-fun x42 () Int
3)
(define-fun x44 () Int
5)
(define-fun x08 () Int
9)
(define-fun x55 () Int
3)
(define-fun x73 () Int
5)
(define-fun x19 () Int
6)
(define-fun x46 () Int
7)
(define-fun x15 () Int
4)
(define-fun x39 () Int
8)
(define-fun x72 () Int
5)
(define-fun x32 () Int
8)
(define-fun x37 () Int
2)
(define-fun x02 () Int
4)
(define-fun x47 () Int
5)
(define-fun x60 () Int
2)
(define-fun x68 () Int
6)
(define-fun x13 () Int
6)
(define-fun x16 () Int
1)
(define-fun x26 () Int
4)
(define-fun x80 () Int
6)
(define-fun x14 () Int
5)
(define-fun x54 () Int
1)
(define-fun x36 () Int
2)
(define-fun x31 () Int
1)
(define-fun x29 () Int
9)
(define-fun x43 () Int
9)
(define-fun x64 () Int
9)
(define-fun x06 () Int
7)
(define-fun x11 () Int
3)
(define-fun x05 () Int
2)
(define-fun x67 () Int
7)
(define-fun x76 () Int
8)
(define-fun x62 () Int
1)
(define-fun x09 () Int
8)
(define-fun x18 () Int
7)
(define-fun x30 () Int
6)
(define-fun x52 () Int
4)
(define-fun x12 () Int
9)
(define-fun x81 () Int
4)
(define-fun x27 () Int
3)
(define-fun x57 () Int
7)
(define-fun x51 () Int
6)
(define-fun x77 () Int
3)
(define-fun x07 () Int
6)
(define-fun x74 () Int
2)
(define-fun x40 () Int
4)
(define-fun x35 () Int
7)
(define-fun x61 () Int
8)
(define-fun x70 () Int
2)
(define-fun x22 () Int
9)
(define-fun x79 () Int
7)
(define-fun x78 () Int
9)
(define-fun x71 () Int
3)
(define-fun x66 () Int
4)
(define-fun x63 () Int
9)
(define-fun x58 () Int
5)
(define-fun x56 () Int
6)
(define-fun x53 () Int
8)
(define-fun x49 () Int
2)
(define-fun x48 () Int
3)
(define-fun x45 () Int
6)
(define-fun x41 () Int
7)
(define-fun x38 () Int
1)
(define-fun x34 () Int
3)
(define-fun x33 () Int
5)
(define-fun x28 () Int
4)
(define-fun x25 () Int
5)
(define-fun x23 () Int
1)
(define-fun x20 () Int
7)
(define-fun x17 () Int
2)
(define-fun x10 () Int
8)
(define-fun x04 () Int
3)
(define-fun x03 () Int
5)
)
おわりに
やってみて思ったのですが、正直これを手入力するのはつらみポイントバクアゲなんてものではありません。 折れた心をセメントで塗り固めながら作業をしました。
定型的な制約を生成するのは手続き型と相性がよさそうです。つまり、制約の生成を手続き型にやらせて、解くのを制約ソルバーにやらせるのがよさそうです。 というわけで次回はVB.NETから制約を生成し、それをz3に放り込む方法を確認してみましょう。
