Overview

The Constraint Solver Engine is a component of the MicroTESK testing framework. It provides test generators with a Java interface to external SMT solvers and helps test data generators construct test data by solving constraints specified in test situations. In the overall MicroTESK architecture, the testing framework includes a test template processor, a testing library, and the Constraint Solver Engine, which supplies the testing library's test generators with access to external SMT solvers. [C1]

Role in test data generation

MicroTESK's constraint-based generation flow expresses test situations as constraints over instruction operands and microprocessor state. A test data generator analyzes a constraint, distinguishes constrained variables from free variables, and calls the Constraint Solver Engine to construct values for the free variables. After operand values are constructed, the generator can return control code that brings the relevant microprocessor resources into the required states. [C2]

This approach supports constraint-based random generation: different calls of a test data generator may produce different values, while each generated value set is still required to cause the specified test situation. [C2]

Solver organization

The engine is implemented as a collection of solvers encapsulated behind a generic interface. The solvers are divided into two main families: [C3]

• Universal solvers, which handle a wide range of constraint types.
• Custom solvers, which target specific test data generation tasks.

Universal solvers are built around external SMT solvers such as Yices and Z3. These solvers provide rich constraint-description capabilities, including Boolean algebra, arithmetic, logic over fixed-size bit vectors, and other theories, along with decision procedures for solving those constraints. [C4]

Java Constraint Solver API and SMT-LIB

MicroTESK uses the Java Constraint Solver API, described in the evidence as a generic interface to SMT-LIB-based constraint solvers. The API supports dynamically creating constraints in Java, mapping them to SMT-LIB descriptions, launching a solver, and transferring results back to Java. [C5]

Extensibility and custom solvers

Some test situations are difficult to express directly as SMT constraints, including situations involving floating-point arithmetic and memory management. For such cases, engineers can provide special custom solvers or generators. Custom solvers may still use SMT solvers to construct test data, but they usually add non-trivial logic for forming the constraint system and interpreting the solution. [C6]

When the design or coverage model is extended with a new type of knowledge, a corresponding custom solver may be needed. To support extension of the engine with new solvers, both universal and custom solvers implement uniform interfaces. [C6]

Position in MicroTESK

The Constraint Solver Engine belongs to MicroTESK's testing framework rather than the modeling framework. The modeling framework represents design and coverage knowledge about the target microprocessor, while the testing framework generates test programs from that model and test templates. Within the testing framework, the Constraint Solver Engine works alongside the test template processor and testing library to support constraint-driven test data construction. [C1]