Project

General

Profile

База данных ограничений » History » Version 16

Andrei Tatarnikov, 12/21/2011 01:52 PM

1 3 Andrei Tatarnikov
h1. Constraint Solver
2 1 Alexander Kamkin
3 11 Andrei Tatarnikov
The constraint solver subsystem is aimed to provide the 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 such values.
4 6 Andrei Tatarnikov
5 8 Andrei Tatarnikov
The subsystem uses a third-party SMT solver as an engine (in the current version, we use the Z3 solver by Microsoft Research). SMT solvers use a special functional language to specify constraints. The subsystem generates constructions in the SMT language and uses the engine to process them and produce the results (find values of unknown input variables).
6 3 Andrei Tatarnikov
7 9 Andrei Tatarnikov
We use language-independent syntax trees to represent constraints. These trees then are processed to generate a representation that can be understood by a particular SMT solver. The syntax tree contains the following node types:
8 13 Andrei Tatarnikov
# Constraint. This is the root node of the tree. It holds the list of unknown variables and the list of limitations for these variables.
9
# Formula. Represents a limitation expression. Can be combined with other limitations to build a more complex limitation (by applying a logic OR, AND or NOT to it). It must be a logic expression that can be solved to true or false.
10
# Operation. Represents an unary or binary operation with some unknown variable, some value or some expression as parameters.
11 14 Andrei Tatarnikov
# Variable.Represents an input variable. It can have an assigned value and, in such case, will be treated as a value. Otherwise, it is an unknown variable. A variable includes a type as an attribute.
12
# Value. Specifies some known value of the specified type which can be accessed as an attribute.
13 16 Andrei Tatarnikov
Note: Operation, Variables and Value can be treated polymorphically as syntax elements (SyntaxElement). This allows combining them to build complex expressions.
14 1 Alexander Kamkin
15 16 Andrei Tatarnikov
16 15 Andrei Tatarnikov
17
18 1 Alexander Kamkin
h1. Constraint Solver Library
19 3 Andrei Tatarnikov
20
The ru.ispras.microtesk.constraints package includes the following sub-packages:
21
22
23
24
h2. Language-independent syntax tree
25
26
27
28
29
h1. База данных ограничений
30
31
База данных ограничений строится автоматически в результате анализа формализованных спецификаций системы команд микропроцессора, выполненной на одном из ADL-языков (например, nML). Некоторые ситуации могут описываться вручную и добавляться в базу данных ограничений.