Project

General

Profile

Edit History

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

Andrei Tatarnikov, 12/21/2011 12:53 PM

1 3 Andrei Tatarnikov 
h1. Constraint Solver
2 1 Alexander Kamkin 





    3
    7
    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.





    4
    6
    Andrei Tatarnikov
    





    5
    7
    Andrei Tatarnikov
    
The subsystem uses an 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
    
    
    
It is based on 





    8
    
    
    





    9
    
    
    





    10
    
    
    





    11
    1
    Alexander Kamkin
    
h1. Constraint Solver Library





    12
    3
    Andrei Tatarnikov
    





    13
    
    
    
The ru.ispras.microtesk.constraints package includes the following sub-packages:





    14
    
    
    





    15
    
    
    





    16
    
    
    





    17
    
    
    
h2. Language-independent syntax tree





    18
    
    
    





    19
    
    
    





    20
    
    
    





    21
    
    
    





    22
    
    
    
h1. База данных ограничений





    23
    
    
    





    24
    
    
    
База данных ограничений строится автоматически в результате анализа формализованных спецификаций системы команд микропроцессора, выполненной на одном из ADL-языков (например, nML). Некоторые ситуации могут описываться вручную и добавляться в базу данных ограничений.