Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Avoid the use of "no <dummy>"

Browse Source
This commit is contained in:
Jip J. Dekker 2021-07-25 14:22:45 +10:00
parent 4b007951a5
commit 4e91fa20a3
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
9 changed files with 257 additions and 249 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

343
.vscode/ltex.hiddenFalsePositives.en-GB.txt vendored
View File

@ -1,179 +1,186 @@
{"rule":"EN_A_VS_AN","sentence":"^\\QOnce given a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the Dummies, the forms an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAs an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, our goal is to find a schedule that minimises the finishing time of the last task.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAs an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, our goal is to find a schedule that minimizes the finishing time of the last task.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q shows an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model for the open shop problem.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo create an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the problem, the user provides the number of jobs and machines that are considered, and the duration of each task.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model of the open shop problem\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAdditionally, the process to encode an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q all happens “behind the scenes”.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QOnce given a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the Dummies, the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q forms an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QUsing the same mechanism, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defines how an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is encoded for a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qsupport incremental usage of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThen, we describe a technique to optimize the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q process for incremental changes to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qavar name=auxiliary variable, description= A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q not explicitly defined in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, but rather introduced in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qbyte-code name=byte-code, description=A set of instructions designed to be efficiently executed by an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTogether with a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q forms an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-api name=Application Programming Interface (API), description= A particular set of rules and specifications that a software program can follow to access and make use of the services and resources provided by another particular software program that implements that API ,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qcvar name=control variable, description= A special form of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represent the result of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q ,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q formed with an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model is then rewritten into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qincremental-rewriting name=incremental-rewriting, description=The \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is continuously changed,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qint-sol name=intermediate solution, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is not (yet) proven to be the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qmodel name=constraint model, description= A formalization of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q or an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt is defined in terms of formalized decision, Dummies of different kinds (e.g. Boolean, integers, or even sets), and Dummies, Boolean logic formulas which are forced to hold in any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and, in case of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe combination of a constraint model and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Qs for its Dummies is said to be an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the constraint model ,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qnanozinc name=NanoZinc, description=A language to represent the current state of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q during \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor such a problem, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with the highest quality ,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qopt-sol name=optimal solution, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for which it has been proven that no other \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q exist of higher quality,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qsol name=solution, description=A complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that all Dummies are satisfied,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QSimilarly, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is said to be partial when it maps only a subset of the Dummies and Dummies in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThey can be used as immutable data used to define Dummies or provide structural information about an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor example, a problem parameter can influence the number of Dummies in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q ,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qrewriting name=rewriting, description= The process of transforming a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is referred to as rewriting.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qaggregation name=constraint aggregation, description=A technique that combines many smaller Dummies into a one or, by exception, a few larger Dummies,\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-ampl name=AMPL: A Mathematical Programming Language, description=AMPL is a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q originally designed to serve as a common input language for mathematical Dummies (e.g. \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q).\\E$"}
{"rule":"A_NNS","sentence":"^\\QFrom these cities it declares a set Paths that contains all possible paths between the different cities.\\E$"}
{"rule":"CD_NN","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q visualizes the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q after placing a queen on the d3 square of an eight by eight chessboard.\\E$"}
{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Qgls-api name=Application Programming Interface (API), description= A particular set of rules and specifications that a software program can follow to access and make use of the services and resources provided by another particular software program that implements that API ,\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qdblp computer science bibliography, https://dblp.org\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA specific problem is captured by an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the combination of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q (i.e. a mapping from all Dummies to values).\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA specific problem is captured by an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the combination of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q (i.e. a mapping from all Dummies to a value).\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QMany Dummies also support the modelling of Dummies, where a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is augmented with an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QThe following set of equations describes this “knapsack” problem as an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q:\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe following set of equations describes this “knapsack” problem as an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q:\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QA \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing a 0-1 knapsack problem\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Q[\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] there has been no \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q yet; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q was \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q found a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q found and proved an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q did not find a solution, but did not exhaust its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Q[\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the Dummies that satisfies the Dummies, [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the Dummies that satisfies the Dummies and minimises the value of the expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, or [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] to similarly maximise the value of the expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Q[\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the Dummies that satisfies the Dummies, [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the Dummies that satisfies the Dummies and minimizes the value of the expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, or [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] to similarly maximise the value of the expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Q[\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the Dummies that satisfies the Dummies, [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the Dummies that satisfies the Dummies and minimizes the value of the expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, or [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] to similarly maximize the value of the expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe other two types of goals are used when the model describes an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QThis \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expresses the knapsack relation, with the following arguments: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q are the weights of the items, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q are the profits for each item, the Dummies in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represent how many of each item are present in the knapsack, and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, respectively, represent the weight and profit of the knapsack\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QThis has the additional benefit that the knapsack structure of the problem is then known.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QInstead, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is created and a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is added to ensure that it takes the correct value.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q shows an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model for the open shop problem.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q formed with an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model is then rewritten into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA modeller can repeatedly add Dummies and Dummies to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and, crucially, the additions to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can be retracted in reverse order through the use of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA single \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, however, is negatively impacted by the change; an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for this \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is no longer found.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA specific problem is captured by an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the combination of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q (i.e. a mapping from all Dummies to a value).\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA specific problem is captured by an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the combination of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q (i.e. a mapping from all Dummies to values).\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA universal approach to the incremental usage of Dummies, and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, is to allow incremental changes to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAdditionally, the process to encode an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q all happens “behind the scenes”.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAlthough \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q does not typically prescribe a way to find the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, it provides the modeller with a way to give “hints” to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is continuously updated with new data, such as newly available jobs to be scheduled or customer requests to be processed.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing the \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing the job shop problem, abstracting from \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q declarations.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing the social golfer problem\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model of the open shop problem\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model can be rewritten by Saville Row into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for a variety of Dummies, including \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAs an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, our goal is to find a schedule that minimises the finishing time of the last task.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAs an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, our goal is to find a schedule that minimizes the finishing time of the last task.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qavar name=auxiliary variable, description= A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q not explicitly defined in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, but rather introduced in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qbyte-code name=byte-code, description=A set of instructions designed to be efficiently executed by an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QConsider for example the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q operator on integers, which \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represents as an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q call.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qcvar name=control variable, description= A special form of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represent the result of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q ,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QDifferent from the rules described, when an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q access or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression is found in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context, it often makes sense to evaluate its sub-expression in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context as well.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFirst, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model is transformed into \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we can then create a simple \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q program that calls \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor example, a problem parameter can influence the number of Dummies in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q ,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor example, the following function returns an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is constrained to be the multiplication of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q by the relational multiplication \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor many \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies this model is close to a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, since integer Dummies and an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q are common.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor many problems the use of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies offers a very successful method to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to a problem.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor problems that are in the form of a linear program, there are proven methods to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor such a problem, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with the highest quality ,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor the selection of an element from an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q language uses an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q access syntax similar to most other computer languages.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor this comparison compare the time that is required to (repeatedly) rewrite an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the time required by the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QHow is an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q transformed into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q?\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QHowever, when it finds a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, it does not yet know if this \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIf any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q was found, it is declared an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIf the Dummies happen to take integer values in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, then we have found an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the mixed integer program.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIf the expression is a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, then the expression is rewritten to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIn the frontend, a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model is combined with its data into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIn this section we extend our architecture with an incremental constraint modelling interface that allows the modeller to change an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qincremental-rewriting name=incremental-rewriting, description=The \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is continuously changed,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QInitially, the search is in stage one: it tries to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for the first \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QInstead, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is created and a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is added to ensure that it takes the correct value.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QInstead, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q must be created to represent the value of the sub-expression, and it must be constrained to take the value corresponding to the expression.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qint-sol name=intermediate solution, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is not (yet) proven to be the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt can read Dummies from a file or via an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt can rewrite (and propagate) an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q multiple times, remembering information about the earlier iteration(s).\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt is an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt is defined in terms of formalized decision, Dummies of different kinds (e.g. Boolean, integers, or even sets), and Dummies, Boolean logic formulas which are forced to hold in any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and, in case of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt is, again, possible to rewrite a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q as a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QLike an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the aim of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is to find the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the problem.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QMany Dummies also support the modelling of Dummies, where a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is augmented with an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qmodel name=constraint model, description= A formalization of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q or an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qnanozinc name=NanoZinc, description=A language to represent the current state of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q during \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QOnce given a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the Dummies, the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q forms an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QOnce given a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the Dummies, the forms an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qopt-sol name=optimal solution, description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for which it has been proven that no other \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q exist of higher quality,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qrewriting name=rewriting, description= The process of transforming a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is referred to as rewriting.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QSimilarly, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is said to be partial when it maps only a subset of the Dummies and Dummies in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QSince we then cannot decide during \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if an element is present in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the elements are made of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q type.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Qsol name=solution, description=A complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that all Dummies are satisfied,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model for this problem contains an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q lookup \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, where the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is larger than the index set of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model is unable to use a set of partitions and instead uses an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of sets.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem is analogous to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q process of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q then consists of two steps: the translation of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model transformations into \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, implemented by a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; and the iterative \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q using these \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q transformations to arrive at a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, implemented using an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q required to translate an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q was negligible.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe combination of a constraint model and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Qs for its Dummies is said to be an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the constraint model ,\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe context may depend on data that is only known at an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q level.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe following example constructs an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that contains the tripled even values of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe following set of equations describes this “knapsack” problem as an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q:\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe goal in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem is then to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for Boolean Dummies that maximizes the cumulative weights of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q clauses.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe goal of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q process is to arrive at a flat \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that only contains Dummies that consist of a singular calls, all arguments to calls are \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q literals or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q identifiers, and using only Dummies and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q types that are \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the target \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe instance is parsed into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe mapping ensures that the context is correctly transformed when accessing the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q table for an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q call.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe other two types of goals are used when the model describes an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe problem asks if there is an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for the Dummies of a given Boolean formula, such that the formula is \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe selection of an element from an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is in many way similar to the choice in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe selection of an element from an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is in many ways similar to the choice in a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIf the expression is a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, then the expression is rewritten to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe following example constructs an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that contains the tripled even values of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QSince we then cannot decide during \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if an element is present in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the elements are made of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q type.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor example, the following function returns an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that is constrained to be the multiplication of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q by the relational multiplication \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAlthough \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q does not typically prescribe a way to find the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, it provides the modeller with a way to give “hints” to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThrough the use of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q on the solving goal item, the modeller can express an order in which they think values should be tried for an arrangement of Dummies in the model.\\E$"}
{"rule":"I_LOWERCASE","sentence":"^\\QSuppose the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q a has index set \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, but i takes the value seven.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QWhen given an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, one may wonder how to find a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTherefore, a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for one \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q looks very different from an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for a different \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor many \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies this model is close to a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, since integer Dummies and an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q are common.\\E$"}
{"rule":"CD_NN","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q visualizes the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q after placing a queen on the d3 square of an eight by eight chessboard.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QPropagate the downward diagonal.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QHowever, when it finds a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, it does not yet know if this \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt is an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qmaximize \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q subject to \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor problems that are in the form of a linear program, there are proven methods to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QWe do this by treating the mixed integer program as a linear program and find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIf the Dummies happen to take integer values in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, then we have found an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the mixed integer program.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo solve an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, it can be rewritten into a mixed integer program.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgiven \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q maximise \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q subject to \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgiven \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q maximize \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q subject to \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe problem asks if there is an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for the Dummies of a given Boolean formula, such that the formula is \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo solve the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem, the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q has to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for the Dummies where at least one literal is true in every clause.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgiven \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q find \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Qtrue \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q,false \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Qsubject to \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe goal in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem is then to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for Boolean Dummies that maximizes the cumulative weights of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q clauses.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem is analogous to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QLike an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the aim of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is to find the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the problem.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt is, again, possible to rewrite a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q as a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor many problems the use of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies offers a very successful method to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to a problem.\\E$"}
{"rule":"THE_SUPERLATIVE","sentence":"^\\QThe goal of the problem is to find a shortest path that visits all the cities exactly once and returns to its origin.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing the \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"A_NNS","sentence":"^\\QFrom these cities it declares a set Paths that contains all possible paths between the different cities.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing the job shop problem, abstracting from \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q declarations.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QDummies of this type are influenced by the ScheduleHorizon \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined on \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the model.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe makespan \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represents the time spanned by all tasks.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QOn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q a UnaryResource is declared for every machine.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QA UnaryResource can be used by at most one activity at a time.\\E$"}
{"rule":"PREPOSITION_VERB","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q uses the requires operator to bind an activity to a resource.\\E$"}
{"rule":"PREPOSITION_VERB","sentence":"^\\QIt first states the resource objects and then merely has to use the requires keyword to force tasks on the same machine to be mutually exclusive.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing the social golfer problem\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model is unable to use a set of partitions and instead uses an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of sets.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFirst, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model is transformed into \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThen, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model forms an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and is subsequently rewritten into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model can be rewritten by Saville Row into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for a variety of Dummies, including \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIn the frontend, a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model is combined with its data into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe instance is parsed into an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe goal of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q process is to arrive at a flat \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that only contains Dummies that consist of a singular calls, all arguments to calls are \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q literals or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q identifiers, and using only Dummies and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q types that are \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the target \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QInstead, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q must be created to represent the value of the sub-expression, and it must be constrained to take the value corresponding to the expression.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QUsing a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the function body explicitly creates an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, constrains it to take to correct value, and then returns it.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt can rewrite (and propagate) an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q multiple times, remembering information about the earlier iteration(s).\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QHow is an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q transformed into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q?\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q required to translate an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q was negligible.\\E$"}
{"rule":"IT_IS","sentence":"^\\QWe design and evaluate an architecture for Dummies that can accommodate its the modern uses.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe machine operates using an Intel Xeon 8260 \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which has 24 non-hyperthreaded cores, and has access to 268.55 GB of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qis an open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qis an open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q solver \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qis a proprietary \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qis a open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qaccap amaze city-position community-detection depot-placement freepizza groupsplitter kidney-exchange multi-knapsack nonogram nside rcpsp-wet road-cons roster stack-cuttingstock steelmillslab triangular\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QIt presents an analysis technique to reason about in what (\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q) form Dummies should be considered.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QIt presents a design and implementation of techniques to automatically introduce \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of Dummies in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QIt develops a technique to simplify Dummies by efficiently eliminating Dummies.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QIt proposes two novel methods to reduce the overhead of using Dummies in incremental techniques: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of changing Dummies.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe first rule, (Ident), is unique in the sense that the context of an identifier does not directly affect other expressions.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QInstead, we introduce the functions “pushCtx” and “collectCtx”.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAs an input to the inference process, a “argCtx” function is used to give the context of the arguments of a function, given the function itself and the context of the call.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAlthough a standard definition for the “argCtx” function may cover the most common cases, it does not cover user-defined functions.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QDefinition of the “argCtx” function for operators.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QFinally, the (Compr) and (Arr) rules show simple inference rules for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q construction expressions.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAs previously discussed, the contexts in which the identifier was used can be retrieved using the “collectCtx” function.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qjoin A table showing the result of joining two contexts.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q(TupC) and (TupD) handle the context inference during the construction and destructuring of tuples respectively.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QFinally, the (Decl) and (Item0) rules describe two base cases in the inference.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QDifferent from the rules described, when an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q access or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression is found in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context, it often makes sense to evaluate its sub-expression in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context as well.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo detect the situation where the sub-expression are only used in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q access or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression we introduce the context.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qjoin The join context operation extended with .\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo detect the situation where the sub-expression are only used in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q access or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression we introduce the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qjoin The join context operation extended with \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qthe disjunction itself is in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q are in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context, and the rest are in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qafter which b2 can be removed from the model.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QConsider for example the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q operator on integers, which \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represents as an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q call.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe mapping ensures that the context is correctly transformed when accessing the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q table for an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q call.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe context may depend on data that is only known at an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q level.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model for this problem contains an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q lookup \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, where the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is larger than the index set of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA single \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, however, is negatively impacted by the change; an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for this \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is no longer found.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q process of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q then consists of two steps: the translation of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model transformations into \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, implemented by a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; and the iterative \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q using these \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q transformations to arrive at a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, implemented using an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qa \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that translates \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q models to a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that produces a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA modeller can repeatedly add Dummies and Dummies to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and, crucially, the additions to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can be retracted in reverse order through the use of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QSolver Unsatisfiable Optimal Solution Satisfied Unk.\\E$"}
{"rule":"WHITESPACE_RULE","sentence":"^\\Q[main]\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[label=ownpubs]assets/bibliography/dekker_publications.bib\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcontinuously updating \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for known Dummies, specialised Dummies when variables get \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, common sub-expression elimination, and removing Dummies and Dummies that are no longer required.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcontinuously updating \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for known Dummies, specialized Dummies when variables get \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, common sub-expression elimination, and removing Dummies and Dummies that are no longer required.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTogether, the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q form an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that can be executed by the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThe translation to \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q turns all expressions into function calls, replaces the special generator syntax in the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and creates the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q function.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, we can then create a simple \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q program that calls \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThen, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model forms an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and is subsequently rewritten into a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThen, we describe a technique to optimize the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q process for incremental changes to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTherefore, a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for one \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q looks very different from an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for a different \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThese are said to be the “root-context” Dummies of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, i.e. those that have to hold globally and are not just used to define an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (CallBuiltin) rule applies to “built-in” functions that can be evaluated directly, such as arithmetic and Boolean operations on fixed values.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (CallNative) rule applies to calls to \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q functions, that describe relations, that have been marked as Dummies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QDummies that follow from the evaluation of the let expression, by the (ItemC) rule, are collected in the third component, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q , of the evaluation arguments.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QDummies that follow from the evaluation of the let expression, by the (ItemC) rule, are collected in the third component, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, of the evaluation arguments.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (ItemT) rule handles introduction of new Dummies by adding them to the context.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (ItemTE) rule handles introduction of new Dummies with a defining equation by evaluating them in the current context and substituting the name of the new \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q by the result of evaluation in the entire scope of the variable.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe rules (ItemTupC) and (ItemTupD) are for the construction and deconstruction of tuple objects.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (Ident) rule looks up a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in the environment and returns the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q itself to be used in any Dummies.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (Const) rule simply returns the constant.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (Acess) rule evaluates the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the index \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (WhereT) rule evaluates the guard of a where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and if true returns the resulting expression in a list.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (WhereF) rule evaluates the guard and when false returns an empty list.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (ListG) rule evaluates the iteration set \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to get its value \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which must be fixed.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIt can read Dummies from a file or via an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QIn this thesis we will follow the same naming standard as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, where a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q has the same name as the original \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with reif appended.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qthe variable \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q variables \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q multiplication Dummies.\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QThe removal of unused identifiers is taken care of by garbage collection in the interpreter.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAny annotated \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is handled by the (CallNative) rule rather than the (Call) rule, which means that it is simply added as a call into the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q code, without evaluating its body.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is continuously updated with new data, such as newly available jobs to be scheduled or customer requests to be processed.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qallow us to express important aspects of the meta-optimization algorithm in a more convenient way, and enable a simple \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q scheme that requires no additional communication with and only small, simple extensions of the target \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Q[\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] there has been no \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q yet; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q was \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q found a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q found and proved an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q did not find a solution, but did not exhaust its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIf any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q was found, it is declared an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QInitially, the search is in stage one: it tries to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for the first \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QCalls to the random number functions have been renamed by appending slv, so that they are not simply evaluates directly.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA universal approach to the incremental usage of Dummies, and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, is to allow incremental changes to an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIn this section we extend our architecture with an incremental constraint modelling interface that allows the modeller to change an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qthe addition or removal of new Dummies or Dummies, changes made to the Dummies of Dummies, additions to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q table, and substitutions made due to equality \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QFor this comparison compare the time that is required to (repeatedly) rewrite an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the time required by the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QWe ran experiments for three models from the MiniZinc Challenge \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q (gbac, steelmillslab, and rcpsp-wet).\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThey can be used as immutable data used to define Dummies or provide structural information about an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QThrough the use of an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q on the solving goal item, the modeller can express an order in which they think values should be tried for an arrangement of Dummies in the model.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo create an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the problem, the user provides the number of jobs and machines that are considered, and the duration of each task.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo detect the situation where the sub-expression are only used in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q access or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression we introduce the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo detect the situation where the sub-expression are only used in an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q access or \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression we introduce the context.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo solve an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, it can be rewritten into a mixed integer program.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTo solve the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q problem, the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q has to find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for the Dummies where at least one literal is true in every clause.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTogether with a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q forms an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QTogether, the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and a complete \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q form an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that can be executed by the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QUsing a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the function body explicitly creates an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, constrains it to take to correct value, and then returns it.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QUsing the same mechanism, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defines how an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is encoded for a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QWe compare our methods against a naive system that repeatedly programmatically changes an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, rewrites the full Dummies, and starts a new \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q instance.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QWe compare the time that is required to (repeatedly) rewrite an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the time taken by the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QWe do this by treating the mixed integer program as a linear program and find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QWhen given an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, one may wonder how to find a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QA \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q model describing a 0-1 knapsack problem\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QThe following set of equations describes this “knapsack” problem as an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q:\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QThe removal of unused identifiers is taken care of by garbage collection in the interpreter.\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QThis \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expresses the knapsack relation, with the following arguments: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q are the weights of the items, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q are the profits for each item, the Dummies in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represent how many of each item are present in the knapsack, and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, respectively, represent the weight and profit of the knapsack\\E$"}
{"rule":"EN_GB_SIMPLE_REPLACE","sentence":"^\\QThis has the additional benefit that the knapsack structure of the problem is then known.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QIt develops a technique to simplify Dummies by efficiently eliminating Dummies.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QIt presents a design and implementation of techniques to automatically introduce \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of Dummies in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QIt presents an analysis technique to reason about in what (\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q) form Dummies should be considered.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QIt proposes two novel methods to reduce the overhead of using Dummies in incremental techniques: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of changing Dummies.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_BEGINNING_RULE","sentence":"^\\QPropagate the downward diagonal.\\E$"}
{"rule":"I_LOWERCASE","sentence":"^\\QSuppose the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q a has index set \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, but i takes the value seven.\\E$"}
{"rule":"IT_IS","sentence":"^\\QWe design and evaluate an architecture for Dummies that can accommodate its the modern uses.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q(TupC) and (TupD) handle the context inference during the construction and destructuring of tuples respectively.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[label=ownpubs]assets/bibliography/dekker_publications.bib\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QA UnaryResource can be used by at most one activity at a time.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qaccap amaze city-position community-detection depot-placement freepizza groupsplitter kidney-exchange multi-knapsack nonogram nside rcpsp-wet road-cons roster stack-cuttingstock steelmillslab triangular\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAlthough a standard definition for the “argCtx” function may cover the most common cases, it does not cover user-defined functions.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAny annotated \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is handled by the (CallNative) rule rather than the (Call) rule, which means that it is simply added as a call into the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q code, without evaluating its body.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAs an input to the inference process, a “argCtx” function is used to give the context of the arguments of a function, given the function itself and the context of the call.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QAs previously discussed, the contexts in which the identifier was used can be retrieved using the “collectCtx” function.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QCalls to the random number functions have been renamed by appending slv, so that they are not simply evaluates directly.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qdblp computer science bibliography, https://dblp.org\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QDefinition of the “argCtx” function for operators.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QDummies of this type are influenced by the ScheduleHorizon \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined on \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the model.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QDummies that follow from the evaluation of the let expression, by the (ItemC) rule, are collected in the third component, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q , of the evaluation arguments.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QDummies that follow from the evaluation of the let expression, by the (ItemC) rule, are collected in the third component, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, of the evaluation arguments.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QFinally, the (Compr) and (Arr) rules show simple inference rules for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q construction expressions.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QFinally, the (Decl) and (Item0) rules describe two base cases in the inference.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-ampl name=AMPL: A Mathematical Programming Language, description=AMPL is a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q originally designed to serve as a common input language for mathematical Dummies (e.g. \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q).\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-api name=Application Programming Interface (API), description= A particular set of rules and specifications that a software program can follow to access and make use of the services and resources provided by another particular software program that implements that API ,\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QIn this thesis we will follow the same naming standard as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, where a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q has the same name as the original \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q with reif appended.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QInstead, we introduce the functions “pushCtx” and “collectCtx”.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QOn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q a UnaryResource is declared for every machine.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QSolver Unsatisfiable Optimal Solution Satisfied Unk.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (Acess) rule evaluates the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the index \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (CallBuiltin) rule applies to “built-in” functions that can be evaluated directly, such as arithmetic and Boolean operations on fixed values.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (CallNative) rule applies to calls to \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q functions, that describe relations, that have been marked as Dummies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (Const) rule simply returns the constant.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (Ident) rule looks up a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in the environment and returns the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q itself to be used in any Dummies.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (ItemT) rule handles introduction of new Dummies by adding them to the context.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (ItemTE) rule handles introduction of new Dummies with a defining equation by evaluating them in the current context and substituting the name of the new \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q by the result of evaluation in the entire scope of the variable.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (ListG) rule evaluates the iteration set \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to get its value \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which must be fixed.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (WhereF) rule evaluates the guard and when false returns an empty list.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe (WhereT) rule evaluates the guard of a where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and if true returns the resulting expression in a list.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe first rule, (Ident), is unique in the sense that the context of an identifier does not directly affect other expressions.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe machine operates using an Intel Xeon 8260 \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which has 24 non-hyperthreaded cores, and has access to 268.55 GB of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe makespan \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q represents the time spanned by all tasks.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe rules (ItemTupC) and (ItemTupD) are for the construction and deconstruction of tuple objects.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QWe ran experiments for three models from the MiniZinc Challenge \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q (gbac, steelmillslab, and rcpsp-wet).\\E$"}
{"rule":"PREPOSITION_VERB","sentence":"^\\QIt first states the resource objects and then merely has to use the requires keyword to force tasks on the same machine to be mutually exclusive.\\E$"}
{"rule":"PREPOSITION_VERB","sentence":"^\\QThe \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q uses the requires operator to bind an activity to a resource.\\E$"}
{"rule":"THE_SUPERLATIVE","sentence":"^\\QThe goal of the problem is to find a shortest path that visits all the cities exactly once and returns to its origin.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qa \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that translates \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q models to a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q that produces a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qafter which b2 can be removed from the model.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qaggregation name=constraint aggregation, description=A technique that combines many smaller Dummies into a one or, by exception, a few larger Dummies,\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qallow us to express important aspects of the meta-optimization algorithm in a more convenient way, and enable a simple \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q scheme that requires no additional communication with and only small, simple extensions of the target \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcontinuously updating \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for known Dummies, specialised Dummies when variables get \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, common sub-expression elimination, and removing Dummies and Dummies that are no longer required.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcontinuously updating \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for known Dummies, specialized Dummies when variables get \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, common sub-expression elimination, and removing Dummies and Dummies that are no longer required.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgiven \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q find \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Qtrue \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q,false \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Qsubject to \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgiven \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q maximise \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q subject to \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgiven \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q maximize \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q subject to \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qis a open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qis a proprietary \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qis an open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qis an open source \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q solver \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qjoin A table showing the result of joining two contexts.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qjoin The join context operation extended with .\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qjoin The join context operation extended with \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qmaximize \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q subject to \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qsupport incremental usage of the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qthe addition or removal of new Dummies or Dummies, changes made to the Dummies of Dummies, additions to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q table, and substitutions made due to equality \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qthe disjunction itself is in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q are in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context, and the rest are in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q context.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qthe variable \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q variables \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q multiplication Dummies.\\E$"}
{"rule":"WHITESPACE_RULE","sentence":"^\\Q[main]\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QOr, when this is not possible, prove that such an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q cannot exist.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QIf such an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q does not exist, then it reports that the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcontinuously updating \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Dummies, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for known Dummies, specialized Dummies when variables get \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, common sub-expression elimination, and removing Dummies and Dummies that are not required any longer.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QA single \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, however, is negatively impacted by the change; for this \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q it cannot find an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q any longer.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\QAlthough it does not prove the unsatisfiability of one instance any longer and slightly increases the number of solver errors, an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is found for five more instances.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qallow us to express important aspects of the meta-optimization algorithm in a more convenient way, and enable a simple \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q scheme that does not require any additional communication with and only small, simple extensions of the target \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"EN_A_VS_AN","sentence":"^\\Q[\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q has not been restarted yet; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q of the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q was \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q found a \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q found and proved an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q in its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q; [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] the last \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q did not find a solution, but did not exhaust its \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}

18
assets/glossary.tex
View File

@ -68,7 +68,7 @@
\newglossaryentry{bnb}{
name={branch and bound},
description={A search method to find a \gls{opt-sol}. After an initial \gls{sol} is found, the search continuously looks for \glspl{sol} for which the \gls{objective} will return a better value than the incumbent \gls{sol}. If it is proven that no such \gls{sol} exists, then the final incumbent \gls{sol} is a \gls{opt-sol}},
description={A search method to find a \gls{opt-sol}. After an initial \gls{sol} is found, the search continuously looks for \glspl{sol} for which the \gls{objective} will return a better value than the incumbent \gls{sol}. If it is such a \gls{sol} cannot exist, then the final incumbent \gls{sol} is a \gls{opt-sol}},
}
\newglossaryentry{byte-code}{
@ -84,7 +84,7 @@
\newglossaryentry{bounds-con}{
name={bounds consistent},
description={A \gls{propagator} is bounds consistent when it reduces the minimum and maximum values of \domains{} for which there is no possible \gls{variable-assignment} such that the \gls{constraint} is satisfied},
description={A \gls{propagator} is bounds consistent when it reduces the minimum and maximum values of \domains{} that do not occur in a \gls{sol}},
}
\newglossaryentry{gls-cbc}{
@ -144,7 +144,7 @@
\newglossaryentry{gls-clp}{
name={constraint logic programming},
description={An extension of logic programming to include the concepts of \gls{cp}. A constraint logic program manipulates a \gls{constraint} store to find relevant variants where no \gls{constraint} contained in the store is \gls{violated}. See \cref{subsec:back-clp}},
description={An extension of logic programming to include the concepts of \gls{cp}. A constraint logic program manipulates a \gls{constraint} store to find relevant variants where all \glspl{constraint} contained in the store are \gls{satisfied}. See \cref{subsec:back-clp}},
}
\newglossaryentry{gls-cp}{
@ -214,7 +214,7 @@
\newglossaryentry{domain-con}{
name={domain consistent},
description={A \gls{propagator} is domain consistent if it is able to remove all values from \domains{} for which there is no possible \gls{variable-assignment} such that the \gls{constraint} is satisfied},
description={A \gls{propagator} is domain consistent if it is able to remove all values from \domains{} that do not occur in a \gls{sol}},
}
\newglossaryentry{essence}{
@ -238,7 +238,7 @@
}
\newglossaryentry{flatzinc}{
name={Flat\-Zinc},
name={Flat\-Zinc},{}
description={A subset of \gls{minizinc} chosen to represent \glspl{slv-mod}. It is the standard format in which \gls{minizinc} communicates with its \glspl{solver}},
}
@ -379,7 +379,7 @@
\newglossaryentry{normal-form}{
name={normal form},
description={A \gls{trs} has reached its normal form when no more rewriting rules can be applied},
description={A \gls{trs} has reached its normal form when none of the rewriting rules can be applied},
}
\newglossaryentry{gls-mip}{
@ -443,7 +443,7 @@
\newglossaryentry{opt-sol}{
name={optimal solution},
description={A \gls{sol} in an \gls{opt-prb} for which it has been proven that no other \gls{sol} exist of higher quality},
description={A \gls{sol} in an \gls{opt-prb} for which it has been proven that other \gls{sol} of higher quality do not exist},
}
\newglossaryentry{restart}{
@ -625,7 +625,7 @@
\newglossaryentry{unsat}{
name={unsatisfiable},
description={A problem is unsatisfiable when there exists no possible for the problem},
description={An \gls{instance}, or a \gls{constraint}, is unsatisfiable when a \gls{sol} cannot exist. All possible \glspl{variable-assignment} would violate at least one \gls{constraint}},
}
\newglossaryentry{variable}{
@ -634,7 +634,7 @@
A formalized decision that is yet to be made.
When searching for a \gls{sol} a decision variable is said to have a certain \gls{domain}, which contains the values that the decision variable can still take.
If at any point the \gls{domain} is reduced to a single value, then the decision variable is said to be \gls{fixed}.
If, however, a decision variable has an empty \gls{domain}, then there is no value it can take that is consistent with the \glspl{constraint}
If, however, a decision variable has an empty \gls{domain}, then there does not exist a value that is consistent with the \glspl{constraint}
},
}

2
chapters/0_abstract.tex
View File

@ -8,7 +8,7 @@
Their use extends to areas such as scheduling, supply chain management, and transportation.
In the past, these languages served mainly as a standardized interface between different \solvers{}.
The \gls{rewriting} required to translate an \instance{} of a \cmodel{} into a \gls{slv-mod} was negligible.
However, \cmls{} have evolved to include functionality that is no longer directly supported by the target \solver{}.
However, \cmls{} have evolved to include functionality that is not directly supported by the target \solvers{}.
As such, the \gls{rewriting} process has become more important and complex.
\minizinc{}, one such language, was originally designed for constraint programming \solvers{}, whose \glspl{slv-mod} contain small number of highly complex \constraints{}.

10
chapters/1_introduction.tex
View File

@ -7,7 +7,7 @@ Many important and difficult problems in the real world are \glspl{dec-prb}.
We can think, for instance, about the decision on the country's rail timetable or the stand-by locations for ambulances in the region.
Formally, we define a \gls{dec-prb} as a set of \variables{} subject to a set of logical \constraints{}.
A \gls{sol} to such a problem is the \gls{assignment} of all \variables{} to values that abide by the logic of the \constraints{}.
These problems are also highly computationally complex: even with the fastest computers there is no simple way to find a solution.
These problems are also highly computationally complex: even with the fastest computers, finding a solution can take a long time.
They get even more complex when we consider \glspl{opt-prb}: if there are multiple solutions, then one may be preferred over the other.
But, although these problems are hard to solve, finding a (good) solution for these problems is essential in many walks of life.
@ -66,13 +66,13 @@ Finally, \lrefrange{line:intro:con:start}{line:intro:con:end} express the \const
The \glsxtrshort{ampl} model provides a clear definition of the problem class, but it can be argued that its meaning is hard to decipher.
\glsxtrshort{ampl} does not provide any way to capture common concepts, such as one task preceding another or that two tasks cannot overlap in our example.
Additionally, the process to encode an \instance{} into a \gls{slv-mod} all happens ``behind the scenes''.
There is no way for a \solver{} to specify how, for example, an operator is best rewritten.
The \solver{} cannot specify how, for example, an operator is best rewritten.
As such, \glsxtrshort{ampl} cannot rewrite all models for all its \solvers{}.
For example, since the model in \cref{lst:intro-open-shop} uses the \mzninline{or} operator, it can only be encoded for \solvers{} that support \glsxtrshort{ampl}'s \gls{cp} interface.
Although they do support the rewriting of models between different problem classes, other \cmls{}, such as \gls{essence} \autocite{frisch-2007-essence} and \glsxtrshort{opl} \autocite{van-hentenryck-1999-opl}, exhibit the same problems.
They do not provide any way to capture common concepts.
And, apart from changing the implementation of \glsxtrshort{opl} or \gls{essence}, there is no way for a \solver{} to influence their preferred encoding.
And, apart from changing the implementation of \glsxtrshort{opl} or \gls{essence}, the \solver{} is unable to influence their preferred encoding.
\gls{clp}, as used in the Prolog language, offers a very different mechanism to create a \cmodel{}.
In these languages, the modeller is encouraged to create high-level concepts and declare the way in which they are rewritten into \gls{native} \constraints{}.
@ -230,7 +230,7 @@ Overall, this thesis makes the following contributions.
\item It presents a formal execution model of rewriting of the \minizinc\ language and extends this model with well-known optimization and simplification techniques.
\item It provides a novel method of tracking of \constraints{} created as part of functional dependencies, ensuring the correct removal of dependencies no longer required.
\item It provides a novel method of tracking of \constraints{} created as part of functional dependencies, ensuring the correct removal of unused dependencies.
\item It presents an analysis technique to reason about in what (\gls{reified}) form \constraints{} should be considered.
@ -272,7 +272,7 @@ We conclude this chapter by analysing the impact of \gls{half-reif} for differen
We first present a novel technique that eliminates the need for the incremental \gls{rewriting}.
Instead, it integrates a meta-optimization specification, written in the \minizinc{} language, into the \gls{slv-mod}.
Then, we describe a technique to optimize the \gls{rewriting} process for incremental changes to an \instance{}.
This method ensures that no work is done for parts of the \instance{} that remain unchanged.
This method prevents the repeated \gls{rewriting} for parts of the \instance{} that remain unchanged.
We conclude this chapter by testing the performance and computational overhead of these two techniques.
Finally, \emph{\Cref{ch:conclusions}} is the concluding chapter of the thesis.

55
chapters/2_background.tex
View File

@ -27,7 +27,7 @@ A specific problem is captured by an \instance{}, the combination of a \cmodel{}
The type of problem described by a \cmodel{} is called a \gls{dec-prb}.
The goal of a \gls{dec-prb} is to find a \gls{sol}: a complete \gls{variable-assignment} that satisfies the \constraints{}.
Or, when this is not possible, prove that no such \gls{assignment} exists.
Or, when this is not possible, prove that such an \gls{assignment} cannot exist.
Many \cmls{} also support the modelling of \glspl{opt-prb}, where a \gls{dec-prb} is augmented with an \gls{objective}.
In this case the goal is to find a \gls{sol} that satisfies all \constraints{} while minimizing (or maximizing) the value of the \gls{objective}.
@ -137,11 +137,11 @@ It is the primary way in which \minizinc{} communicates with \solvers{}.
The former constrains that the selection \variables{} multiplied by the space required for the represented element and ensures their sum is smaller than the available space.
The latter calculates the value of the \mzninline{total_joy} \variable{} by adding together selection \variables{} multiplied by the joy value of the represented element.
In these \constraints{}, the \prbpars{} are merely represented by the values given in the \gls{parameter-assignment}.
Their names are no longer present in the \gls{slv-mod}.
Their names are not present in the \gls{slv-mod}.
This \gls{slv-mod} is then passed to the targeted \solver{}.
The \solver{} attempts to determine a complete \gls{variable-assignment} and maximize the \gls{assignment} of the \mzninline{total_joy} \variable{}.
If there is no such \gls{assignment}, then it reports that the \gls{slv-mod} is \gls{unsat}.
If such an \gls{assignment} does not exist, then it reports that the \gls{slv-mod} is \gls{unsat}.
\end{example}
\begin{listing}
\mznfile{assets/listing/back_knapsack.fzn}
@ -183,7 +183,7 @@ Variable declarations are stated in the form \mzninline{@\(T\)@: @\(I\)@ = @\(E\
\item and the modeller can functionally define the value using an expression \(E\).
\end{itemize}
The syntax \mzninline{= @\(E\)@} is optional.
It is omitted when a \variable{} has no functional definition, or when a \parameter{} is a \prbpar{} and assigned externally.
It is omitted when a \variable{} has is not functionally defined, or when a \parameter{} is a \prbpar{} and assigned externally.
The identifier used in a top-level variable declaration must be unique.
Two declarations with the same identifier result in an error during the \gls{rewriting} process.
@ -471,7 +471,7 @@ Part of the semantics of a \cml{} is the choice as to how to treat these \gls{pa
Suppose the \gls{array} \texttt{a} has index set \mzninline{1..5}, but \mzninline{i} takes the value seven.
This means the expression \mzninline{a[i]} undefined.
If \minizinc{} did not implement any special handling for \gls{partial} functions, then the whole expression would have to be marked as undefined and no \gls{sol} is found.
If \minizinc{} did not implement any special handling for \gls{partial} functions, then the whole expression would have to be marked as undefined and a \gls{sol} cannot be found.
However, intuitively if \mzninline{i = 7} the \constraint{} should be trivially true.
\end{example}
@ -518,7 +518,7 @@ There is both the question of what happens when an undefined expression is evalu
\item[Relational] The \gls{rel-sem} follows from all expressions in a \cml{} eventually becoming part of a relational \constraint{}.
So even though a (functional) expression does not have a well-defined result, we can still decide whether its surrounding relation holds.
For example, the expression \mzninline{x div 0} is undefined, but the relation \mzninline{int_div(x, 0, y)} is said to be \mzninline{false}.
There are no possible values for \mzninline{x} and \mzninline{y} such that the relation holds.
Values for \mzninline{x} and \mzninline{y} such that the relation holds do not exist.
It can be said that the relational semantic makes the closest relational expression that contains an undefined expression \mzninline{false}.
\end{description}
@ -575,18 +575,18 @@ Therefore, only that one value for \mzninline{b} has to be tried.
\gls{cp} is the idea of solving \glspl{dec-prb} by performing an intelligent search by inferring which values are still feasible for each \variable{} \autocite{rossi-2006-cp}.
A \gls{cp} \solver{} performs a depth first search.
Using a mechanism called \gls{propagation} the \solver{} removes values from \domains{} that are no longer possible.
Using a mechanism called \gls{propagation} the \solver{} removes values from \domains{} that are impossible.
\Gls{propagation} works through the use of \glspl{propagator}: algorithms dedicated to a specific \constraint{} that prune \domains{} when they contain values that are proven to be inconsistent.
This mechanism can be very efficient because a \gls{propagator} only has to be run again if the \domain{} of one of its \variables{} has changed.
If a \gls{propagator} can prove that it is always \gls{satisfied}, then it is subsumed: it never has to be run again.
In the best case scenario, \gls{propagation} eliminates all impossible values and all \variables{} have been \gls{fixed} to a single value.
In the best case scenario, when \gls{propagation} eliminates values, all \variables{} are \gls{fixed} to a single value.
In this case we have arrived at a \gls{sol}.
Often, \gls{propagation} alone is not enough to find a \gls{sol}.
When we reach a \gls{fixpoint}, where no more \domain{} reductions are performed, and no \gls{sol} is found, the \solver{} then has to make a search decision.
When we reach a \gls{fixpoint}, where \gls{propagation} cannot reduce any \domains{}, and a \gls{sol} is not found, the \solver{} then has to make a search decision.
It fixes a \variable{} to a value or adds a new \constraint{}.
This search decision is an assumption made by the \solver{} in the hope of finding a \gls{sol}.
If no \gls{sol} is found using the search decision, then it needs to try making the opposite decision which requires the exclusion of the chosen value or adding the opposite \constraint{}.
If a \gls{sol} is not found using the search decision, then it needs to try making the opposite decision which requires the exclusion of the chosen value or adding the opposite \constraint{}.
Note that there is an important difference between values excluded by \gls{propagation} and making search decisions.
Values excluded by propagation are guaranteed to not occur in any \gls{sol}, whereas, values excluded by a search heuristic are merely removed locally and can still be part of a \gls{sol}.
@ -601,7 +601,7 @@ Every \domain{} change that is made during \gls{propagation}, after the first se
Whenever a new search decision is made, the current position of the list is tagged.
If the \solver{} now needs to undo a search decision (\ie\ \gls{backtrack}), it reverses all changes until it reaches the change that is tagged with the search decision.
Because all changes before the tagged point on the \gls{trail} were made before the search decision was made, it is guaranteed that these \domain{} changes do not depend on the search decision.
Furthermore, because \gls{propagation} is performed to a \gls{fixpoint}, it is guaranteed that no duplicate \gls{propagation} is required.
Furthermore, because \gls{propagation} is performed to a \gls{fixpoint}, \gls{propagation} is never duplicated.
The solving method used by \gls{cp} \solvers{} is very flexible.
A \solver{} can support many types of \variables{}: they can range from Boolean, floating point numbers, and integers, to intervals, sets, and functions.
@ -613,7 +613,7 @@ They allow modellers to always use \glspl{global} and depending on the \solver{}
\begin{example}%
\label{ex:back-nqueens}
As an example of the \gls{propagation} mechanism, let us consider the N-Queens problem.
Given a chessboard of size \(n \times n\), find a placement for \(n\) queen chess pieces such that no queen can attack another.
Given a chessboard of size \(n \times n\), find a placement for \(n\) queen chess pieces such that the queens cannot attack each other.
This means we can only place one queen per row, one queen per column, and one queen per diagonal.
The problem can be modelled in \minizinc{} as follows.
@ -630,12 +630,12 @@ They allow modellers to always use \glspl{global} and depending on the \solver{}
The \variables{} in the \gls{array} \mzninline{q} decide for each column in which row the queen is placed.
This automatically restricts every column to only have a single queen.
As such, no queen will be able to attack vertically.
The \constraints{} model the remaining rules of the problem: no two queens can be placed in the same row, no two queen can be placed in the same upward diagonal, and no two queens can be placed in the same downward diagonal.
As such, the queen will not be able to attack vertically.
The \constraints{} model the remaining rules of the problem: two queens cannot be placed in the same row, two queens cannot be placed in the same upward diagonal, and two queens cannot be placed in the same downward diagonal.
For many \gls{cp} \solvers{} this model is close to a \gls{slv-mod}, since integer \variables{} and an \mzninline{all_different} \gls{propagator} are common.
When solving the problem, initially no values can be eliminated from the \glspl{domain} of the \variables{}.
The first propagation happens when the first queen is placed on the board, the first search decision.
When solving the problem, initially we cannot eliminate any values from the \glspl{domain} of the \variables{}.
The first \gls{propagation} happens when the first queen is placed on the board, the first search decision.
\Cref{fig:back-nqueens} visualizes the \gls{propagation} after placing a queen on the d3 square of an eight by eight chessboard.
When the queen it placed on the board in \cref{sfig:back-nqueens-1}, it fixes the value of column 4 (d) to the value 3. This implicitly eliminates any possibility of placing another queen in the column.
@ -683,7 +683,7 @@ Instead, it is sometimes better to use a propagator with a lower level of consis
Although it does not eliminate all possible values of the domain, searching the values that are not eliminated may take less time than achieving domain consistency.
This is, for example, the case for integer linear \constraints{}: \[ \sum_{i} c_{i} x_{i} = d\] where \(c_{i}\) and \(d\) are integer \parameters{} and \(x_{i}\) are integer \variable{}.
For these \constraints{}, no realistic \gls{domain-con} \gls{propagator} exists because the problem is \gls{np}-hard \autocite{choi-2006-fin-cons}.
For these \constraints{}, a realistic \gls{domain-con} \gls{propagator} cannot exist because the problem is \gls{np}-hard \autocite{choi-2006-fin-cons}.
Instead, \solvers{} generally use a \gls{bounds-con} \gls{propagator}, which guarantees only that the minimum and maximum values in the \glspl{domain} of the \variables{} are used in at least one possible \gls{assignment} that satisfies the \constraint{}.
Thus far, we have only considered finding \glspl{sol} for \glspl{dec-prb}.
@ -691,10 +691,10 @@ Thus far, we have only considered finding \glspl{sol} for \glspl{dec-prb}.
The \gls{cp} \solver{} follows the same method as previously described.
However, when it finds a \gls{sol}, it does not yet know if this \gls{sol} is an \gls{opt-sol}.
It is merely an incumbent \gls{sol}.
The \solver{} must therefore resume its search, but it is no longer interested in just any \gls{sol}, only \glspl{sol} for which the \gls{objective} returns a better value.
The \solver{} must therefore resume its search, but it is not interested in just any \gls{sol}, only \glspl{sol} for which the \gls{objective} returns a better value.
This is achieved by adding a new \constraint{} that enforces a better objective value than the incumbent \gls{sol}.
If the search process finds another \gls{sol}, then the incumbent \gls{sol} is updated and the search process continues.
If the search process does not find any other \glspl{sol}, then it is proven that there are no better \glspl{sol} than the current incumbent \gls{sol}.
If the search process does not find any other \glspl{sol}, then it is proven that a better \gls{sol} than the current incumbent \gls{sol} cannot exist.
It is an \gls{opt-sol}.
\gls{cp} solvers like \gls{chuffed} \autocite{chuffed-2021-chuffed}, Choco \autocite{prudhomme-2016-choco}, \gls{gecode} \autocite{gecode-2021-gecode}, and OR-Tools \autocite{perron-2021-ortools} have long been one of the leading methods to solve \minizinc\ instances.
@ -730,7 +730,7 @@ In \gls{lp} our \variables{} must be continuous.
If we require that one or more take an integer value (\(x_{i} \in \mathbb{Z}\)), then the problem becomes \gls{np} hard.
The problem is referred to as \gls{mip} (or Integer Programming if \textbf{all} \variables{} must take an integer value).
Unlike \gls{lp}, there is no algorithm that solves a mixed integer program in polynomial time.
Unlike \gls{lp}, there is not an algorithm that solves a mixed integer program in polynomial time.
We can, however, adapt \gls{lp} solving methods to solve a mixed integer program.
We do this by treating the mixed integer program as a linear program and find an \gls{opt-sol}.
If the \variables{} happen to take integer values in the \gls{sol}, then we have found an \gls{opt-sol} to the mixed integer program.
@ -1011,10 +1011,9 @@ To support \gls{opl}'s dedicated search language, the language is tightly integr
Its search syntax requires that the \gls{opl} process directly interacts with the \solver{}'s internal search mechanism and that the \solver{} reasons about search on the same level as the \gls{opl} model.
It is therefore not always possible to connect other \solvers{} to \gls{opl}.
While this advanced search language is an interesting construct, it is no longer available in the current version of \gls{opl} \autocite{ibm-2017-opl}.
While this advanced search language is an interesting construct, it has been removed from the current version of \gls{opl} \autocite{ibm-2017-opl}.
Instead, \gls{opl} now offers the use of ``search phases'', which function similarly to \minizinc{}'s \gls{search-heuristic} \glspl{annotation}.
\subsection{Essence}%
\label{sub:back-essence}
@ -1037,7 +1036,7 @@ Partitions are defined for finite types: Booleans, enumerated types, or a restri
Let us consider modelling in \gls{essence} using the well-known ``social golfer'' problem.
In the social golfer problem, a community of golfers plans games of golf for a set number of weeks.
Every week all the golfers are split into groups of equal size and each group plays a game of golf.
The goal of the problem is to find a way to split the groups differently every week, such that no two golfers will meet each other twice.
The goal of the problem is to find a way to split the groups differently every week, such that two golfers will not meet each other twice.
Two golfers can only be part of the same group once.
A \cmodel{} for the social golfer problem in \gls{essence} can be seen in \cref{lst:back-essence-sgp}.
@ -1057,7 +1056,7 @@ Partitions are defined for finite types: Booleans, enumerated types, or a restri
Because the \variable{} reasons about partitions of the golfers, a correct \gls{assignment} is already guaranteed to correctly split the golfers into groups.
The usage of a set of size \texttt{weeks} means that we directly reason about that number of partitions that have to be unique.
The type of the \variable{} does, however, not guarantee that no two golfers will meet each other twice.
The type of the \variable{} does, however, not guarantee that two golfers will not meet each other twice.
Therefore, a \constraint{} that enforces this is found on \lref{line:back:essence:con}.
Notably, the \texttt{together} function tests whether two elements are in the same part of a partition.
@ -1143,7 +1142,7 @@ In a term rewriting rule, a term can also contain a term variable, which capture
\end{example}
Two properties of a \gls{trs} that are often studied are \gls{termination} and \gls{confluence}.
A \gls{trs} is said to be terminating if, no-matter what order the term rewriting rules are applied, you always arrive at a \gls{normal-form} (\ie{} a set of \glspl{term} for which no more rules apply).
A \gls{trs} is said to be terminating if, no-matter what order the term rewriting rules are applied, you always arrive at a \gls{normal-form} (\ie{} a set of \glspl{term} for which none of the rules apply).
A \gls{trs} is confluent if, no-matter what order the term rewriting rules are applied, you always arrive at the same \gls{normal-form} (if you arrive at a \gls{normal-form}).
It is trivial to see that our previous example is non-terminating, since you can repeat rule \(r_{3}\) an infinite amount of times.
@ -1184,7 +1183,7 @@ Similarly, there is a \mzninline{minimize} predicate that is used to find the op
The evaluation of a constraint logic program rewrites the list of \constraints{}, called the goal, in the order given by the programmer.
The \gls{rewriting} of the \constraint{} predicates is tried in the order in which the different \gls{rewriting} rules for the \constraint{} predicates are defined.
The process is completed when all \constraints{} are rewritten and no inconsistency is detected between the \gls{native} \constraints{} that are produced.
The process is completed when all \constraints{} are rewritten and the produced \gls{native} \constraints{} are not found to be inconsistent.
If all the possible ways of rewriting the program are tried, but all of them prove to be inconsistent, then the program itself is said to be \gls{unsat}.
Even when a correct rewriting is found, it is possible to continue the process.
This way you find all possible correct ways to rewrite the program.
@ -1236,7 +1235,7 @@ This means that, for some rules, multiple terms must match, to apply the rule.
\item Finally, the transitivity rule introduces a derived \constraint{}.
When it finds the \constraints{} \texttt{X -> Y} and \texttt{Y -> Z}, then it adds another \constraint{} \texttt{X -> Z}.
Different from the other rules, no \constraints{} are removed.
Different from the other rules, the matched \constraints{} are not removed.
\end{itemize}
Note that the use of multi-headed rewriting rules is essential to define these rules.
@ -1394,7 +1393,7 @@ It is a well understood technique that originates from compiler optimization \au
constraint (abs(x)*2 >= 20) \/ (abs(x)+5 >= 15);
\end{mzn}
There is however no need to create two separate \variables{} (and defining \constraints{}) to represent the absolute value of \mzninline{x}.
However, we do not need to create two separate \variables{} (and defining \constraints{}) to represent the absolute value of \mzninline{x}.
The same \variable{} can be used to represent the \mzninline{abs(x)} in both sides of the disjunction.
\end{example}

13
chapters/3_rewriting.tex
View File

@ -20,14 +20,14 @@ To create an efficient \gls{slv-mod} the \gls{rewriting} process uses many simpl
\item specialized \glspl{decomp} when variables get \gls{fixed},
\item \gls{aggregation},
\item common sub-expression elimination,
\item and removing \variables{} and \constraints{} that are no longer required.
\item and removing \variables{} and \constraints{} that are not required any longer.
\end{itemize}
We now present a new architecture for the \gls{rewriting} process that has been designed for the modern day needs of \minizinc{}.
At the core of our \gls{rewriting} process lie formalized rewriting rules.
As such, this architecture represents an abstract machine model for \minizinc{}.
These rules allow us to reason about the system and about the simplifications both to the process and the resulting \gls{slv-mod}.
The process can even be made incremental: in \cref{ch:incremental} we discuss how when making incremental changes to the \minizinc{} model, no recompilation is required for the unchanged parts.
The process can even be made incremental: in \cref{ch:incremental} we discuss how when making incremental changes to the \minizinc{} \instance{}, unchanged parts of the \instance{} do not need to be rewritten again.
\begin{figure}
\centering
@ -65,7 +65,7 @@ They are guaranteed to only constrain the \variables{} introduced in the same \g
\nanozinc{} is used to represent the current state of the \instance{}.
\nanozinc{} is similar to \flatzinc{} in that it contains only declarations of \variables{} and a flat list of \constraints{}.
However, while all function calls in \flatzinc{} need to be \gls{native}, \nanozinc{} calls can refer to any function implemented in \microzinc{}.
Furthermore, \nanozinc{} allows for \constraints{} to be ``attached'' to a \variable{}, in order to be able to track their lifetime and remove them if the corresponding \variable{} is no longer required.
Furthermore, \nanozinc{} allows for \constraints{} to be ``attached'' to a \variable{}, in order to be able to track their lifetime and remove them if the corresponding \variable{} becomes unused.
As a small syntactic difference with \flatzinc{}, \constraints{} and \variable{} declarations in \nanozinc{} can be freely interleaved.
The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}.
@ -475,7 +475,8 @@ It returns the concatenation of the resulting lists with all the additional \nan
Our prototype implementation of the \microzinc{}/\nanozinc{} framework consists of the following components.
The \gls{compiler} translates \minizinc{} into a \gls{byte-code} encoding of \microzinc{}.
The compiler currently supports a significant subset of the full \minizinc{} language, with the missing features (such floating point values and complex output statements) requiring additional engineering effort but no new technology.
The compiler currently supports a significant subset of the full \minizinc{} language.
The missing features, such floating point values and complex output statements, require additional engineering effort, but do not require new technology.
The \gls{interpreter} evaluates \microzinc{} \gls{byte-code} and \nanozinc{} programs based on the \gls{rewriting} system introduced in this section.
It can read \parameters{} from a file or via an \gls{api}.
@ -666,7 +667,7 @@ It is set when the \domain{} of a \variable{} is tightened by a \constraint{} th
When the flag is set, the \variable{} cannot be removed, even when the reference count is zero.
This \constraint{} may then become subsumed after \gls{propagation} and can then be removed.
Its meaning is now completely captured by the \domains{} of the \variables{}.
However, if any defining \constraint{} can later determine the same, or a strictly tighter, \domain{}, then it is no longer \gls{binding}.
However, if any defining \constraint{} can later determine the same, or a strictly tighter, \domain{}, then it is not \gls{binding} any longer.
It is again fully implied by its defining \constraints{}.
The flag can then be unset and the \variable{} can potentially be removed.
@ -722,7 +723,7 @@ The static approach can be further improved by inlining function calls, since th
\paragraph{Implementation} In the implementation of our \microzinc{} \interpreter{}, \gls{cse} directly interacts with the reference counting mechanism.
It is clear that when an expression is reused by returning it from the \gls{cse} table, this creates a new reference to that expression.
However, the entries in the \gls{cse} table should not keep the corresponding variables alive.
Otherwise, no \variable{} would ever become unused.
Otherwise, none of the \variables{} would ever become unused.
Therefore, we treat \gls{cse} entries as weak references.
They reference a \variable{}, but do not affect its liveness (\ie{} increase its reference count).
If an entry is found in the \gls{cse} table with a reference count of zero, it is removed from the table and its contents are not used.

30
chapters/4_half_reif.tex
View File

@ -290,7 +290,7 @@ It is, however, not as straightforward to construct its full \gls{reif}.
In addition to the \gls{half-reified} \gls{cnf}, a generic \gls{reif} would require the implication \(\neg \texttt{b} \implies \neg c\).
Based on the \gls{cnf} of \(c\), this would result in the following logical formula:
\[ \neg b \implies \neg c = \forall_{i} b \lor \neg \exists_{j} lit_{ij} \]
This formula, however, is no longer a direct set of clauses.
This formula, however, is not direct set of clauses.
Rewriting this formula into \gls{cnf} would result in:
\[ \neg b \implies \neg c = \forall_{i,j} b \lor lit_{ij} \]
It adds a new binary clause for every literal in the original \gls{cnf}.
@ -517,7 +517,7 @@ Otherwise, the \compiler{} follows the following steps to try to introduce the m
\item If \(ctx\) is \posc{} or \negc{}, then change \(ctx\) to \mixc{} and return to step 1.
\item Finally, if none of the earlier steps were successful, then the compilation fails.
Note that this can only occur when there is no definition for the \gls{reif} of a \constraint{}, \ie{} neither a \gls{native} constraint nor a \gls{decomp}.
Note that this can only occur when there is not a definition for the \gls{reif} of a \constraint{}, \ie{} neither a \gls{native} constraint nor a \gls{decomp}.
\end{enumerate}
The (Access) and (ITE) rules show the context inference for \gls{array} access and \gls{conditional} expressions respectively.
@ -610,7 +610,7 @@ This means that individual members of a tuple, like the value and the partiality
Finally, the (Decl) and (Item0) rules describe two base cases in the inference.
The declaration item of a \variable{} does not further affect the context, and does not depend on it.
It merely triggers the creation of a new \variable{}.
The (Item0) rule is triggered when there are no more inner items in the let-expression.
The (Item0) rule is triggered when the inner items in the let-expression have been depleted.
\subsection{Potentially Root}%
\label{subsec:half-?root}
@ -768,7 +768,7 @@ Finally, in \cref{subsec:half-dyn-context} we will discuss how the context in wh
\subsection{Chain compression}%
\label{subsec:half-compress}
\Gls{rewriting} with \gls{half-reif} will in many cases result in \glspl{implication-chain}: \mzninline{b1 -> b2 /\ b2 -> c}, where \texttt{b2} has no other occurrences.
\Gls{rewriting} with \gls{half-reif} will in many cases result in \glspl{implication-chain}: \mzninline{b1 -> b2 /\ b2 -> c}, where \texttt{b2} does not occur elsewhere.
In this case the conjunction can be replaced by \mzninline{b1 -> c} and \texttt{b2} can be removed from the \cmodel{}.
The case shown in the example can be generalized to
@ -776,7 +776,7 @@ The case shown in the example can be generalized to
constraint b1 -> b2 /\ forall(i in N)(b2 -> c[i])
\end{mzn}
\noindent{}which, if \texttt{b2} has no other usage in the instance, can be resolved to
\noindent{}which, if \texttt{b2} does not occur elsewhere in the \instance{}, can be resolved to
\begin{mzn}
constraint forall(i in N)(b1 -> c[i])
@ -869,7 +869,7 @@ In the \microzinc{} \interpreter{}, this problem is resolved by only keeping the
The context recorded in the \gls{cse} table and the found context are joined using the join operator, as described in \cref{fig:half-join}.
If this context is different from the recorded context, then the expression is re-evaluated in the joint context and its result kept in the \gls{cse} table.
All usages of the previously recorded \gls{cvar} are replaced by the new result.
The dependency tracking through the use of \constraints{} attached to \variables{} ensures no defining \constraints are left in the model.
The dependency tracking, through the use of \constraints{} attached to \variables{}, ensures that all defining \constraints{} are removed from the model.
This ensures that all \variables{} and \constraints{} created for the earlier version are correctly removed.
Because the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and \negc{} context.
@ -1075,7 +1075,7 @@ Grouped by \solver{} library and whether \gls{half-reif} is used, \cref{tab:half
The \gls{rewriting} statistics for the \gls{gecode} \solver{} library, shown in \cref{subtab:half-flat-gecode}, show significant changes in the resulting \flatzinc{}.
Although the total number of \constraints{} remains stable, we see that well over half of all \glspl{reif} are replaced by \glspl{half-reif}.
This replacement happens mostly 1-for-1; the difference between the number of \glspl{half-reif} introduced and the number of \glspl{reif} reduced is only 20. In comparison, the number of implications removed by \gls{chain-compression} looks small, but this number is highly dependent on the \minizinc{} model.
In many models, no implications can be removed, but for some problems an implication is removed for every \gls{half-reif} that is introduced.
In many models \gls{chain-compression} does not remove any implications, but in some models an implication is removed for every \gls{half-reif} that is introduced.
Finally, the overhead of the introduction of \gls{half-reif} and the newly introduced optimization techniques is minimal.
The \Cref{subtab:half-flat-lin} paints an equally positive picture of \glspl{half-reif} for linearization.
@ -1105,10 +1105,10 @@ It might be possible to create more dedicated \glspl{decomp} for \gls{half-reifi
\Cref{tab:half-mznc} shows the results reported by the solvers. The \solver{} reports
\begin{description}
\item[Unsatisfiable] when it proves the instance does not have a solution,
\item[Optimal solution] when it has found a solution and has proven it optimal,
\item[Satisfied] when it has found a solution for the problem,
\item[Unknown] when no solution is found, and
\item[Unsatisfiable] when it proves the \instance{} does not have a \gls{sol},
\item[Optimal solution] when it has found a \gls{sol} and has proven the \gls{sol} to be optimal,
\item[Satisfied] when it has found a \gls{sol} for the problem,
\item[Unknown] when it does not find a \gls{sol} is found within the time limit, and
\item[Error] when the \solver{} program crashes.
\end{description}
@ -1118,14 +1118,14 @@ The results shown in this table are very mixed.
For \gls{gecode}, \gls{half-reif} does not seem to impact its solving performance.
We would have hoped that \glspl{propagator} for \glspl{half-reif} would be more efficient and reduce the number of \glspl{propagator} scheduled in general.
However, neither number of \instances{} solved, nor the required solving time improved.
A single \instance{}, however, is negatively impacted by the change; an \gls{opt-sol} for this \instance{} is no longer found.
A single \instance{}, however, is negatively impacted by the change; for this \instance{} it cannot find an \gls{opt-sol} any longer.
We expect that this \instance{} has benefited from the increased Boolean \gls{propagation} that is caused by full \gls{reif}.
Overall, these results do not show any significant positive or negative effects in \gls{gecode}'s performance when using \gls{half-reif}.
When using \gls{cplex}, \gls{half-reif} clearly has a positive effect.
Although it no longer proves the unsatisfiability of one instance and slightly increases the number of solver errors, an optimal solution is found for five more instances.
Although it does not prove the unsatisfiability of one instance any longer and slightly increases the number of solver errors, an \gls{opt-sol} is found for five more instances.
The same linearized instances when using the \gls{cbc} solver seem to have the opposite effect.
Even though it reduces the time required to prove that two instances are unsatisfiable, it can no longer find six optimal solutions.
Even though it reduces the time required to prove that two instances are \gls{unsat}, it cannot find six \glspl{opt-sol} any longer.
These results are hard to explain.
In general, we would expect the reduction of \constraints{} in a \gls{mip} instance would help the \gls{mip} solver.
However, we can imagine that the removed \constraints{} in some cases help the \gls{mip} solver.
@ -1136,7 +1136,7 @@ When using \gls{half-reif} in addition to \gls{aggregation} and \gls{del-rew}, t
The solving statistics for \gls{openwbo} might be most positive.
Through the use of \gls{half-reif}, \gls{openwbo} is able to find and prove the \gls{opt-sol} for 3 more \instances{}.
It negatively impacts one \instance{}, that no longer finds any \gls{sol}.
It negatively impacts one \instance{}, for which find a \gls{sol} is not found any more.
That the effect is so positive is surprising since its \gls{rewriting} statistics for \gls{maxsat} showed the least amount of change.
% \section{Summary}

26
chapters/5_incremental.tex
View File

@ -62,7 +62,7 @@ We define a few additional \minizinc{} \glspl{annotation} and functions that
\begin{itemize}
\item allow us to express important aspects of the meta-optimization algorithm in a more convenient way, and
\item enable a simple \gls{rewriting} scheme that requires no additional communication with and only small, simple extensions of the target \solver{}.
\item enable a simple \gls{rewriting} scheme that does not require any additional communication with and only small, simple extensions of the target \solver{}.
\end{itemize}
\subsection{Restart Annotation}
@ -91,7 +91,7 @@ The proposed \glspl{annotation} are shown in \cref{lst:inc-restart-ann}.
The \mzninline{restart_on_solution} annotation tells the solver to restart immediately for each \gls{sol}, rather than looking for the best one in each restart.
The \mzninline{restart_without_objective} tells it not to add \gls{bnb} \constraints{} on the \gls{objective}.
The other \mzninline{restart_X} annotations define different strategies for restarting the search when no \gls{sol} is found.
The other \mzninline{restart_X} annotations define different strategies for restarting the search when a \gls{sol} cannot be found.
The \mzninline{timeout} annotation gives an overall time limit for the search.
Finally, the \mzninline{restart_limit} stops the search after a fixed number of \glspl{restart}.
@ -123,7 +123,7 @@ The state access functions are defined in \cref{lst:inc-state-access}.
Function \mzninline{status} returns the status of the previous restart, namely:
\begin{description}
\item[\mzninline{START}] there has been no \gls{restart} yet;
\item[\mzninline{START}] the \solver{} has not been restarted yet;
\item[\mzninline{UNSAT}] the \gls{search-space} of the last \gls{restart} was \gls{unsat};
\item[\mzninline{SAT}] the last \gls{restart} found a \gls{sol};
\item[\mzninline{OPT}] the last \gls{restart} found and proved an \gls{opt-sol} in its \gls{search-space};
@ -211,7 +211,7 @@ Note that a simple hill-climbing (for minimization) can still be defined easily
It takes advantage of the fact that the declared \gls{objective} is available through the built-in \variable{} \mzninline{_objective}.
A more interesting example is a simulated annealing strategy.
When using this strategy, the \glspl{sol} that the \solver{} finds are no longer required to steadily improve in quality.
When using this strategy, the sequence of \glspl{sol} that the \solver{} finds are not required to steadily improve in quality.
Instead, we ask the \solver{} to find a \gls{sol} that is a significant improvement over the previous \gls{sol}.
Over time, we decrease the amount by which we require the \gls{sol} needs to improve until we are just looking for any improvements.
This \gls{meta-optimization} can help improve the qualities of \gls{sol} quickly and thereby reaching the \gls{opt-sol} quicker.
@ -247,7 +247,7 @@ A predicate that implements lexicographic search is shown in \cref{lst:inc-lex-m
The lexicographic search changes the \gls{objective} at each stage in the evaluation.
Initially, the search is in stage one: it tries to find an \gls{opt-sol} for the first \gls{objective}.
Whenever we find a \gls{sol} we stay in the same stage, but constrain the \gls{search-space} to find a better \gls{sol}.
When there exists no better \gls{sol}, we move on to the next stage, trying to find the \gls{opt-sol} for the next \gls{objective} while the earlier \glspl{objective} maintain their value.
When there does not exist a better \gls{sol}, we move on to the next stage, trying to find the \gls{opt-sol} for the next \gls{objective} while the earlier \glspl{objective} maintain their value.
This process is repeated until reach the final \gls{objective}.
When we reach a stage without an associated \gls{objective}, we are guaranteed to have reached the lexicographic optimal.
Our search is thus complete.
@ -264,7 +264,7 @@ The predicate in \cref{lst:inc-pareto} shows a \gls{meta-optimization} for the P
In this implementation we keep track of the number of \glspl{sol} found so far using \mzninline{nsol}.
There is a maximum number we can handle, \mzninline{ms}.
At the start the number of solutions is zero.
If we find no \glspl{sol}, then we finish the entire search.
If we do not find any \glspl{sol}, then we finish the entire search.
Otherwise, we record that we have one more \gls{sol}.
We store the \gls{sol} values in \mzninline{s1} and \mzninline{s2} \glspl{array}.
Before each \gls{restart} we add \constraints{} removing Pareto dominated \glspl{sol}, based on each previous \gls{sol}.
@ -372,10 +372,10 @@ In addition, for the new \constraints{} the \solver{} is extended using the foll
\begin{description}
\item[\mzninline{status(s)}] Record the status of the previous \gls{restart}, and fix \mzninline{s} to the recorded status.
\item[\mzninline{sol(x, sx)} (variants)] Constrain \mzninline{sx} to be equal to the value of \mzninline{x} in the incumbent solution.
If there is no incumbent solution, it has no effect.
\item[\mzninline{sol(x, sx)} (variants)] Constrain \mzninline{sx} to be equal to the value of \mzninline{x} in the incumbent \gls{sol}.
If a \gls{sol} has not yet been found, then it does not constrain \mzninline{sx}.
\item[\mzninline{last_val(x, lx)} (variants)] Constrain \mzninline{lx} to take the last value assigned to \mzninline{x} during search.
If no value was ever assigned, it has no effect.
If \mzninline{x} was never assigned, then it does not constraint \mzninline{lx}.
Note that many solvers (in particular \gls{sat} and \gls{lcg} solvers) already track \mzninline{last_val} for their \variables{} for use in search.
To support \gls{rbmo} a \solver{} must at least track the last value of each of the \variables{} involved in such a \constraint{}.
This is straightforward by using a \mzninline{last_val} \gls{propagator}.
@ -432,8 +432,8 @@ Now \mzninline{s} is not one, and \mzninline{b1} is set to \mzninline{true}.
The \mzninline{float_random} \gls{propagator} assigns \mzninline{rnd1} a new random value and, depending on whether it is greater than \mzninline{0.2}, the Boolean \variables{} \mzninline{b2}, and consequently \mzninline{b3} is assigned.
If it is \mzninline{true}, the \constraint{} in \lref{line:6:x1:end} becomes active and assigns \mzninline{x[1]} to its value in the previous \gls{sol}.
Furthermore, it is not strictly necessary to guard \mzninline{int_uniform} against being invoked before the first solution is found.
The \mzninline{sol} \constraints{} will simply not propagate anything in case no \gls{sol} has been recorded yet, but we use this simple example to illustrate how these Boolean conditions are rewritten and evaluated.
Furthermore, it is not strictly necessary to guard \mzninline{int_uniform} against being invoked before the first \gls{sol} is found.
The \mzninline{sol} \constraints{} will simply not propagate anything until the first \gls{sol} is recorded, but we use this simple example to illustrate how these Boolean conditions are rewritten and evaluated.
\section{An Incremental Constraint Modelling Interface}%
\label{sec:inc-incremental-compilation}
@ -482,7 +482,7 @@ These changes can be caused by the \gls{rewriting} of a \constraint{}, \gls{prop
When a \constraint{} is removed, its corresponding changes are undone by reversing all actions recorded on the \gls{trail} up to the point where the \constraint{} was added.
In order to limit the amount of \gls{trail}ing required, the programmer must create explicit ``choice points'' to which the system state can be reset.
In particular, this means that if no choice point was created before the initial \instance{} was rewritten, then this \gls{rewriting} can be performed without any \gls{trail}ing.
In particular, this means that until the first choice point is created \gls{rewriting} can be performed without any \gls{trail}ing.
\begin{example}\label{ex:inc-trail}
@ -730,7 +730,7 @@ Although some additional time is spent \gls{rewriting} the \gls{rbmo} models com
The \gls{rewriting} of the \gls{rbmo} \instances{} would likely take less time when using the new prototype architecture.
Between all the methods, solving time is very similar.
\gls{rbmo} seems to have a slight advantage.
No benefit can be noticed from the use of the incremental solver \gls{api}.
We do not notice any benefit from the use of the incremental solver \gls{api}.
\subsubsection{GBAC}

7
chapters/6_conclusions.tex
View File

@ -25,7 +25,7 @@ The \gls{rewriting} process of a \minizinc{} \instance{} into a \gls{slv-mod} th
The latter operates on (partial) \glspl{slv-mod}, expressed using the \nanozinc{} language.
Distinctively, \nanozinc{} has the ability to attach \constraints{} to a \variable{}.
During \gls{rewriting} \constraints{} introduced to define a \variable{} are attached to it.
This ensures that if it is discovered that a \variable{} is no longer required (\ie{} it is no longer referred to by any \constraints{}), it can correctly be removed.
This ensures that if it is discovered that a \variable{} becomes unused (\ie{} it is not referred to by \constraints{} any longer), it can correctly be removed.
Crucially, the architecture is easily extended with well-known simplification techniques to improve the quality of the produced \solver{} specifications.
@ -75,7 +75,8 @@ Crucially, our analysis considers the possibility of identifiers being used in m
Depending on the context of a \constraint{}, we can decide if a \gls{reif} can be avoided, if a \gls{half-reif} can be used, or if we have to use a full \gls{reif}.
We noted that \gls{half-reif} interacts with some existing simplification techniques in the architecture and propose alterations to accommodate them.
Foremost, \gls{cse} can no longer always reuse the same results for identical \constraints{}, it must now consider the context of the \constraint{}.
Foremost, \gls{cse} cannot always reuse the same results for identical \constraints{} any more.
It must now also consider the context of the \constraint{}.
For \constraints{} were \gls{cse} is triggered in multiple contexts, we propose rules to either use the result that is acceptable in both contexts, or create such a result.
Using this adjustment we ensure that identical \constraints{} are not duplicated and re-use the same \gls{cvar}, even when they occurred in different contexts.
The usage of \gls{propagation} can change the context of a \constraint{} during the \gls{rewriting} process.
@ -99,7 +100,7 @@ It is thus important that we achieve a better understanding of when the latter o
As also discussed by \textcite{feydy-2011-half-reif}, we see that \gls{cp} solvers are sometimes negatively impacted because \glspl{half-reif} do not fix their \gls{cvar}, requiring more search.
As a solution to this problem we could consider a form in between \gls{half-reif} and full \gls{reif}.
In this form the propagator would set the \gls{cvar} to \mzninline{true} if the \constraint{} holds, but does not propagate the negation of the \constraint{} when it is set to \mzninline{false}.
The downside of this form is that it is no longer equivalent to a logical implication, which means that measures such as \gls{chain-compression} would no longer be applicable.
The downside of this form is that it is not equivalent to a logical implication, which means that measures such as \gls{chain-compression} would not be applicable.
However, \glspl{propagator} for this form are still easy to design/implement, and they ensure that the \gls{cvar} is fixed through \gls{propagation}.
Finally, automated \gls{half-reif} in \minizinc{} will allow new solving performance improvements by allowing \solver{} implementers to experiment with \glspl{decomp} or \glspl{propagator} for \gls{half-reified} \constraints{}.