specification.md

 # Specificiation 
 
-## Atoms
+NDL is a strongly-typed declarative language describing both constraint programming problem structure and neighbor operators.
 
-There are two types of atoms in the NDL language:
+## Syntax 
+
+There are three types of atoms in the NDL language:
 * integers, i.e. `0`
 * variables with Prolog syntax, i.e. `X`, `Variable`, `_OtherVariable`
 * variable indexes, that are terms with arity depending on the variable dimensionality, i.e. for a 2-dimension array of variable named `queen`, the variable's index takes form `queen(<integer>, <integer>)`, i.e. `queen(1,1)`.
 
 Additionaly string constants (lower case, as `name`) and the integer ranges (written as `0..10`) are used as a syntax sugar in model definitions, but aren't used in the NDL query itself.
 
-## Types
-
-Every atom has an associated type, storing additional information about the atom:
+## Type system
 
-* in case of the variable, type defines domain of the variable; language doesn't allow to change the variable's type, therefore all arithmetic operations are implemented in a way to satisfy the domain closure
+There are three kinds of types in the language:
+* constants - named integers, represented as term `const/1`, i.e. `const(size)`.  
+* ranges - named sets of integers, representes as term `range/1`, i.e. `range(teams)`.
+* variable indexes - where index may be 0-dimensional (singleton variable), 1-dimensional (1-d array of variables), 2-dimensional, up to 6-dimensional, represented as term `var/1` i.e. `var(queen)`. There exist subkinds of this kind: auxillary variables (`avar/1`), reified constraints `rvar/1`) and fixed variables (`fvar/1`). 
 
-Types are defined in the NDL model as `constants` and are problem dependent.
+Specific kinds are used in a different way in the systems. For every constraint programming problem, we define a set of types specific to the problem.
 
 ## Model
 
-NDL model is a typed Prolog program consisting of following predicates:
+NDL model defines structure of the constraint programming problem and is compiled to a typed Prolog program consisting of following predicates:
 
-* Constant related:
-  * `constant_definition(+Name:string, -Constant:integer)` - contains the constant definition. Constant should be understood as a type with only one possible value. The predicate should be used only using the compilation and shouldn't be used in the NDL queries.
-  * `constant_usages(+Name:string, -Context:list)` - another compile-only information. `Context` cotains information about all possible contexts, where the constant may be used, i.e. it allows to emulate the typed arguments in other predicates. Possible contexts include:
+* Type related:
+  * `type_of(+Context:context, -Type:type)` - contains typing information about variables and constraints, possible context include:
     * domain of a variable
     * indexing of a variable in a specific axis/dimension
-    * to be part of an arithmetic expression with a variable's value **FIXME**
-    * to be part of an arithmetic expression with a variable's index in a specific axis/dimension **FIXME**
-  * `constant(+Name:string, -Value:integer)` - allows to get constant value by it's name. Used in the NDL query.
-  * `constant_range_definition(+Name:string, -Range:range)` - analogically to the integer constant, this defines a type with a range of possible values.
-  * `constant_range_usages(+Name, -Context:list) - again, used to simulate typing in the Prolog program.
-  * `constant_range(+Name:string, -Value:integer) is nondet` - allows to non-deterministically get one of the type inhibitants. Used in the NDL query.
+    * 1st/2nd argument of the constraint
+  * `type_uses(+Type:type, -Contexts:list)` - contain information about all the context, the type can bu used in
+* Constant related:
+  * `constant_definition(+Name:string, -Constant:integer)` - contains the constant definition. Constant should be understood as a type with only one possible value. The predicate should be used only using the compilation and shouldn't be used in the NDL queries.
+  * `constant(+Name:string, -Value:integer)` - allows to get constant value by it's name. **Used in the NDL query**.
+* Range related
+  * `range_definition(+Name:string, -Range:range)` - analogically to the integer constant, this defines a type with a range of possible values.
+  * `range(+Name:string, -Value:integer) is nondet` - allows to non-deterministically get one of the type inhibitants. **Used in the NDL query.**
 * Variable related:
   * `fixed(+Name:string)` - variables with this name shouldn't be modified by the NDL query. Used only during compilation.
-  * `variable(+Name:string, -Index:variable_index) is nondet` - allows to non-deterministically get an index of the variable named `Name`. Used in the NDL query.
-  * `new_value(+Name:string, -Value:Integer) is nondet` - allows to non-deterministically get an possible value for the variable named `Name`. Used in the NDL query.
+  * `auxillary(+Name:string)` - variables with this name should be calculated in run-time based on one-directional constrants, used to define complex constraints
+  * `reified(+Name:string)` - variables with this name reify constraints with the same name. Their domain is always boolean.
+  * family of `variable` predicates allowing to non-deterministically get an indexed variable and it's index. **Used in the NDL query.**
+    * `variable(+Name:string, -Index:variable_index) is nondet` - for 0-dimensional variable types. 
+    * `variable(+Name:string, ?Index1:integer, -Index:variable_index) is nondet` - for 1-dimensional variable types.
+    * `variable(+Name:string, ?Index1:integer, ?Index2:integer, -Index:variable_index) is nondet` - for 2-dimensional variable types.
+    * ...
+    * `variable(+Name:string, ?Index1:integer, ?Index2:integer, ?Index3:integer, ?Index4:integer, ?Index5:integer, ?Index6:integer -Index:variable_index) is nondet` - for 6-dimensional variable types
+    
 * Constraint related:
-  * `constraint(+Name:string, ?Index1:variable_index, ?Index2:variable_index) is nondet` - allows to non-deterministically check if two variables indexed `Index1` and `Index2` are constrained with a constraint named `Name`. Also allows to find indexes satisfying those requirements. Used in the NDL query.
-  * `is_satisfied(+Name:String, +Index1:variable_index, +Index2:variable_index)` - allows to check if the constraint named `Name` is satisfied on variables indexed `Index1` and `Index2`. Used in the NDL query. **FIXME**
-dynamic_predicate(constraint/3, public). 
+  * `constraint(+Name:string, ?Arg1:type_of(arg1(Name)), ?Index2:type_of(arg2(Name)) is nondet` - allows to non-deterministically check if two arguments (variables or range elements) are constrained with a constraint named `Name`. Also allows to find elements satisfying those requirements. **Used in the NDL query**.
 
 ## Query