First Steps: FMS as a calculator
Sums
Let's see how we can use FMS as a calculator. We can define an identifier like x to be a numeric value like 4+5 as:
x := 4 + 5.
Don't forget the dot at the end (every statement ends with it)
You didn't write a constraint which uses your newly defined x. As a result of this, FMS thinks you can't be interested in this as it tries to prune as much things away as possible.
If you don't want to write a constraint about x, we can use the library function relevant to cheat our way out of this. Now we can write down a working example:
The standard operations +/*- are available. Take care that the division operator is integer division, so it truncates.
Also the abs function is available which takes the absolute value of a number.
Multiple symbols
It is possible to define multiple symbols and use one to define another. The order of your statements is irrelevant. Now we can define y to be the double of x.
Symbols with local scopes
Sometimes it will be useful to introduce a symbol locally, for example when you want to reuse the result of a complex expression multiple times. This can be done with the let-construct. You could for instance use a let-construct to simplify the expression (3+4)*2+(3+4) to let y:=3+4 in y*2+y. This helps the readability of your expressions. You can also introduce multiple new symbols in a let-construct if you separate them with a semicolon. The order in which these symbols are introduced again does not matter.
A let-construct can introduce shadowing. When you locally define an identifier which was in scope already. The outer-scoped one is hidden and unreachable in the inner expressions.
The other way around
Unlike simple calculators, FMS allows you to solve equations with multiple solutions. For this we use variables that can take a range of possible values, and constraints (equations) over these variables.
Declaring a ranged variable is done through name :: element of setExpression. For now we only introduce two kinds of sets (ranges):
- Contiguous ranges of integers. A range from
atobcan be written down as{a..b}. - Enumerations. The enumeration of a few constants like
{1,2,8,6}.
Then, you can write down the constraints which should hold. All global variables occurring in a constraint are considered relevant, so we do not have to explicitly state this anymore.
Using constraints, it possible to have multiple results. By default all possible results are printed. If you want to override this you can use the statement nbModels n at the top of your file, where the n represents the number of solutions you are interested in. If you set n to 0 it means that you are interested in all solutions.
Note that for constraints we use the equals symbol = instead of the definitional equality :=.
Optimization
When there are multiple solutions it is possible that you're interested in an optimal one according to a certain criterion. For this you can add an optimization statement: $minimize or $maximize with a term which needs to be optimized.
In this case multiple solutions will still be printed. But each subsequent solution is guaranteed to be better than the previous one.
More than numbers
Strings
FMS also supports strings between double quotes wherever you write a number. The standard lexicographic order applies when comparing strings.
Booleans
The Boolean values true and false are available through the standard library. You can introduce a Boolean variable as a proposition through p :: proposition.
This behaves just like p :: element of {true,false}, but it allows for a more efficient implementation.
Constraints over propositions can be written with logical connectives | (or), & (and), ~ (not), => <= (implies), <=> (if and only if).