After starting the program, it asks for the inputs described in Chapter 3. Example inputs are contained in the distribution package. For controlling the solver further, one can use arguments when calling the program. These arguments are described when calling the solver by rsolver -h.
Note that the efficiency of the algorithm depends on the specific form, an input constraint is given. For example, a constraint of the form ∀x is handled in a different way than a constraint of the form ∀xϕ1 ∧∀xϕ2.
Usually (but not always!) the following transformations increase the efficiency:
Other possibilities of influencing the efficiency of RSolver are the following:
If RSolver still cannot solve your problem, we strongly encourage you to contact us ( ). Your feedback will be essential for improving the software further.