Clean up implementation of printing options table
[maxima.git] / share / algebra / solver / EnglishSource / SOLVRDOC.TEX
blobafcac800ce0b974eacb4f5039e93317efd31af58
1 \section{The Structure of the Solver}
3 The requirements, in particular the points  \ref{AnfImmed}, \ref{AnfLinear} and
4 \ref{AnfNonlinear}, set up in  chapter \ref{SolverAnforderungen} and schematically represented the structuring of the equations solvers  in figure \ref{Grobstruktur} suggests to lay down this into five largely independent main modules, see \cite{Trispel}. Built up on this structure and the heuristic algorithms described in the preceding chapter,  the Macsyma program packet \verb+SOLVER+ was developed for the functionality extension of the Macsyma functions \verb+SOLVE+ and \verb+LINSOLVE+.
6 The tasks of the module {\em Solver Preprocessor} are general, checking the command syntax and semantics, the construction of internal data structures, and the execution of an introductory consistency check. The check determines whether the set of equations directly contains contradictory  statements like  number = number or constraint conditions between parameters .
8 The {\em Immediate Assignment Solver}  searches the system of equations for direct assignments of the form $\mbox{\em var} = \const$ or $\const = \mbox{\em var}$ before the call of the {\em Linear Solvers}  and executes these immediately, so that the cost of computation  for the following program module is kept as small as possible.
10 The  {\em Linear Solver} is a pre and post processor for the Maxima function \verb+LINSOLVE+  for the simultaneous solution of linear systems of equations. The module extracts  pieces  of linear equations according to the heuristic algorithm described in paragraph \ref{HeurAlgoLin}  and solves the equations by calling \verb+LINSOLVE+. The resulting solutions are inserted into the remaining equations before leaving the {\em Linear Solvers}.
12 The {\em Valuation Solver} is the core module of the  {\em Solvers}. Its tasks are the use of valuation strategies for the generation of the solution sequences and the solution of the nonlinear equations with the help of the Maxima build-in function \verb+SOLVE+. In the case of multiple solutions the {\em Valuation Solver}  checks each individual solution for consistency with the remaining system of equations. Inconsistent solutions are rejected, while valid solutions are inserted into the remaining system  of equations and the corresponding solution paths are tracked separately through recursive  calls of the {\em Valuation Solvers}.
14 All steps necessary for the editing of the solutions for output to the user are taken over  by the {\em Solver Postprocessor}. These are the expansion of the hierarchically organized solution list supplied by the {\em Valuation  Solver}, the back substitution of the
15 symbolic solutions as well as picking out, evaluating and outputting the variables and composite terms asked for by the user.
17 \begin {figure} [htbp]
18 \begin {center}
19 \includegraphics[height=10cm]{StrukturEn.png}
20 \caption \protect {\begin {minipage} [h] {10cm}% --- TABLE
21 Structure of the Solvers
22 \label{Grobstruktur}
23 \end {minipage}
25 \end {center}
26 \end {figure}
28 %\inbildpsf{Struktur des Solvers}{struktur.eps}{100mm}{Grobstruktur}
29 \clearpage
31 \section{The Modules of Solvers}
33 \subsection{The Solver Preprocessor}
35 \begin {figure} [htbp]
36 \begin {center}
37 \includegraphics[height=8cm]{PreprocEn.png}
38 \caption \protect {\begin {minipage} [h] {10cm}% --- TABLE
39 Flow diagram of the  Solver Preprocessor\label{AblPreproc}
40 \end {minipage}
42 \end {center}
43 \end {figure}
45 %\inbildpsf{Ablaufdiagramm des Solver Preprocessors}{preproc.eps}{60mm}%
46 %{AblPreproc}
48 Beside the examination of the command syntax and semantic as well as the construction of the internal equations, variables and parameter lists,  the {\em Solver Preprocessor} executes a consistency check of the equations, whose flow diagram is represented in figure \ref{AblConsChk}. Aim of the consistency check is it to detect from the beginning, whether the system of equations is unsolvable due to direct contradictions. Such contradictions can occur in form of pure number equations, e.g. \ $0=1$, or in addition, in the form of constrained  conditions between symbols declared as parameters.
50 In order to uncover direct contradictions, the routine for the consistency check searches after equations in the system of equations, which consist exclusively of numbers  or numbers with parameters, but does not contain variables.  If a contradictory number equation is found, then the  {\em Solver Preprocessor}  aborts immediately. If such an equation is  consistently, as for example $0=0$, it is removed from the system of equations, since it does not influence the solubility and solution of the system  and therefore is redundant.
52 The handling of parameters with constrain conditions is somewhat more complex. Assumed, the symbols $A$ and $B$ were defined as parameters of a system of equations, which contains the equation 
53 \begin{equation} \label{ParamConstraint}
54 A + B = 1
55 \end{equation}
57 \begin {figure} [htbp]
58 \begin {center}
59 \includegraphics[height=8cm]{ConschkEn.png}
60 \caption \protect {\begin {minipage} [h] {10cm}% --- TABLE
61 Flow diagram of the routine for the consistency check\label{AblConsChk}
62 \end {minipage}
64 \end {center}
65 \end {figure}
67 %\inbildpsf{Ablaufdiagramm der Routine zur Konsistenzpr"ufung}{conschk.eps}%
68 %{125mm}{AblConsChk}
70 From this condition follows, that $A$ and $B$ are not {\em independent} parameters and therefore the system of equations is not solvable for any combinations of their values. Since conditioned inconsistencies of this type cannot be excluded with many technical problem settings, it is not meaningful to abort the solution process in such cases unless the parameterized equation contradicts  other constraints  in the system of equations. The decision, whether a parameter constraint is to be regarded as admissible, is delegated therefore by the consistency check to the user. In the case of the equation (\ref{ParamConstraint}) the system asks in the following way for the validity of the condition:
71 \begin{literatim}{|}
72 Is   B + A - 1   positive, negative, or zero?
73 \end{literatim}
75 Becomes the question answered with \verb+p;+ or \verb+n;+ ({\em positive} resp.\ {\em
76 negative}), then the Solver aborts. If the response reads \verb+z;+ ({\em zero}), then the consistency check stores the constained condition in a global list named \verb+SolverAssumptions+, which can be inspected after the Solver run. Subsequently, the consistency check removes the redundant equation from the system.
78 % ch 2.2
79 \subsection{The Immediate Assignment Solver}
81 \begin {figure} [htbp]
82 \begin {center}
83 \includegraphics[height=8cm]{ImmedEn.png}
84 \caption \protect {\begin {minipage} [h] {10cm}% --- TABLE
85 Flow diagram of the Immediate Assignment Solver\label{AblImmed}
86 \end {minipage}
88 \end {center}
89 \end {figure}
91 %\inbildpsf{Ablaufdiagramm des Immediate Assignment Solvers}{immed.eps}%
92 %{125mm}{AblImmed}
94 The task of the {\em Immediate Assignment Solvers} is to search the system of equations for direct assignments of the form $\mbox{\em var} = \const$  and to use such equations directly for the elimination of the corresponding variables. With systems of equations, set up  mechanically, as for instance in the example \ref{ET}, the cost of computation  in  {\em Linear Solver}  for the extraction and solution of the linear equations can be often reduced considerably by such a preprocessing of the equations.
96 At first, the {\em Immediate Assignment Solvers }  filters out all direct assignments  $\mbox{\em var} = \const$ and $\const = \mbox{\em var}$ from the system  in a loop and stores them in the form $\mbox{\em var} = \const$ in the solution list, if a solution for {\em var}  is not yet entered. Subsequently, the system of equations is analyzed by means of the solution list  and checked again for consistency.
98 \clearpage
100 \subsection{The Linear Solver}% 2.2.3
102 The process of the {\em Linear Solvers} starts, as described in paragraph \ref{HeurAlgoLin}, with the construction of the complete coefficient matrix of the symbolic system of equations. Using this coefficient matrix, the valuation matrix is created, which serves for the extraction of  parts of linear equations. As long as the valuation matrix contains still '1' elements, i.e. $\sum C \neq 0$ und $\sum R \neq 0$, the described heuristic evaluation strategy  is applied, which decides, which nonlinear equation is removed or which in a nonlinear sense occurring variable is transferred to right hand side of the equation.
104 If the valuation matrix was reduced to a zero-matrix, then a list of the remaining (linear) equations and a list of the linear variables are created, which can be transferred as function parameters to the Maxima instruction \verb+LINSOLVE+, which  serves for the solution of a linear system of equations. 
105 For efficiency,  before the call of \verb+LINSOLVE+ however, still another special feature is considered, which was not mentioned during the description of the extraction algorithm. Occasionally it can occur, that simultaneously with the deleting of a nonlinear equation the only instance of a linear variable $x_j$ is removed  from the entire valuation matrix, without that it was noticed directly. 
106 Likewise equations can develop, which are no longer nonlinear w.r.t as linear detected variables, but do not contain these variables any more, i.e. the associated coefficients are directly zero. 
107 Therefore,  all linear variables of the linear subsystem are  again checked, whether they are still contained in the linear equations, an
108 The {\em Linear Solver}
109 would also be able to solve the system of equations without these additional measures, but frequently unnecessary cost of computation can be saved by it.
111 In section \ref{LoesungLin}, it was demonstrated, that while solving of over-determined linear systems of equations, inconsistencies can occur, which does not necessarily imply the insolubility of the system of equations. If such contradictory equations are detected, e.g. the right side of equation  (\ref{constraint})\footnote{That access to the contradictory equations from the outside is not possible using the standard  {\tt LINSOLVE} command.  Therefore a particularly modified version of the instruction  on Lisp level was necessary, which was made available by Jeffrey P.\ Golden, Macsyma, Inc. (the USA), on a kindly request.}, 
112 they are submitted a consistency checking, as at the beginning the entire system of equations. If the contradictory equations prove as true inconsistencies, then the total system does not have a solution, and the {\em Linear Solver} aborts with an appropriate error message. If the contradictory equations contain still looked-for variables, then they are removed from the system of equations and added as new constrained  conditions to the remaining system. Thereupon \verb+LINSOLVE+ is again called  with the linear independent part of the equations (inconsistencies can not occur any longer with the second run).
114 If the linear equations were successfully solved, then the solutions are inserted into the remaining system of equations and the list of the looked-for variables is updated. That is, all variables, for which a solution was found  by the {\em Linear Solver}, are removed from the list, while new variables, which are contained in these solutions, are added to the list.
116 \clearpage
118 \begin {figure} [htbp]
119 \begin {center}
120 \includegraphics[height=8cm]{LinearEn.png}
121 \caption \protect {\begin {minipage} [h] {10cm}% --- TABLE
122 Flow diagram of the Linear Solver\label{AblLinear}
123 \end {minipage}
125 \end {center}
126 \end {figure}
127 %\inbildpsf{Ablaufdiagramm des Linear Solvers}{linear.eps}{160mm}%
128 %{AblLinear}
130 \clearpage
132 \subsection{The Valuation Solver} %%% 2.2.4  =================
134 The {\em Valuation Solver} first checks,  whether equations and variables still  are available, which can be solved. 
135 If this is the case, then for the remaining equations two valuation matrices are set up, which serve as basis for the solution sequence order. Both matrices have the dimensions $n \times m$, whereby $n$ is the number of the equations and $m$ the number of variables,  looked for at the moment. The first matrix, the  {\em  path matrix of variables}, contains for each equation the number of  paths for this variable (see section \ref{KomplBewertung})) w.r.t each variable. The second matrix is the  {\em valuation matrix}. Their entries are calculated by the heuristic operator tree valuations of each equation w.r.t. each variable.
138 To these two matrices one applies  afterwards  -- depending on whether an internal or user-defined  is desired -- an valuation strategy, which arranges the pairs of equation/variables in such a way, that the first items  in this list are the most promising candidates for a following solution attempt  by means of the \verb+SOLVE+ command.
140 As long as not all proposals for solutions in the list were tried  and no correct solution for one of the suggestions was  calculated, on the basis the determined solution order the next equation from the equation list is selected and tried to solve. If this does not succeed, one or more user-defined transformation functions (if available) for the transformation of the equation are applied and  in each case a solution attemptsare  made.  If these are also without result, the next proposal for a solution is tried.
142 If  none of the equations is solvable after any variable any more, then the {\em Valuation Solver} returns the unresolved equations in implicit form additionally to all solutions found up to this point, so that these  may be treated later with a numeric procedure. With a successful solution attempt all single solutions (nonlinear equations may have multiple solutions) are checked separately for consistency with the remaining equations. Those solutions, which lead to contradictory predicates, are rejected and with them the corresponding solution path.
144 If after the consistency check no solution  remains, then the system of equations is inconsistent, and the  {\em Valuation Solver} aborts.  If exactly one solution remains, then this solution is appended to the solution list and substituted into the remaining equations. Finally the list of the wanted variables is updated, whilst the variable just calculated is removed from it and new variables, possibly contained in the solution,  are added. These  can be variables, which are not given as parameters and also not indicated as looked-for. The main solution loop of the {\em Valuation Solvers} begins then again from the start.
146 With consistent multiple solutions all solution paths must be pursued separately. Fot that the {\em Valuation Solver} calls itself recursively with the remaining equations and variables for each individual solution  and stores the outputted results in a hierarchically structured solution list. Their expansion is task of the {\em Solver Postprocessors} described in the next section.
149 \clearpage
151 \begin {figure} [htbp]
152 \begin {center}
153 \includegraphics[height=8cm]{Valsolv1En.png}
154 \caption \protect {\begin {minipage} [h] {10cm}% --- TABLE
155 Flow diagram of the Valuation Solver (part 1)\label{AblValSolv1}
156 \end {minipage}
158 \end {center}
159 \end {figure}
161 %\inbildpsf{Ablaufdiagramm des Valuation Solvers (Teil 1)}{valsolv1.eps}%
162 %{157mm}{AblValSolv1}
164 \clearpage
166 \begin {figure} [htbp]
167 \begin {center}
168 \includegraphics[height=8cm]{Valsolv2aEn.png}
169 \includegraphics[height=8cm]{Valsolv2bEn.png}
170 \caption \protect {\begin {minipage} [h] {10cm}% --- TABLE
171 Flow diagram of the Valuation Solver (part 2)\label{AblValSolv2}
172 \end {minipage}
174 \end {center}
175 \end {figure}
177 %\inbildpsf{Ablaufdiagramm des Valuation Solvers (Teil 2)}{valsolv2.eps}%
178 %{79mm}{AblValSolv2}
180 \clearpage
183 %%% 2.2.4 ====================
184 \subsection{The Solver Postprocessor}
186 \begin {figure} [htbp]
187 \begin {center}
188 \includegraphics[height=8cm]{PostProcEn.png}
189 \caption \protect {\begin {minipage} [h] {10cm}% --- TABLE
190 Flow diagram of the Solver Postprocessor\label{AblPostproc}
191 \end {minipage}
193 \end {center}
194 \end {figure}
196 %\inbildpsf{Ablaufdiagramm des Solver Postprocessors}{postproc.eps}%
197 %{106mm}{AblPostproc}
199 The Valuation Solver supplies in the case of multiple solutions of nonlinear equations a hierarchically structured list of results (because of the recursive pursuit of the solution paths) as function value, therefore  the {\em Solver Postprocessor} must dissolve  the list hierarchy at the beginning, so that the back substitution can be executed.
201 If not all equations within a solution path could be solved  symbolically, then the result list contains the list of the remaining, unresolved nonlinear equations additionally to the variables, for which a solution was found. These will provisionally removed from the equation list and buffered, in order to be added later to the final result.
203 Depending upon the desire of the user, the back substitution of the system of equations takes place afterwards, which is present up to this point still in upper triangle form. For that, the solution list is evaluated iterative with itself, until no modification of the results is to be seen any  more. Even, if the back substitution is not required by the user\footnote{This requires to set the option variable {\tt SolverBacksubst} to {\tt FALSE} (see section \ref{Optionen})}, it  is nevertheless executed, but only so far as necessary, in order to eliminate all not specified command line variables  from the solutions. If e.g. a system of equations
204 in the variables $x$, $y$, $z$ and $w$ is to be solved only after the variables $x$ and $y$  and the solution process gives  the triangle form
205 \begin{eqnarray}
206 x &=& f_1(y,z,w)\\
207 y &=& f_2(z,w)  \\
208 w &=& f_3(z)    \\
209 z &=& \const,
210 \end{eqnarray}
211 so the complete back substitution leads to the result
212 \begin{eqnarray}
213 x &=& \const \\
214 y &=& \const
215 \end{eqnarray}
216 With switched off complete back substitution, the following two equations are given back 
217 \begin{eqnarray}
218 x &=& g(y) \\
219 y &=& \const
220 \end{eqnarray}
221 which does not contain the internal variables $z$ und $w$ any longer, but are further coupled by the variable $y$ among themselves.
223 After termination of the back substitution and the evaluation of the composite terms in the variable list of the command line using the solutions, the at first filtered unresolved equations are again appended to the solution list. The finished solution list is then given to the user as function value.
226 \section{Application of {\tt Solver}}  % ch. 2.3
228 \subsection{Command syntax}
230 The call of  {\tt Solver} from the Maxima command line use the syntax
232 \begin{literatim}{|}
233     Solver( list_of_equations, list_of_variables, list_of_parameters )
234 \end{literatim}
235 or, if the system of equations, which is to be solved, does not contain any parameters, also with
236 \begin{literatim}{|}
237     Solver( list_of_equations, list_of_variables )
238 \end{literatim}
239 The list of   equations is a list of Maxima objects, for which \verb+EquationP+ equals \verb+TRUE+. The system of equations
240 (\ref{linearxyz}) -- (\ref{linearxy}) is thus formulated in the following way:
241 \begin{literatim}{|}
242 (COM5) Equations :
244     x + 2*y -     z =  6,
245   2*x + y*z -   z^2 = -1,
246   3*x -   y + 2*z^2 =  3
248 \end{literatim}
249 The unknown variables are told to the Solver likewise in form of a list, e.g. as
250 \begin{literatim}{|}
251      [x, y, z]
252 \end{literatim}
253 for the above-mentioned systen of equations. Beside purely atomic variable symbols  (\verb+SymbolP+) the variable list may contain  also composite terms in the looked-for unknowns. If for the system of equations  the variables $x$, $y$ 
254 and $z$ are not explicitly searched, but rather $x$ and the value  $\sin(\pi yz)$, then the variable list reads
255 \begin{literatim}{|}
256      [x, sin(%pi*y*z)] .
257 \end{literatim}
259 The parameter list must contain exclusively atomic symbols, thus only objects with  \verb+SymbolP+ equals \verb+TRUE+. 
260 Composite terms are here neither admissible nor meaningfully.
262 \subsection{Special Features of the Syntax of Equations}
264 At this point we refer to some differences of the command syntax in  comparison with the admissible invocations of the Maxima build-in \verb+SOLVE+ function. The latter may also get the equations in {\em Expression} form, i.e. as expressions  $\verb#EquationP# = \verb#FALSE#$, which are implicitly understood  as equations of the form $\mbox{\em Expression} = 0$:
265 \begin{literatim}{|}
266      [
267          x + 2*y -     z - 6,  \$\leftarrow\$ {\rm{}not  admissable}
268        2*x + y*z -   z^2 + 1,
269        3*x -   y + 2*z^2 - 3
270      ]$
271 \end{literatim}
272 This form of representation of the equation  is used internally, e.g. by the {\em 
273 Valuation Solver}, but is not permitted as call of the Solver in the command line. Furthermore, the \verb+SOLVE+ function permits  omitting the brackets around the arguments, if only one equation and/or only one variable is to be transferred. This is  also not admissible with the use of Solver.
275 \subsection{Example Calls of Solver}
277 \begin{example}{SolverExample1}
278 For the input of the system of equations \verb+COM5+  a correct call of the Solver is the instruction in the command line \verb+COM7+. 
279 The specification of the calculated solutions is done in form of a list of solution lists, see output line \verb+D7+.
280 \begin{literatim}{|}
281 (COM6) MsgLevel : 'DETAIL$   {\rm/* see section \ref{Optionen} */}
283 (COM7) Solver( Equations, [x, y, z] );
285 {\rm{}Output of}{\em Solver Preprocessors}{\rm:}
286 The variables to be solved for are [X, Y, Z]
287 Checking for inconsistencies...
288 ... none found.
290 {\rm{}Output of}{\em Immediate Assignment Solvers}{\rm:}
291 Searching for immediate assignments.
292 No immediate assignments found.
294 {\rm{}Output of}{\em Linear Solvers}{\rm:}
295 Searching for linear equations...
296   ...with respect to: [X, Y, Z]
297 Found 2 linear equations in 2 variables.
298 The variables to be solved for are [X, Y]
299                                          2
300 The equations are [- Z + 2 Y + X - 6, 2 Z  - Y + 3 X - 3]
301 Solving linear equations.
302                             2                  2
303                          4 Z  - Z - 12      2 Z  + 3 Z + 15
304 The solutions are [X = - -------------, Y = ---------------]
305                                7                   7
306 Searching for linear equations...
307   ...with respect to: [Z]
308 No linear equations found.
310 {\rm{}Output of}{\em Valuation Solvers}{\rm:}
311 Checking for remaining equations.
312 1 equation(s) and 1 variable(s) left.
313 The variables to be solved for are [Z]
314 Trying to solve equation 1 for Z
316 {\rm{}Here  a complexity valuation Is not needed,}
317 {\rm{}because there is only one equation and one variable left.}
318 Valuation: (irrelevant)
319                    3       2
320 The equation is 2 Z  - 12 Z  + 17 Z + 31 = 0
321 Checking if equation was solved correctly.
322                          SQRT(13) %I - 7      SQRT(13) %I + 7
323 The solutions are [Z = - ---------------, Z = ---------------, Z = - 1]
324                                 2                    2
325 Solution is correct.
327 {\rm{}Individual consistency check w.r.t. multiple solutions:}
328 The solution is not unique. Tracing paths separately.
329 Solution 1 for Z
330 Checking for inconsistencies...
331 ... none found.
332 Solution 2 for Z
333 Checking for inconsistencies...
334 ... none found.
335 Solution 3 for Z
336 Checking for inconsistencies...
337 ... none found.
338                                     SQRT(13) %I - 7      SQRT(13) %I + 7
339 Consistent solutions for Z : [Z = - ---------------, Z = ---------------,
340                                            2                    2
342                                                                    Z = - 1]
344 {\rm{}Recursive pursuit of all three solution paths:}
345 Checking for remaining equations.
346 All variables solved for. No equations left.
347 Checking for remaining equations.
348 All variables solved for. No equations left.
349 Checking for remaining equations.
350 All variables solved for. No equations left.
352 {\rm{}Output of}{\em Solver Postprocessors}{\rm:}
353 Postprocessing results.
355             27 SQRT(13) %I - 41        17 SQRT(13) %I - 87
356 (D7) [[X = -------------------, Y = - -------------------,
357                     14                         14
359       SQRT(13) %I - 7          27 SQRT(13) %I + 41      17 SQRT(13) %I + 87
360 Z = - ---------------], [X = - -------------------, Y = -------------------,
361              2                         14                       14
363     SQRT(13) %I + 7
364 Z = ---------------], [X = 1, Y = 2, Z = - 1]]
365            2
366 \end{literatim}
367 For an better overview, here is the result again in TEX-output:
368 \begin{equation}
369 \left[
370    x = {{27\,\sqrt{13}\,i-41}\over{14}},  \,\,
371    y = -{{17\,\sqrt{13}\,i-87}\over{14}}, \,\,
372    z = -{{\sqrt{13}\,i-7}\over{2}}
373 \right]
374 \end{equation}
375 \begin{equation}
376 \left[
377    x = -{{27\,\sqrt{13}\,i+41}\over{14}}, \,\,
378    y = {{17\,\sqrt{13}\,i+87}\over{14}}, \,\,
379    z = {{\sqrt{13}\,i+7}\over{2}}
380 \right]
381 \end{equation}
382 \begin{equation}
383 \left[
384    x =  1, \,\,
385    y =  2, \,\,
386    z = -1 
387 \right]
388 \end{equation}
389 \end{example}
391 \begin{example}{SolverExample2}
392 As  second example, the following system of equations parameterized in $a$ and $b$
393 \begin{eqnarray}
394 3ax + y^2 &=& 1 \\
395  bx - y   &=& -1
396 \end{eqnarray}
397 is to be solved for the variables $x$ and $y$ as well as the composite term $x/y$ . Since the system of equations does not contain any direct assignments and in this case a repeated search for linear equations  is not meaningful, the {\em Immediate Assignment Solver} and the repetition loop of the {\em Linear Solvers}  are switched off with the instruction \verb+COM8+:
398 \begin{literatim}{|}
399 (COM8) SolverImmedAssign : SolverRepeatLinear : FALSE$
401 (COM9) ParEq : [ 3*a*x + y^2 =  1, b*x - y = -1 ]$
403 (COM10) Solver( ParEq, [x, y, x/y], [a, b] );
405                                        X
406 The variables to be solved for are [X, -, Y]
407                                        Y
408 The parameters are [A, B]
409 Checking for inconsistencies...
410 ... none found.
411 Trying to solve for [X, Y]
412                                      X
413 in order to solve for the expression -
414                                      Y
415 Searching for linear equations...
416   ...with respect to: [X, Y]
417 Found 1 linear equations in 2 variables.
418 The variables to be solved for are [X, Y]
419 The equations are [- Y + B X + 1]
420 Solving linear equations.
421 The solutions are [Y = B X + 1]
423 Checking for remaining equations.
424 1 equation(s) and 1 variable(s) left.
425 The variables to be solved for are [X]
426 Trying to solve equation 1 for X
427 Valuation: (irrelevant)
428                  2  2
429 The equation is B  X  + (2 B + 3 A) X = 0
430 Checking if equation was solved correctly.
431                          2 B + 3 A
432 The solutions are [X = - ---------, X = 0]
433                              2
434                             B
435 Solution is correct.
436 The solution is not unique. Tracing paths separately.
437 Solution 1 for X
438 Checking for inconsistencies...
439 ... none found.
440 Solution 2 for X
441 Checking for inconsistencies...
442 ... none found.
443                                     2 B + 3 A
444 Consistent solutions for X : [X = - ---------, X = 0]
445                                         2
446                                        B
447 Checking for remaining equations.
448 All variables solved for. No equations left.
449 Checking for remaining equations.
450 All variables solved for. No equations left.
451 Postprocessing results.
453               2 B + 3 A        B + 3 A  X   2 B + 3 A                   X
454 (D10) [[X = - ---------, Y = - -------, - = ----------], [X = 0, Y = 1, - = 0]]
455                   2               B     Y    2                          Y
456                  B                          B  + 3 A B
457 \end{literatim}
458 \end{example}
464 \section{\label{Optionen}The Options of {\tt Solver}}  % 2.4 ====================================
466 Using  the Maxima command line (\verb+Macsyma toplevel+) or a program file, the behavior of the Solver can be influenced by the individual setting of a set of option variables, which are listed and described in the following. Behind the names of the option variables, the standard assignments (values/symbols) are given  in angle parentheses, which are set automatically on the first start of the module \verb+SOLVER+.
468 \begin{description}
470 \item[{\tt MsgLevel <SHORT>}] ({\em message level}) 
471 controls the scope of the displayed messages during the program run. The assignments \verb+OFF+, \verb+SHORT+ and
472 \verb+DETAIL+ are admissible. 
474 Becomes  \verb+MsgLevel : OFF+, then all program outputs are completely suppressed. In the case of  \verb+SHORT+ only status informations are returned whilst the program is running. The keyword \verb+DETAIL+  causes additionally the output of all of the Solver modules intermediate results and also of messages of the decisions made due to the heuristics.
477 \item[{\tt SolverImmedAssign <TRUE>}] 
478 switches the {\em Immediate 
479 Assignment Solver} on (\verb+TRUE+) resp.\ off (\verb+FALSE+). If the module is switched on, then before the call of {\em Linear Solvers} the system of equations is searched for direct allocations of the form $\mbox{\em 
480 var} = \const$ or $\const = \mbox{\em var}$, which can be inserted immediately into the remaining equations.
483 \item[{\tt SolverRepeatImmed <TRUE>}] 
484 determines whether the {\em Immediate 
485 Assignment Solver}  is called repeatedly (\verb+TRUE+), until no more direct assignments are found, or whether only one call takes place  (\verb+FALSE+).
487 \item[{\tt SolverSubstPowers <FALSE>}] ({\em substitute powers})
488 controls the handling of variables, which occur in powers $p_k$
489 of integer multiples $p_k=k p_0$, $k \in \nz$, of a basic power $p_0
490 \in \nz \setminus \{ 1 \}$.
491 If the system of equations contains e.g. the variable  $x$ exclusively in the powers $x^2$, $x^4$,
492 $x^6$, \ldots, e.g. $p_0=2$, then  by \verb+SolverSubstPowers:TRUE+ the term $x^{p_0}=x^2$ is substituted with the
493 new variable symbol $X2$, that therfore only occurs in the powers $X2$, $X2^2$, $X2^3$, \ldots. 
494 In this way the degree of the equations which are to be solved is reduced as well as the solution variety. 
495 However, if necessary, a rework of the solutions are necessary.
498 \item[{\tt SolverInconsParams <ASK>}] ({\em inconsistent parameter handling}) 
499 influence the behavior of the routine for the consistency check. Admissible parameters are \verb+ASK+, \verb+BREAK+
500 and \verb+IGNORE+.
501 If  during the consistency  check a dependency between the  parameters is discovered, then with \verb+SolverInconsParams : ASK+ the users is asked for the validity of the appropriate constrained condition.  With a positive response, this is stored  for later evalutaion in the list  \verb+SolverAssumptions+. If the dependency is not admissible or if the option variable is set with \verb+BREAK+, then the solution process is aborted. If the parameter is set to \verb+IGNORE+,  then the consistency check is caused to accept basically all constrained conditions between parameters as valid as long as these do not contradict directly already made conditions.
503 \item[{\tt SolverLinear <TRUE>}] 
504 switches the {\em Linear Solver} on
505 (\verb+TRUE+) resp.\ off (\verb+FALSE+). Switching off is recommended if the system of equations, which is to be solved, does not contain linear equations or their number is very small in relation to the number of  nonlinear equations. In these cases much computing time can be saved through bypass the {\em Linear Solvers}, since the algorithm to search for linear equations is quite complex.
507 \item[{\tt SolverRepeatLinear <TRUE>}] 
508 cause repeated calls of {\em Linear Solvers}. If the variable is set to \verb+FALSE+, then  {\em Linear Solver} is executed only once.
510 \item[{\tt SolverFindAllLinearVars <TRUE>}] 
511 decides whether  {\em 
512 Linear Solver}  that looks for maximal large  pieces of linear equations regarding all available variables (\verb+TRUE+), or whether only subsystems in the variables are to be extracted, which are immediately looked for during the solution process (\verb+FALSE+). The setting of the variables plays especially a role, if under-determined systems of equations are to be solved. 
513 \nl Here \verb+SolverFindAllLinearVars : FALSE+ should to be set, because otherwise no solutions for the originally interesting variables could possibly be found due to the too small number of equations. With \verb+FALSE+ it is guaranteed that at first after these variables is solved and the degrees of freedom are expressed in the other unknowns.
515 \item[{\tt SolverValuationStrategy <MinVarPathsFirst>}] 
516  contains the name of the function, which is generate a solution order from the variable path matrix and the valuation matrix   (see section \ref{SolverValuationStrategies}). The call of the function within the {\em Valuation Solvers} is done with:
517 des {\em Valuation Solvers} mit:
518 \begin{literatim}{|}
519      SolveOrder : Apply( 
520        SolverValuationStrategy, [ VarPathMatrix, ValuationMatrix ]
521      )
522 \end{literatim}
523 As function value a list of the form
524 \begin{literatim}{|}
525      [ [i1, j1, b1], [i2, j2, b2], ... ]
526 \end{literatim}
527  is expected, which was  
528  described in section  \ref{KomplBewertung}. \nl To observe here is the option variable \verb+SolverMaxLenValOrder+.
530 \item[{\tt SolverDefaultValuation <10>}] 
531 determines the valuation factor for operators, which were not explicitly assigned such a factor with the \verb+SetProp+ instruction  (see section \ref{ChgOpValuations}).
533 \item[{\tt SolverMaxLenValOrder <5>}] ({\em maximum length of valuation order}) 
534 determines the maximal length of the solution order. If the last proposal for solution in the list does not lead to success, then the  {\em Valuation Solver} aborts the solution process, even if not all pairs of equation/variables were tried.
536 \item[{\tt SolverTransforms <[]>+}] 
537 contains a list of the names of functions, which can be applied after a unsuccessful solution attempt to the corresponding equation, in order to increase the solution chances with a renewed attempt. Thereby the functions are executed  in the order of their occurring in the list. After each function call  the next solution attempt takes place directly. If this fails, then the next transformation in the list is applied, as long as the equation could be solved or no further transformation is available. Since the possibilities for manipulations  with the transformations are quite extensive,  a more accurate specification of their definition and application is in section \ref{SolverTransforms}.
539 \item[{\tt SolverPostprocess <TRUE>}] 
541 switches the {\em Solver 
542 Postprocessor}  on (\verb+TRUE+) resp.\ off (\verb+FALSE+).  If switched to status off,  the hierarchical result list of the Solver is returned without rework, e.g. without expansion, back substitution and extraction of the variables requested by the user. This control variable serves primarily for Debug purposes.
544 \item[{\tt SolverBacksubst <TRUE>}] ({\em backsubstitution}) 
545 determines whether the {\em Solver Postprocessor}  is to execute a back substitution of the system of equations brought on triangle form (\verb+TRUE+) or not (\verb+FALSE+). If the calculated symbolic solutions are very extensive, then it is often meaningful to execute no complete back substitution, but to output some of the looked-for variables as functions of other calculated unknowns.
547 \item[{\tt SolverDispAllSols <FALSE>}] ({\em display all solutions}) 
548 instructs the Solver, if set to \verb+TRUE+,  to output {\em all} found solutions at the termination of the solution process  and not only for the variables indicated by the user.
550 \item[{\tt SolverRatSimpSols <TRUE>}] ({\em perform rational simplifications on solutions}) 
551 instructs the {\em Solver Postprocessor}  to simplify the results  with the instruction \verb+FullRatSimp+ before the output.
553 \item[{\tt SolverDumpToFile <FALSE>}] 
554  (\verb+TRUE+) instructs the {\em Valuation Solver},  to write all found solutions (after each successful solution attempt) as well as the remaining equations and variables into a Maxima batch file, whose name is saved in the option variable  \verb+SolverDumpFile+. This option is intended for extensive problems, where Maxima is inclined  to system crashes because of  acute lack of main and swap memory.
555 Within a crash,  at least a part of the results can be saved by the storage of the intermediate results.
558 \item[{\tt SolverDumpFile <"{}SOLVER.DMP"{}>}] 
559 contains the name of the file, into which the intermediate results are to be written.
561 \end{description}
564 % -----------------------------------------------------------------------------
565 %\stop  %%% STOPPED here with translation, wL 20.11.23
566 % -----------------------------------------------------------------------------
569 \section[user specific transformation routines]{Definition and
570 Integration of User Specific Transformation Routines\label{SolverTransforms}} %==================== 2.5
572 Often the {\em Valuation Solver} encounters equations during the solution process, which it is not able to solve, although already some simple rearrangements or simplifications could help, in order to receive the desired result. E.g.\  the \verb+SOLVE+ function is not able to solve the equation
573 \begin{equation}
574 x + \sin^2 x + \cos ^2 x = 1
575 \end{equation}
577 correctly for $x$, since it does not know that the square terms of sine and cosine  can be combined easyly into '1'.
579 In order to be able to execute rearrangements or simplifications of the equations depending upon the application case, the dynamic integration of user-defined transformation functions is bulid in the Solver, which are applied to unresolved equations if necessary. The  {\em Valuation
580 Solver}  transfers to these functions among other things the equation and the variable, after which the equation is to be solve. The transformation function has now the task to transform the equation and return it as its function value again to the Solver, so that a renewed solution attempt can begin.
582 The call of a transformation function from the Solver works in the following way:
584 \begin{literatim}{|}
585      Transform : CopyList( SolverTransforms ),
586        \vdots
587      SOLVER LOOP
588           \vdots
589         Trans : Pop( Transform ),
590         TransEq : Apply( Trans, [ Equation, Variable, Solution ] )
591           \vdots
592      LOOP END
593 \end{literatim}
595 Thereby  the additionally transferred parameter \verb+Solution+ contains the result of the failed solution attempt, on the basis of which possibly helpful conclusions can be drawn. The following instruction shows an example of the definition of a simple, user specific transformation routine, which tries to make an equation solvable by simplifying of trigonometric functions:
596 \begin{literatim}{|}
597      TransformTrig( Equation, Variable, Solution ) := 
598        TrigSimp( Equation )$
599 \end{literatim}
601 For the integration of the function  their name had to be inserted into the \nl global list \verb+SolverTransforms+:
602 \begin{literatim}{|}
603      SolverTransforms : [ 'TransformTrig ]$
604 \end{literatim}
607 Also the application of a transformation routine may  be unsuccessful, therefore it exists the possibility to remember the Solver the failure of the simplifying attempt by return of an empty list (\verb+[]+) as function value. In this way it is prevented that a further call of the
608 \verb+SOLVE+ function with the same equation takes place. Instead the Solver tries directly,  to execute the next transformation in the list, if available,.
609 For an alternative to the rearranging of the equation and an afterward solution by the {\em internal} Solver, a transformation routine is also allowed, to determine the solutions of the transferred equation  {\em itself} and return them in the form
610 \begin{literatim}{|}
611      [ Variable = Solution_1, Variable = Solution_2, ... ] 
612 \end{literatim}
614 A possible area of application for such functions would be the application of numeric procedures for the solution of nonlinear equations, which  contain only  one variable and no parameters. Or the equation can be manipulated by hand, 
615 whilst  the transformation routine calls a   {\em Maxima-Break}. 
616 The method for the definition and integration of transformation functions with success return, wil be demonstrated in the following completely worked example. To solve is the system of equations (\ref{Trig1}) --  (\ref{Trig3})  for the variables  $x$, $y$
617 and $z$. This task is quite simple in principle, but nevertheless it causes substantial difficulties  to the Solver.
618 \begin{eqnarray}
619         z - \sin x &=& 0 \label{Trig1} \\
620 y + z^2 + \cos x^2 &=& 5               \\
621              y + x &=& 1 \label{Trig3}
622 \end{eqnarray}
624 At first, the system of equations is input as an equation list as well as the variables:
625 \begin{literatim}{|}
626 (COM11) TrigEq :
628           z - sin(x) = 0,
629   y + z^2 + cos(x)^2 = 5,
630                y + x = 1
633 (COM12) Var : [x, y, z]$
634 \end{literatim}
636 The first solution attempt is to be executed without transformation functions:
638 \begin{literatim}{|}
639 (COM13) SolverTransforms : []$
641 (COM14) Solver( TrigEq, Var );
643 The variables to be solved for are [X, Y, Z]
644 Checking for inconsistencies...
645 ... none found.
647 Searching for linear equations...
648   ...with respect to: [X, Y, Z]
649 Found 2 linear equations in 2 variables.
650 The variables to be solved for are [Y, Z]
651 The equations are [Z - SIN(X), Y + X - 1]
652 Solving linear equations.
653 The solutions are [Y = 1 - X, Z = SIN(X)]
655 Checking for remaining equations.
656 1 equation(s) and 1 variable(s) left.
657 The variables to be solved for are [X]
658 Trying to solve equation 1 for X
659 Valuation: (irrelevant)
660                    2         2
661 The equation is SIN (X) + COS (X) - X - 4 = 0
662 Checking if equation was solved correctly.
663                           2         2
664 The solutions are [X = SIN (X) + COS (X) - 4]
665 Solution is not correct.
666 Cannot solve equation. Giving up.
668 Postprocessing results.
669 Cannot determine an explicit solution for X
671                                           2         2
672 (D14)        [[Y = 1 - X, Z = SIN(X), [SIN (X) + COS (X) - X - 4]]]
673 \end{literatim}
675 In this case the Solver is not able to solve the equation with the squared sine and cosine terms for the variable $x$ and therefore returns  the unresolved equation in implicit form as last item of the solution list. 
676 To simplifyf the equations two transformation functions are now to be defined and merged in. The first transformation serves for the simplification of logarithm terms, the second for the simplification of terms, which contain trigonometric functions. Both functions check whether their application was successful and returns an empty list, if the transformation did not cause any modification of the equation.
677 \begin{literatim}{|}
678 (COM15) TransformLog( Equation, Variable, Solution ) := BLOCK(
679   [ Eq ],
680   Eq : LogContract( Equation ),
681   IF Eq = Equation THEN
682     RETURN( [] )
683   ELSE
684     RETURN( Eq )
687 (COM16) TransformTrig( Equation, Variable, Solution ) := BLOCK(
688   [ Eq ],
689   Eq : TrigSimp( Equation ),
690   IF Eq = Equation THEN
691     RETURN( [] )
692   ELSE
693     RETURN( Eq )
695 \end{literatim} 
697 The transformation function \verb+TransformLog+ may be applied basically as first, therefore the integration of the routines takes place in the following order:
699 \begin{literatim}{|}
700 (COM17) SolverTransforms : [ 'TransformLog, 'TransformTrig ]$
701 \end{literatim}
702 Now a new run of Solver may be started.
703 \begin{literatim}{|}
704 (COM18) Solver( TrigEq, Var );
706 The variables to be solved for are [X, Y, Z]
707 Checking for inconsistencies...
708 ... none found.
710 Searching for linear equations...
711   ...with respect to: [X, Y, Z]
712 Found 2 linear equations in 2 variables.
713 The variables to be solved for are [Y, Z]
714 The equations are [Z - SIN(X), Y + X - 1]
715 Solving linear equations.
716 The solutions are [Y = 1 - X, Z = SIN(X)]
718 Checking for remaining equations.
719 1 equation(s) and 1 variable(s) left.
720 The variables to be solved for are [X]
721 Trying to solve equation 1 for X
722 Valuation: (irrelevant)
723 The equation is SIN (X) + COS (X) - X - 4 = 0
724 Checking if equation was solved correctly.
725                           2         2
726 The solutions are [X = SIN (X) + COS (X) - 4]
727 Solution is not correct.
728 \end{literatim}
730 Here the Solver recognize as in the preceded case that it cannot solve the equation and applies the first transformation in the list to it.
731 \begin{literatim}{|}
732 Applying transformation TRANSFORMLOG
733 Transformation failed.
734 \end{literatim}
736 Since the equation does not contain logarithmic functions, the simplifying attempt is not successful. Therefore the second transformation routine is tried.
737 \begin{literatim}{|}
738 Applying transformation TRANSFORMTRIG
739 The transformation yields - X - 3 = 0
740 Retrying with transformed equation.
741 Checking if equation was solved correctly.
742 The solutions are [X = - 3]
743 Solution is correct.
745 Solution 1 for X
746 Checking for inconsistencies...
747 ... none found.
748 Consistent solutions for X : [X = - 3]
749 Checking for remaining equations.
750 All variables solved for. No equations left.
751 Postprocessing results.
753 (D18)                   [[X = - 3, Y = 4, Z = - SIN(3)]]
754 \end{literatim}
756 The transformation function \verb+TransformTrig+ succeeds to simplfy the equation, so that the Solver is now able, to determine the correct solution for the variable $x$.
764 \section{Modification of the Operator Valuations\label{ChgOpValuations}}  % ch 2.6 =====================
766 To give the user of the Solver the possibility for an individual intervention of the heuristic complexity valuation of algebraic terms,  the valuations of the arithmetic operators are stored as {\em Macsyma Properties}  under the keyword \verb+Valuation+, and not as immutable constants. The definition of a valuation factor takes place with the instruction
768 \begin{literatim}{|}
769      SetProp( {\em{}Operator}, 'Valuation, {\em{}Valuation factor} )$
770 \end{literatim}
772 The standard mappings of the valuation factors are pre-defined in the Solver:
773 \begin{literatim}{|}
774      SetProp( 'sin,   'Valuation, 10 )$
775      SetProp( 'cos,   'Valuation, 10 )$
776      SetProp( 'tan,   'Valuation, 10 )$
777      SetProp( 'asin,  'Valuation, 12 )$
778      SetProp( 'acos,  'Valuation, 12 )$
779      SetProp( 'atan,  'Valuation, 12 )$
780      SetProp( 'sinh,  'Valuation, 12 )$
781      SetProp( 'cosh,  'Valuation, 12 )$
782      SetProp( 'tanh,  'Valuation, 12 )$
783      SetProp( 'asinh, 'Valuation, 12 )$
784      SetProp( 'acosh, 'Valuation, 12 )$
785      SetProp( 'atanh, 'Valuation, 12 )$
786      SetProp( "{}+"{},    'Valuation,  1 )$
787      SetProp( "{}-"{},    'Valuation,  1 )$
788      SetProp( "{}*"{},    'Valuation,  4 )$
789      SetProp( "{}/"{},    'Valuation,  4 )$
790      SetProp( "{}^"{},    'Valuation, 10 )$
791      SetProp( 'exp,   'Valuation, 10 )$
792      SetProp( 'log,   'Valuation, 10 )$
793      SetProp( 'sqrt,  'Valuation, 10 )$
794 \end{literatim}
796 E.g. if the valuation of the tanh--operator should be modified on 20, then this can be done at any time by
797 \begin{literatim}{|}
798      SetProp( 'tanh, 'Valuation, 20 )$
799 \end{literatim}
801 A quality factor can queried with the \verb+Get+ command:
802 \begin{literatim}{|}
803      Get( {\em{}Operator}, 'Valuation );
804 \end{literatim}
805 Example: The valuation of ``$*$''-- operator is determined through:
807 \begin{literatim}{|}
808 (COM19) Get( "{}*"{}, 'Valuation );
810 (D19)                                   4
811 \end{literatim}
813 If the result of the query has  the value \verb+FALSE+,  then this means that no valuation factor for the operator concerned was defined.
818 \section[User Specific Valuation Strategie]% ch 2.7 ===============================================
819 {Definition and Integration of \\User Specific Valuation Strategies%
820 \label{SolverValuationStrategies}}
822 By means of a reassignment of the procedure variable \verb+SolverValuationStrategy+ the {\em Valuation Solver} is caused to use  a user-defined valuation strategy to the determination of the solution order instead of the internal function. The function are given by their call 
823 two valuation matrices,
824 \begin{literatim}{|}
825      SolveOrder : Apply(
826        SolverValuationStrategy, [ VarPathMatrix, ValuationMatrix ]
827      )
828 \end{literatim}
829 which are the  {\em variable path matrix} and the {\em complexity valuation matrix}, whose row dimension equal the number of the equations and their column dimension equals the number of variables which are be determined.
831 The entry at the position $(i,j)$ of the {\em variable path matrix} corresponds to the number of paths to the instances of the variable $x_j$ in equation  $i$ (see section \ref{KomplBewertung}). The {\em complexity evaluation matrix} contains at the position $(i,j)$ the complexity valuation of the equation $i$
832 w.r.t. the variable $x_j$. Thus, for the system of equations (\ref{linearxyz}) -- (\ref{linearxy})
833 the path matrix reads 
836 \bordermatrix{
837                   & x & y & z \cr
838 (\ref{linearxyz}) & 1 & 1 & 1 \cr 
839 (\ref{linearx})  & 1 & 1 & 2 \cr 
840 (\ref{linearxy}) & 1 & 1 & 1 \cr 
844 %\begin{displaymath}
845 %\bordermatrixlr{\left[}{
846 %                  & x & y & z \cr
847 % & 1 & 1 & 1 \cr %(\ref{linearxyz})
848 %  & 1 & 1 & 2 \cr %(\ref{linearx}) 
849 % & 1 & 1 & 1 \cr %(\ref{linearxy}) 
850 %}{\right]}
851 %\end{displaymath}
852 and the valuation matrix using the standard operator valuation factors are determined to
854 \begin{displaymath}
855 \bordermatrix{
856                   & x & y &  z \cr
857 (\ref{linearxyz}) & 1 & 4 &  1 \cr
858 (\ref{linearx})   & 4 & 4 & 14 \cr
859 (\ref{linearxy})  & 4 & 1 & 40 \cr
861 \end{displaymath}
863 %\begin{displaymath}
864 %\bordermatrixlr{\left[}{
865 %                  & x & y &  z \cr
866 %(\ref{linearxyz}) & 1 & 4 &  1 \cr
867 %(\ref{linearx})   & 4 & 4 & 14 \cr
868 %(\ref{linearxy})  & 4 & 1 & 40 \cr
869 %}{\right]}
870 %\end{displaymath}
872 \noindent
873 From these matrices the valuation strategy must generate  a solution order (see section \ref{KomplBewertung})) in the form
875 \begin{literatim}{|}
876      [ [i1, j1, b1], [i2, j2, b2], ...  ]
877 \end{literatim}
878 The maximal length of the list should not be larger than the value of the option variable \verb+SolverMaxLenValOrder+.
880 The basic structure of an valuation strategy is given by the following pseudocode:
882 \begin{literatim}{|}
883      MyValuationStrategy( PathMat, ValMat ) := BLOCK(
884        
885        {\rm{}generate a solution order from the valuation strategies} 
886        {\rm{}limit the length of the list to} SolverMaxLenValOrder  {\rm{}elements}
888        RETURN( {\rm{}the solution order} )
889      )$
890 \end{literatim}
892 \noindent
893 To insert the function afterwards, the procedure variable \verb+SolverValuationStrategy+ is to assign with the function name:
895 \begin{literatim}{|}
896      SolverValuationStrategy : 'MyValuationStrategy$
897 \end{literatim}