Kodkodi 1.0.2 (October 30, 2008) is a front-end for the Java library Kodkod, a SAT-based solver for first-order logic with relations, transitive closure, and partial instances. Kodkod forms the basis of Alloy Analyzer version 4. The Kodkodi front-end is designed to make the Kodkod library available to other programming languages than Java. Kodkodi is developed and maintained by Jasmin Christian Blanchette at the Technische Universität München. It is available under the following license:
Copyright (c) 2008, Technische Universität München. All rights reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: * Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. * The name of the Technische Universität München may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Kodkodi requires the 2007 version of Kodkod to be installed in the Java classpath. To run the program, you simply need a Java 1.5 virtual machine (normally called java). To recompile it, you need a Java compiler and the ANTLR parser generator (version 3.1.1).
The kodkodi program takes its input from standard input and writes its output to standard output (on success) or standard error (on failure). Examples are provided in the examples directory.
Example:
$ java de.tum.in.isabelle.Kodkodi.Kodkodi < examples/pigeonhole.kki ---UNIVERSE--- [A0, A1, A2, A3, A4, A5] ---BOUNDS--- relation bounds: s0: [[[A0], [A1], [A2]]] s1: [[[A3], [A4]]] r0: [[], [[A0, A3], [A0, A4], [A1, A3], [A1, A4], [A2, A3], [A2, A4]]] int bounds: [] ---FORMULA--- (FUNCTION(r0, s0 ->one s1) && (all [S0: one s0, S1: one s0] | (!(S0 = S1) => no ((S0 . r0) & (S1 . r0))))) ---OUTCOME--- UNSATISFIABLE ---STATS--- p cnf 54 68 primary variables: 6 translation time: 90 ms solving time: 0 ms
Kodkodi's input format borrows heavily from the output format of the toString() implementations found in the Kodkod library. The operator that are available in Alloy 4 are given the same precedences as they have there.
The grammar is expressed using a variant of Extended Backus-Naur Form (EBNF). The actual grammar used by Kodkodi is written using ANTLR and can be found in the file Kodkodi.g.
The grammar is based on the following lexical units, or tokens:
WHITESPACE ::= ( | \n | \r | \t | \v)+
COMMENT ::= // ~(\n)* (\n | EOF)
NUM: ::= [+ | -] (0 | 1 | … | 9)+
STR_LITERAL ::= " ~(" | \n)* "
ATOM_NAME ::= A NAT
TUPLE_NAME ::= (P | T NAT _) NAT
RELATION_NAME ::= (s | r | m NAT _) NAT
VARIABLE_NAME ::= (S | R | M NAT _) NAT
TUPLE_REG ::= $ (A | P | T NAT _) NAT
TUPLE_SET_REG ::= $ (a | p | t NAT _) NAT
FORMULA_REG ::= $f NAT
REL_EXPR_REG ::= $e NAT
INT_EXPR_REG ::= $i NAT
NAT abbreviates '0' | '1'..'9' '0'..'9'*.
Comments start with // and end with the line. Whitespace is ignored, except as a token separator. In addition to the tokens listed above, various keywords and operators are recognized as tokens. These are shown in bold in the grammar.
The table below describes the lexical conventions adopted for naming atoms, tuples, relations, variables, and registers.
| Token Name | Syntax | Description |
| ATOM_NAME | Aj | Atom at index j in the universe |
| TUPLE_NAME | Pj | Pair at index j in the pair space associated with the universe |
| Tn_j | n-tuple at index j in the n-tuple space associated with the universe (n ≥ 3) | |
| RELATION_NAME | sj | Set number j |
| rj | Binary relation number j | |
| mn_j | n-ary multirelation number j (n ≥ 3) | |
| VARIABLE_NAME | Sj | Set variable number j |
| Rj | Binary relation variable number j | |
| Mn_j | n-ary multirelation variable number j (n ≥ 3) | |
| TUPLE_REG | $Aj | One-tuple register number j |
| $Pj | Pair register number j | |
| $Tn_j | n-tuple register number j (n ≥ 3) | |
| TUPLE_SET_REG | $aj | One-tuple set register number j |
| $pj | Pair set register number j | |
| $tn_j | n-tuple set register number j (n ≥ 3) | |
| FORMULA_REG | $fj | Formula register number j |
| REL_EXPR_REG | $ej | Relational expression register number j |
| INT_EXPR_REG | $ij | Integer expression register number j |
Atoms and tuples are defined implicitly in terms of the universe. Relations and variables need no declarations, but relations do need bounds. Registers must be assigned to before they are used in an expression. It is highly recommended to use low indices because Kodkodi stores relations, variables, and registers in 0-based arrays.
This section presents the overall structure of Kodkod input files.
problem ::= prealloc_directive?
option*
univ_spec
tuple_reg_directive*
bound_spec*
int_bound_spec?
expr_reg_directive*
solve_directive
Kodkodi takes a “problem” as input. A problem consists of three main parts: a universe specification, a set of bound specifications, and a Kodkod formula to satisfy supplied in a “solve” directive.
Example:
univ: {A0}
bounds s0: [{A0}]
solve all [S0 : one s0, S1 : one s0] | S0 = S1
prealloc_directive ::= prealloc (RELATION_NAME |
VARIABLE_NAME |
TUPLE_REG |
TUPLE_SET_REG |
FORMULA_REG |
REL_EXPR_REG |
INT_EXPR_REG)*;
The optional prealloc directive can be used as an optimization to tell Kodkodi how many relations, variables, and registers will be needed. This way, Kodkodi can allocate the memory at startup, instead of continuously resizing its internal data structures.
Example:
prealloc $p10 $P25 $f59 $e20 $i12 s20 r45 S10 R23
option ::= solver : STR_LITERAL (, STR_LITERAL)* |
symmetry_breaking : NUM |
sharing : NUM |
bitwidth : NUM |
skolem_depth : NUM |
flatten : (true | false)
Kodkod supports various options, documented in the kodkod.engine.config.Options class. The following solvers are supported:
solver: "DefaultSAT4J" solver: "LightSAT4J" solver: "ZChaff" solver: "ZChaffMincost" solver: "MiniSatProver" solver: "MiniSat" solver: "SAT4J" "instance" solver: "External" "executable" "temp_input" "temp_output" "arg_1" … "arg_n"
univ_spec ::= univ : { A0 [.. ATOM_NAME] }
The universe specification fixes the universe's uninterpreted atoms. Kodkodi requires that the atoms are numbered consecutively from A0 to A(n − 1).
Examples:
univ: {A0}
univ: {A0 .. A99}
bound_spec ::= bounds RELATION_NAME (, RELATION_NAME) :
[ tuple_set [, tuple_set] ]
A relational bound specification gives a lower and an upper bound for the given relations. If only one bound is specified, it is taken as both lower and upper bound. The lower bound must be a subset of the upper bound.
Examples:
bounds s0, s1: [{}, {A0 .. A9}]
bounds r2: [{A0 .. A9} -> {A10 .. A19}]
int_bound_spec ::= int_bounds : int_bound_seq (, int_bound_seq)* int_bound_seq ::= [NUM :] [ tuple_set (, tuple_set)* ]
An integer bound specification establishes a correspondence between integers and sets of atoms that represent that integer in relational expressions. The syntax makes it possible to specify the bounds of consecutive integers in sequence.
Example:
int_bounds: [{A0}, {A1}], 10: [{A2}, {A3}, {A4}]
In the above example, 0 is bounded by {A0}, 1 is bounded by {A1}, 10 is bounded by {A2}, 11 is bounded by {A11}, and 12 is bounded by {A4}.
solve_directive ::= solve formula
The “solve” directive tells Kodkod to try to satisfy the given formula.
Example:
solve all [S0 : one s0, S1 : one s0] | !(S0 = S1) => no (S0.r0 & S1.r0)
Registers make it possible to use a complex syntactic construct several times without duplicating it. They also help reduce Kodkod's memory usage and running time.
tuple_reg_directive ::= TUPLE_REG := tuple |
TUPLE_SET_REG := tuple_set
A tuple register directive assigns a value to a tuple or tuple set register.
Examples:
$P0 := [A0, A0]
$P1 := [A1, A1]
$t4_0 := {$P0, $P1} -> {$P0, $P1}
expr_reg_directive ::= FORMULA_REG := formula |
REL_EXPR_REG := rel_expr |
INT_EXPR_REG := int_expr
Formulas, relational expressions, and integer expressions can also be assigned to registers using an expression register directive. An alternative is to use the let binder inside an expression.
Examples:
$f0 := all [S0 : one s0] | s0 in univ $e5 := (s0 & s1).r1 + (s0 & s2).r2 $i14 := 2 * #($e5) + 1
Kodkod supports partial solutions in the form of bounds on relations. The bound specifications involve tuples and tuple sets.
tuple ::= [ ATOM_NAME (, ATOM_NAME)* ] |
ATOM_NAME |
TUPLE_NAME |
TUPLE_REG
An n-tuple is normally specified using the syntax [Aj1, …, Ajn]. The brackets are optional when n = 1. Alternatively, tuples can be specified using an index in the n-tuple space. For example, given the universe {A0 .. A9}, the name P27 refers to the pair [A2, A7].
Examples:
[A0, A1, A5, A20] A0 P5 $P14
tuple_set ::= tuple_set -> tuple_set |
tuple_set [ NUM ] |
{ tuple (, tuple)* } |
{ tuple .. tuple } |
{ tuple # tuple } |
none |
all |
TUPLE_SET_REG
Tuple sets can be constructed in several ways. The -> operator denotes the Cartesian product of two tuple sets. The [] operator projects the tuple set onto the given dimension. Tuple sets can be specified exhaustively by listing all their tuples. If all the tuples have consecutive indices, the range operator .. can be used. Alternatively, if all the tuples occupy a rectangular, cubic, etc., area in the tuple space, they can be specified by passing the lowest and highest corner of the area to the # operator. Finally, none is a synonym for {}, and all denotes the complete tuple set (whose arity is deduced from the context).
Examples:
{A1}
{A1, A2} -> {A3, A4}
{[A1, A2] .. [A3, A4]}
{[A1, A2] # [A3, A4]}
$p14
Kodkod supports three types of expression: Boolean expressions (formulas), relational expressions, and integer expressions.
formula ::= (all | some) decls | formula |
let assigns | formula |
if formula then formula else formula |
formula || formula |
formula xor formula |
formula <=> formula |
formula => formula |
formula && formula |
! formula |
ACYCLIC ( RELATION_NAME ) |
FUNCTION ( RELATION_NAME , rel_expr -> (ONE | LONE) rel_expr ) |
TOTAL_ORDERING ( RELATION_NAME , RELATION_NAME , RELATION_NAME ,
RELATION_NAME ) |
rel_expr (in | =) rel_expr |
int_expr (= | < | <= | > | >=) int_expr |
(no | lone | one | some) rel_expr |
false |
true |
FORMULA_REG |
( formula )
A formula, or Boolean expression, specifies a constraint involving relations and integers.
Example:
some [S0 : some s0] | if S0 in s1 then !$f1 else $i0 <= $i1
rel_expr ::= let assigns | rel_expr |
if formula then rel_expr else rel_expr |
rel_expr (+ | -) rel_expr |
rel_expr ++ rel_expr |
rel_expr & rel_expr |
rel_expr -> rel_expr |
rel_expr [ int_expr (, int_expr)* ] |
rel_expr . rel_expr |
(^ | * | ~) rel_expr |
{ decls | formula } |
(Bits | Int) [ int_expr ] |
iden |
ints |
none |
univ |
RELATION_NAME |
VARIABLE_NAME |
REL_EXPR_REG |
( rel_expr )
A relational expression denotes a relation (set, binary relation, or multirelation).
Example:
if #(s0) > 5 then s0.r0 + s1.r1 else none
int_expr ::= sum decls | int_expr |
let assigns | int_expr |
if formula then int_expr else int_expr |
int_expr (<< | >> | >>>) int_expr |
int_expr (+ | -) int_expr |
int_expr (* | / | %) int_expr |
(# | sum) ( rel_expr ) |
int_expr | int_expr |
int_expr ^ int_expr |
int_expr & int_expr |
(~ | - | abs | sgn) int_expr |
NUM |
INT_EXPR_REG |
( int_expr )
An integer expression denotes an integer.
Example:
(sum [S0 : one s0] | #(S0) * (#(S0) + 1) / 2) % 10
decls ::= [ decl (, decl)* ] decl ::= VARIABLE_NAME : (no | lone | one | some | set) rel_expr
The all, some, and sum quantifiers take a list of variable declarations.
Example:
[S0 : set s0, S1 : one s1]
assigns ::= [ assign (, assign)* ]
assign ::= FORMULA_REG := formula |
REL_EXP_REG := rel_exp |
INT_EXP_REG := int_exp
The let binder takes a list of register assignments.
Example:
[$f0 := all [S0 : one s0] | s0 in univ, $i14 := 2 * #($e5) + 1]
The operator precedences and associativities are given in the table below. Fully bracketed operators are not listed.
| Level | Operator Class | Arity | Associativity |
| 1 | all | some | sum | let | if then else | Binary/Ternary | Right-associative |
| 2 | || | Binary | Associative |
| 3 | xor | Binary | Associative |
| 4 | <=> | Binary | Associative |
| 5 | => | Binary | Right-associative |
| 6 | && | Binary | Associative |
| 7 | ! | Unary | N/A |
| 8 | in = < <= > >= | Binary | N/A |
| 9 | no lone one some | Unary | N/A |
| 10 | << >> >>> | Binary | Left-associative |
| 11 | + - | Binary | Left-associative |
| 12 | * / % | Binary | Left-associative |
| 13 | ++ | Binary | Associative |
| 14 | | | Binary | Associative |
| 15 | ^ | Binary | Associative |
| 16 | & | Binary | Associative |
| 17 | -> | Binary | Associative |
| 18 | [] | Binary | Left-associative |
| 19 | . | Binary | Left-associative |
| 20 | ^ * ~ - abs sgn | Unary | N/A |