
## 9. Future Work

The current system (with the presented semantics and the corresponding implementation) uses one way (binary representation) for representing (unsigned) integers but (as shown in the given examples), it still enables using different encoding styles in specifications. For further convenience, we are planning to natively support other representations for integers, so the user could choose among several encodings. Also, signed integers and floating point numbers could be supported.

The language ursa **(and the interpreter) can be extended by new language constructs**
(e.g., by division). A new form of the assert **can be added, such that it propagates intermediate solutions to subsequent commands of the same sort. Support for global constraints can**
also be developed, but primarily only as a ,,syntactic sugar" - the user could express global constraints more easily, but internally they would be expanded as if they were expressed using loops (i.e., as in the current version of the system). Alternative forms of support for global constraints would require substantial changes in the sat**-reduction mechanism.**
On the lower algorithmic and implementation level, we are planning to further improve the current version of transformation to cnf.

In the current version, ground integers are represented by built-in fixed-precision integers, which is typically sufficient. However, in order to match symbolic integers, ground integers should be represented by arbitrary (but fixed) length integers and we are planning to implement that.

Concerning the underlying sat **solvers, currently only two complete** sat **solvers are**
used. We are planning to integrate additional solvers, since some solvers are better suited to some sorts of input instances, as the sat **competitions show. Within this direction of** work, we will also analyze performance of stochastic solvers within ursa**. In addition,** we are exploring potentials of using non-cnf sat **solvers [67, 53, 38] within** ursa**, which**
avoids the need for transformation to cnf **[69]. Choosing among available solvers can be** automated by using machine learning techniques for analysis of the generated sat **instances**
(or even input specifications) [73, 55]. For solving optimization problems, instead of the existing naive implementation, we are planning to implement more advanced approaches and to explore the use of MaxSAT and pseudo-Boolean solvers [3].

On the theoretical side, the full operational semantics outlined in this paper can be formally defined and it could be proved that solutions produced by the ursa **system indeed** meet the specifications and if there are no produced solutions, then the specifications is inconsistent. Along with the formal verification (i.e., verification within a proof assistant)
of the sat **solver** ArgoSAT **used [45, 44], that would provide a formal correctness proof** of the ursa system (which would make it, probably, the first trusted **constraint solver).**
In the presented version of ursa**, reducing to** sat **is tightly integrated (and defined by**
the semantics of the system) in the program execution phase. **An alternative would be as** follows: during the program execution phase, a first-order formula is generated and only before the solving phase it is translated to a propositional **formula. Moreover, the generated** formula would not need to be translated to a propositional formula, but could be tested for satisfiability by using smt **(satisfiability modulo theory) solvers (e.g., for linear arithmetic,** equality theory, alldifferent theory etc.) [2]. In particular, symbolic computations employed by the ursa **system are closely related to the theory of bit-vector arithmetic and to decision**
procedures for this theory based on "bit-blasting" [8, 9]. Since solvers for this theory typically cover all the operators used in ursa, the theory of bit-vector arithmetic can be