Alloyの出力したKodKod fileを読む

sig X{}
run{
	#X = 2
}

CNFを読もうとしたが、フォーマット*1を教えてもらっても、C言語に例えるならコンパイル済みのバイナリをhexdumpで眺めているような感じでハードルが高いのでKodKod fileを見てみることにした。

import java.util.Arrays;
import java.util.List;
import kodkod.ast.*;
import kodkod.ast.operator.*;
import kodkod.instance.*;
import kodkod.engine.*;
import kodkod.engine.satlab.SATFactory;
import kodkod.engine.config.Options;

/* 
  ==================================================
    kodkod formula: 
  ==================================================
    #(this/X) = 2 && 
    Int/next = Int/next && 
    seq/Int = seq/Int && 
    String = String && 
    this/X = this/X
  ==================================================
*/
public final class Test {

public static void main(String[] args) throws Exception {

Relation x0 = Relation.nary("Int/next", 2);
Relation x1 = Relation.unary("seq/Int");
Relation x2 = Relation.unary("String");
Relation x3 = Relation.unary("this/X");

List<String> atomlist = Arrays.asList(
 "X$0", "X$1", "X$2"
);

Universe universe = new Universe(atomlist);
TupleFactory factory = universe.factory();
Bounds bounds = new Bounds(universe);

TupleSet x0_upper = factory.noneOf(2);
bounds.boundExactly(x0, x0_upper);

TupleSet x1_upper = factory.noneOf(1);
bounds.boundExactly(x1, x1_upper);

TupleSet x2_upper = factory.noneOf(1);
bounds.boundExactly(x2, x2_upper);

TupleSet x3_upper = factory.noneOf(1);
x3_upper.add(factory.tuple("X$0"));
x3_upper.add(factory.tuple("X$1"));
x3_upper.add(factory.tuple("X$2"));
bounds.bound(x3, x3_upper);


IntExpression x6=x3.count();
IntExpression x7=IntConstant.constant(2);
Formula x5=x6.eq(x7);
Formula x8=x0.eq(x0);
Formula x9=x1.eq(x1);
Formula x10=x2.eq(x2);
Formula x11=x3.eq(x3);
Formula x4=Formula.compose(FormulaOperator.AND, x5, x8, x9, x10, x11);

Solver solver = new Solver();
solver.options().setSolver(SATFactory.DefaultSAT4J);
solver.options().setBitwidth(0);
solver.options().setFlatten(false);
solver.options().setIntEncoding(Options.IntEncoding.TWOSCOMPLEMENT);
solver.options().setSymmetryBreaking(20);
solver.options().setSkolemDepth(0);
System.out.println("Solving...");
System.out.flush();
Solution sol = solver.solve(x4,bounds);
System.out.println(sol.toString());
}}

なるほどなるほど。こういうJavaファイルを出力して、コンパイルして実行しているのか。

それはそうと、明示的に出力させているのにファイルをテンポラリファイルとして吐き出すので、UIへの出力からマウスで選択してコピペしないといけないのとか非常にめんどい。そろそろAlloyをソースからビルドできるように環境を整えねば。

未解決問題:

• (未解決) Alloyのソースをいじってビルドし直すにはどうすればいいのか。
  • Evaluatorの出力がコピペが出来なくてめんどくさいのでなんとかしたい
  • Visualizeの結果を1枚1枚スクリーンショットを取るのはめんどくさいので連番画像で出力したい
  • KodKod fileがテンポラリファイルとして出力されるのをやめさせたい

*1:benchmarks submission guidelines