Prototyping an mcSAT-based SMTsolver in Rust

Sammanfattning: Satisfiability modulo theories, or SMT, is the decision problem of determining whether a set of formulas is satisfiable or not, given one or more background theories. The model-constructing satisfiability calculus, or mcSAT, is a framework used for solving SMT problems. It is an alternative to the framework DPLL(T) which is commonly used for many state-of-the-art SMT solvers today, and it has shown promising results in a number of different prototypes. Today there are many SMT solvers available that are developed using C/C++. Another language that has increased in popularity is Rust, which has a focus on safety and performance. The language is designed to be memory-safe, and the compiler can analyze and eliminate many memory-safety issues at compile time. There are no known SMT solvers written in Rust today. The goal of this thesis was to define an architecture for an mcSAT-based SMT solver that can be implemented using Rust, and to create a simple prototype with some of the key parts of the architecture. A big focus is on figuring out what works well with Rust and whether there are any pitfalls with how the language works. An architecture specifically for Rust is introduced, along with an early prototype using this  architecture and a preliminary evaluation. The prototype works for simple examples using a Boolean theory. Not all of the rules of mcSAT have been implemented, and both the architecture and the prototype are in the early stages of development with room for improvements. The result shows that Rust is suitable for writing this typ    fsoftware, even though there are a few pitfalls that developers should be aware of.