База данных ограничений » History » Version 5
Andrei Tatarnikov, 12/21/2011 12:30 PM
| 1 | 3 | Andrei Tatarnikov | h1. Constraint Solver |
|---|---|---|---|
| 2 | 1 | Alexander Kamkin | |
| 3 | 5 | Andrei Tatarnikov | The constraint solver subsystem is aimed to provide a possibility to automatically generate test cases based on specified constraints. A constraint is represented by a set of limitations for input values. The solver finds values of input variables which will violate the limitations if there are any. The subsystem uses an SMT solver as an engine (in the current version, we use the Z3 solver by Microsoft Research). |
| 4 | 3 | Andrei Tatarnikov | |
| 5 | It is based on |
||
| 6 | |||
| 7 | |||
| 8 | |||
| 9 | 1 | Alexander Kamkin | h1. Constraint Solver Library |
| 10 | 3 | Andrei Tatarnikov | |
| 11 | The ru.ispras.microtesk.constraints package includes the following sub-packages: |
||
| 12 | |||
| 13 | |||
| 14 | |||
| 15 | h2. Language-independent syntax tree |
||
| 16 | |||
| 17 | |||
| 18 | |||
| 19 | |||
| 20 | h1. База данных ограничений |
||
| 21 | |||
| 22 | База данных ограничений строится автоматически в результате анализа формализованных спецификаций системы команд микропроцессора, выполненной на одном из ADL-языков (например, nML). Некоторые ситуации могут описываться вручную и добавляться в базу данных ограничений. |