##########################################################################
#                                                                        #
#  Combine - an OCaml library for combinatorics                          #
#                                                                        #
#  Copyright (C) 2012-2014                                               #
#    Remy El Sibaie                                                      #
#    Jean-Christophe Filliatre                                           #
#                                                                        #
#  This software is free software; you can redistribute it and/or        #
#  modify it under the terms of the GNU Library General Public           #
#  License version 2.1, with the special exception on linking            #
#  described in file LICENSE.                                            #
#                                                                        #
#  This software is distributed in the hope that it will be useful,      #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
#                                                                        #
##########################################################################


* Library

  The Combine library contains four main modules:
  - Dlx: implements Knuth's dancing links
  - Zdd: implements Zero-suppressed binary decision diagrams
  - Emc: a common interface to modules Dlx and Zdd to solve EMC +
         reduction of EMC to SAT
  - Tiling: converts a 2D tiling problem into an EMC problem

  Usage: the Combine library is packed into a single module Combine, installed
  in the subdirectory combine/ of OCaml's standard library. Thus, it must be
  used as follows:

    ocamlc -I +combine combine.cma <other files>

  full documentation : https://usr.lmf.cnrs.fr/~jcf/combine/


* Examples

  The distribution contains several example programs:
  - queens.ml: solve the N-queens puzzle
  - sudoku.ml: well, you haved guessed already
  - color.ml: 4-color planar graphs using DLX and SAT (requires OCamlgraph
    and an explicit 'make color.opt')


* Tiling language and interpreter

  In addition to the library, Combine provides a language to describe 2D tiling
  problems and an interpreter (combine) for this language.

  Directory tests/ contains various examples of tiling problems (.cmb files).
  To execute such a test, just run "combine" on the file.

  The grammar of the tiling language is the following:

<file> ::=              | decl ... decl

<decl> ::=
			| pattern <identifier> = <expr>
			| tiles <identifier> = <tile_list>
			| problem <identifier>  equal <expr> tl = tiles
			| assert b = boolean_expr
			| print <identifier>
			| solve a = algo <identifier>  out = output
			| count a = algo <identifier>
                        | dimacs <identifier> <string>
			| debug st = state
			| timing st = state
			| exit
			| include <string>

algo ::=
			| dlx
			| zdd
                        | sat <string>

state ::=
			| on
			| off

option ::=
			| one
			| maybe
			| sym
			| rot

tiles ::=
			| <tile_list>
			| <identifier>

tile_list ::=
			| [ tile, ..., tile ]

output ::=
			| svg_out <string>
			| ascii_out

isometry ::=
			| id
			| rot90
			| rot180
			| rot270
			| vertrefl
			| horizrefl
			| diag1refl
			| diag2refl

tile ::=
			| <expr> o = list(option)

expr ::=
			| lpar <expr> rpar
			| <identifier>
			| constant <dim> <bool>
			| union <expr> <expr>
			| inter <expr> <expr>
			| diff <expr> <expr>
			| xor <expr> <expr>
			| <expr> minus <expr>
			| <expr> ampamp <expr>
			| <expr> barbar <expr>
			| <expr> hat <expr>
			| set <expr> <dim> <bool>
			| crop <dim> <dim> <expr>
			| shift <expr> <dim>
			| resize <expr> <dim>
			| apply <isometry> <expr>
			| <ascii>

bool ::=
			| false
			| true

boolean_expr::=
			| <bool>
			| <expr> equal <expr>