Variable expression with all operations history

During execution manager will set expressions in variables in order to aid debugging. Every expression might have on out of three possible formats:

Format 1: Constant variable

Constant variables have the following expressions:

variableName[value]{=source}

For instance:

solver.FromConstant(0).Operation(OperationType.BinaryNegation).FullExpression() == "_v_1[1]{=1}"

Part _v_1 is a variable name. In this example it is simply _v_1.

Part [1] indicates precalculated variable value.

Part {=1} means that the variable obtained its value from constant expression (in this case just from number one).

Format 1: Non-constant variable with precalculated value

Non-constant variables with precalculated values have the following expressions:

variableName[value?Domain]{=source}

For instance:

solver.FromConstant(0).Create("a").Operation(OperationType.BinaryNegation).Create("result").FullExpression() == "result[1?BinaryInteger]{=_v_5[1?BinaryInteger]{=!a[0?BinaryInteger]{=_v_0[0]{=0}}}}"

This looks terrible. Let's analyze the expression from left to right:

Part result is a variable name.

Part [1?BinaryInteger] indicates that the variable SHOULD have value 1. Manager cannot be sure of that because it is up to solver whether the variable will have this value, but all operations (if executed correctly) should give one in this example. It also means that the variable should be binary in the solution.

Part {=_v_5[1?BinaryInteger]{=!a[0?BinaryInteger]{=_v_0[0]{=0}}}} shows the source of the value. Let's decompose it:

Part _v_5[1?BinaryInteger]says that result took its value from assigning to variable _v_5, which was binary variable which should be equal to one.

Part {=!a[0?BinaryInteger]{=_v_0[0]{=0}}} gives the source of _v_5 variable. Let's go on:

Part !a[0?BinaryInteger] says that _v_5 is a binary negated variable a which is a binary variable and should be equal to 0.

Part {=_v_0[0]{=0}} says, that a took its value from variable _v_0, which was constant and equal to zero.

I hope you get the idea. You can track history of your operations just by examining the expression of a variable.

Format 3: Non-constant variable without known value

Non-constant variable without known value has the following format:

variableName[Domain]{=source}

For instance:

solver.Create("v", Domain.AnyInteger) == "v[AnyInteger]{=}"

We can see, that variable v is any integer, and that we don't know the source (part {=}).

Operations

Different operations have different formats. Below is a short list of operations' expressions:

Absolute value: |variable|
Addition: variable + variable
Approximation: approximation(function)
Approximation2D: approximation2D(function)
ArrayGet: arrayGet(index: value, variables)
ArraySet: arraySet(wantedIndex: value, value: value, inArrayIndex: value, variables)
Binary negation: !variable
Condition: variable ? variable : variable
Conjunction: variable && variable
Counting sort: countingSort(position: index, variable)
Decomposition: decomposition(digit: index, base: value, variable)
Disjunction: variable || variable
Division: variable / variable
Exclusive disjunction: variable ^ variable
Equivalency: variable <==> variable
Exponentiation: variable ** variable
GCD: gcd(variable, variable)
Is equal: variable ?== variable
Is greater or equal: variable ?>= variable
Is greater than: variable ?> variable
Is less or equal: variable ?<= variable
Is less than: variable ?< variable
Is lexicographical equal: (variable, variable) ?== (variable, variable)
Is lexicographical greater or equal: (variable, variable) ?>= (variable, variable)
Is lexicographical greater than: (variable, variable) ?> (variable, variable)
Is lexicographical less or equal: (variable, variable) ?<= (variable, variable)
Is lexicographical less than: (variable, variable) ?< (variable, variable)
Is lexicographical not equal: (variable, variable) ?!= (variable, variable)
Is not equal: variable ?!= variable
Material implication: variable => variable
Maximum: max(variable, variable)
Minimum: min(variable, variable)
Multiplication: variable * variable
N-th element: nthElement(index: 0, variable)
Negation: -variable
Remainder: variable % variable
Selection sort: selectionSort(position: index, variable)
Subtraction: variable - variable
Unsigned magnitude decomposition: unsignedMagnitudeDecomposition(bit: index, variable)