Task #4523
open
Implementing a solver for simple constraints
Added by Alexander Kamkin about 11 years ago.
Updated over 9 years ago.
Description
Цель - генерация рандомизированных данных, удовлетворяющих несложным ограничениям (constrained random generation).
- Определить и описать в Wiki класс рассматриваемых ограничений.
- Реализовать солвер (постараться добиться равномерного распределение данных, удовлетворяющих ограничениям).
- Протестировать солвер (не берется за сложные ограничения, решает простые ограничения, решает их правильно, распределение данных близко к равномерному).
Files
Генератор случайных чисел лучше взять из MicroTESK и перенести в Java Constraint Solver API.
- Subject changed from Создание солвера простых ограничений to [solver] Создание солвера простых ограничений
Андрей перенесет рандомизатор, но где солвер?
- Priority changed from Normal to Urgent
Artem, the solver (even if it has not been fully implemented) should be added to Fortress. Sergey will use it in his experiments.
- Subject changed from [solver] Создание солвера простых ограничений to [solver] Implementing a solver for simple constraints
I've run the most long-term testcase for HDL Retrascope, collected 7811 SMT2-files and I've extracted some statistical data about them.
The most frequently used operations are: EQ, NOT, AND, OR. They are used in 85% cases.
About 60% of all SMT2-files contains only these 'basis' operators.
So the most wanted task for embedded simple solver is to be able to solve these simple constraints.
I've attached to this task a couple of examples of target constraints.
- Subject changed from [solver] Implementing a solver for simple constraints to Implementing a solver for simple constraints
- Category set to Solver
- Target version changed from 0.3 to 0.4
- Priority changed from Urgent to Immediate
The most currently needed expressions are of type "(x >= const) & (x <= const)".
Also available in: Atom
PDF