Project

General

Profile

Edit History

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

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

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





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





    4
    
    
    





    5
    
    
    
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 languages and uses the engine to process them and produce the results (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). Некоторые ситуации могут описываться вручную и добавляться в базу данных ограничений.