Merge pull request #555 from conjure-cp/docfix-20230401

fix #522, also clarify text

docs/refs.bib

@@ -95,7 +95,7 @@ @inproceedings{c341e68df4c14ab5b77b0693aa1cc90f
   title = {A framework for generating informative benchmark instances},
   abstract = {Benchmarking is an important tool for assessing the relative performance of alternative solving approaches. However, the utility of benchmarking is limited by the quantity and quality of the available problem instances. Modern constraint programming languages typically allow the specification of a class-level model that is parameterised over instance data. This separation presents an opportunity for automated approaches to generate instance data that define instances that are graded (solvable at a certain difficulty level for a solver) or can discriminate between two solving approaches. In this paper, we introduce a framework that combines these two properties to generate a large number of benchmark instances, purposely generated for effective and informative benchmarking. We use five problems that were used in the MiniZinc competition to demonstrate the usage of our framework. In addition to producing a ranking among solvers, our framework gives a broader understanding of the behaviour of each solver for the whole instance space; for example by finding subsets of instances where the solver performance significantly varies from its average performance.},
   keywords = {Instance generation, Benchmarking, Constraint programming},
-  author = {Nguyen Dang and {\"O}zg{\"u}r Akg{\"u}n and {Espasa Arxer}, Joan and Miguel, {Ian} and Peter Nightingale},
+  author = {Nguyen Dang and {\"O}zg{\"u}r Akg{\"u}n and {Espasa}, Joan and Miguel, {Ian} and Peter Nightingale},
   year = {2022},
   month = {jul},
   day = {23},
@@ -184,7 +184,7 @@ @inproceedings{5d418525265e4c2189449a84ef9db61e
   title = {Effective encodings of constraint programming models to SMT},
   abstract = {Satisfiability Modulo Theories (SMT) is a well-established methodology that generalises propositional satisfiability (SAT) by adding support for a variety of theories such as integer arithmetic and bit-vector operations. SMT solvers have made rapid progress in recent years. In part, the efficiency of modern SMT solvers derives from the use of specialised decision procedures for each theory. In this paper we explore how the Essence Prime constraint modelling language can be translated to the standard SMT-LIB language. We target four theories: bit-vectors (QF_BV), linear integer arithmetic (QF_LIA), non-linear integer arithmetic (QF_NIA), and integer difference logic (QF_IDL). The encodings are implemented in the constraint modelling tool Savile Row. In an extensive set of experiments, we compare our encodings for the four theories, showing some notable differences and complementary strengths. We also compare our new encodings to the existing work targeting SMT and SAT, and to a well-established learning CP solver. Our two proposed encodings targeting the theory of bit-vectors (QF_BV) both substantially outperform earlier work on encoding to QF_BV on a large and diverse set of problem classes.},
   keywords = {Constraint modelling, SMT, Automated reformulation},
-  author = {Ewan Davidson and {\"O}zg{\"u}r Akg{\"u}n and {Espasa Arxer}, Joan and Peter Nightingale},
+  author = {Ewan Davidson and {\"O}zg{\"u}r Akg{\"u}n and {Espasa}, Joan and Peter Nightingale},
   year = {2020},
   doi = {10.1007/978-3-030-58475-7_9},
   language = {English},

docs/tutorials/BIBD.rst

@@ -11,7 +11,7 @@ The Problem
 
 Balanced Incomplete Block Design (BIBD) is a problem from the field of experimental design. It is best explained with an example.
 
-Emily wants to establish which crops (🥔,🌽,🥦,🥕,🥒, 🍅) grow best in Scotland. She has recruited 4 farmers who are happy to help by growing some of the crops. Unfortunately none of the farmers have enough space to grow every crop, they can each grow 3 different crops. Emily is concerned that the different environment of each farm may impact the crops growth. Therefore she wants to make sure that each farmer grows a different combination of crops and that every crop has been grown in the same number of different farms. This approach is called Balanced Incomplete Block Design (BIBD).
+Emily wants to establish which crops (🥔, 🌽, 🥦, 🥕, 🥒, 🍅) grow best in Scotland. She has recruited 4 farmers who are happy to help by growing some of the crops. Unfortunately none of the farmers have enough space to grow every crop, they can each grow 3 different crops. Emily is concerned that the different environment of each farm may impact the crops growth. Therefore she wants to make sure that each farmer grows a different combination of crops and that every crop has been grown in the same number of different farms. This approach is called Balanced Incomplete Block Design (BIBD).
 
 We can build a model to tell us the crops that each farm should grow.
 
@@ -21,24 +21,24 @@ We need to specify the crops, the number of farms, the number of crops that can
 
 Emily has decided that she wants each crop to be grown in 2 different farms, and that each pair of farmers will have 1 crop in common.
 
-Essence will take a .param file containing the values of the initial parameters. In the .param file we should define the parameters:
+Essence will take a ``.param`` file containing the values of the initial parameters. In the ``.param`` file we should define the parameters:
 
 .. code-block:: essence
 
-  letting crops be new type enum {🥔,🌽,🥦,🥕,🥒, 🍅}
+  letting crops be new type enum {🥔, 🌽, 🥦, 🥕, 🥒, 🍅}
   letting farms be 4
   letting crops_per_farm be 3
   letting farms_per_crop be 2
   letting overlap be 1
 
-The model will be in a .essence file. It should start by accessing the provided parameters, this uses the given keyword, followed by the names of the parameters and their type.
+The model will be in a ``.essence`` file. It should start by accessing the provided parameters, this uses the ``given`` keyword, followed by the names of the parameters and their type.
 
 .. code-block:: essence
 
   given farms, crops_per_farm, farms_per_crop, overlap: int
   given crops new type enum
 
-Next, we need to define what we are looking for. The 'find' keyword indicates that the solver should find a value to for that variable. We want to find a set containing sets of crops. Each set of crops is a crop assignment for a farm.
+Next, we need to define what we are looking for. The ``find`` keyword indicates that the solver should find a value for that variable. We want to find a set containing sets of crops. Each set of crops is a crop assignment for a farm.
 
 .. code-block:: essence
 
@@ -47,7 +47,7 @@ Next, we need to define what we are looking for. The 'find' keyword indicates th
 
   find crop_assignment: set of set of crops
 
-Once the parameters and ***targets?** of the model have been defined, we should define the constraints. ``such that`` indicates the start of the constraints.
+Once the parameters and decision variables of the model have been defined, we should define the constraints. ``such that`` indicates the start of the constraints.
 
 .. code-block:: essence
 
@@ -64,7 +64,7 @@ Result::
 
 With no constraints it produces an empty set for crop assignment.
 
-The first, basic, constraints is the number of farms. The number of sets in the crop_assignment set should equal the numbers of farms. ``|crop_assignment|`` indicates the size of the crop_assignment set. By setting the size equal to the number of farms (after the such that keyword) the solver will only produce solutions where the size of the set is the same as the number of farms.  A comma on the end of line indicates that there are more constraints to follow.
+The first, basic, constraint is the number of farms. The number of sets in the ``crop_assignment`` set should equal the number of farms. ``|crop_assignment|`` indicates the size of the ``crop_assignment`` set. By setting the size equal to the number of farms (after the ``such that`` keyword) the solver will only produce solutions where the size of the set is the same as the number of farms.  A comma separates constraints, so at the end of a line this indicates that there are more constraints to follow (none for the moment).
 
 .. code-block:: essence
 
@@ -108,7 +108,7 @@ Result::
    {🥦, 🥒, 🍅},
    {🥕, 🥒, 🍅}}
 
-The model now has the correct number of farms and assigns the correct number of crops per farms, but doesn't assign all types of crops.
+The model now has the correct number of farms and assigns the correct number of crops per farm, but doesn't assign all types of crops.
 
 The next constraint is number of farms with a given crop. This is more complex than the previous constraints. Let's go over it step by step.
 For every crop we need to find the number of farms assigned that crop and set it to equal the parameter Emily chose for farms per crop. In order to find this we first use a ``forAll`` to apply the constraint to every crop. ``forAll crop : crops . [OurCalculation] = farms_per_crop``
@@ -137,11 +137,11 @@ Result::
 
 Our model now produces a crop assignment that assigns the correct number of crops to each farmer and the correct number of crops in total but there is lot of overlap between the first and second farmer and between the third and fourth farmer but very little overlap between the two pairs. This is why Emily specified the overlap constraint (sometimes called lambda in BIBD models). In order to make sure that every pair of farmers have at least 1 crop in common we need to define another constraint.
 
-We need to check every pair of farms, we can do this by using two ``forAll`` keywords (``forAll farm1 in crop_assignment. forAll farm2 in crop_assignment . [OurConstraint]``). We can then use the ``intersect`` keyword to get all crops that the two farms have in common. The ``||`` notation can be used to get the size of the intersect which we can then set equal to the overlap parameter (``|farm1 intersect farm2| = overlap``).
+We need to check every pair of farms, we can do this by using two ``forAll`` keywords (``forAll farm1 in crop_assignment. forAll farm2 in crop_assignment . [OurConstraint]``). We can then use the ``intersect`` keyword to get all crops that the two farms have in common, and require the size of this intersection to be equal to the overlap parameter (``|farm1 intersect farm2| = overlap``).
 
-However, running the model at this point produces no solutions, as iterating over the crop_assignment in this way means that sometimes farm1 and farm2 will be the same farm, so the intersection will be the number of crops assigned to the farm (3) and never be 1 (the overlap parameter), resulting in no valid solutions.
+However, running the model at this point produces no solutions, as iterating over the ``crop_assignment`` in this way means that sometimes ``farm1`` and ``farm2`` will be the same farm, so the intersection will be the number of crops assigned to the farm (3) and never be 1 (the overlap parameter), resulting in no valid solutions.
 
-In order to avoid this we need to add an further condition to the constraint which checks they are not the same farm before applying the constraint. ``->`` is used, where the left hand side has a condition and the right hand side has a constraint which is only used if the left hand side is true. ``farm1 != farm2 -> |farm1 intersect farm2| = overlap``
+In order to avoid this we need to add a further condition to the constraint which checks they are not the same farm before applying the constraint. ``->`` is used, where the left hand side has a condition and the right hand side has a constraint which is only used if the left hand side is true. ``farm1 != farm2 -> |farm1 intersect farm2| = overlap``
 
 
 .. code-block:: essence
@@ -189,7 +189,7 @@ There is a nicer way to do the final constraint, instead of using a second ``for
 
 
 
-Providing information in the find statements rather than as constraints often leads to better perform. Essence provides domain attributes which can be attached to find statements . One of them is size k, which tells Essence that a set is of size k. In our model the number of farms and the number of crops per farm are in effect the size of the crop_assignment set and the size of the sets within the crop_assignment set. Therefore we can move these definitions out of the list of constraints and into the find statement.
+Providing information in the ``find`` statements rather than as constraints often leads to better performance. Essence provides domain attributes which can be attached to ``find`` statements . One of them is ``size k``, which tells Essence that a set is of size ``k``. In our model the number of farms and the number of crops per farm are in effect the size of the ``crop_assignment`` set and the size of the sets within the ``crop_assignment`` set. Therefore we can move these definitions out of the list of constraints and into the ``find`` statement.
 
 .. code-block:: essence