Task #4523
openImplementing a solver for simple constraints
0%
Description
Цель - генерация рандомизированных данных, удовлетворяющих несложным ограничениям (constrained random generation).
- Определить и описать в Wiki класс рассматриваемых ограничений.
- Реализовать солвер (постараться добиться равномерного распределение данных, удовлетворяющих ограничениям).
- Протестировать солвер (не берется за сложные ограничения, решает простые ограничения, решает их правильно, распределение данных близко к равномерному).
Files
Updated by Alexander Kamkin about 11 years ago
Генератор случайных чисел лучше взять из MicroTESK и перенести в Java Constraint Solver API.
Updated by Alexander Kamkin almost 11 years ago
- Subject changed from Создание солвера простых ограничений to [solver] Создание солвера простых ограничений
Updated by Alexander Kamkin over 10 years ago
Андрей перенесет рандомизатор, но где солвер?
Updated by Alexander Kamkin almost 10 years ago
- 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.
Updated by Alexander Kamkin almost 10 years ago
- Subject changed from [solver] Создание солвера простых ограничений to [solver] Implementing a solver for simple constraints
Updated by Sergey Smolov over 9 years ago
- File ispras_z3_temp804273368088899473.smt2 ispras_z3_temp804273368088899473.smt2 added
- File ispras_z3_temp5723932898750597270.smt2 ispras_z3_temp5723932898750597270.smt2 added
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.
Updated by Sergey Smolov over 9 years ago
- File smt2-files.zip smt2-files.zip added
Updated by Alexander Kamkin over 9 years ago
- Subject changed from [solver] Implementing a solver for simple constraints to Implementing a solver for simple constraints
- Category set to Solver
Updated by Alexander Kamkin over 9 years ago
- Target version changed from 0.3 to 0.4
Updated by Igor Melnichenko over 9 years ago
- Priority changed from Urgent to Immediate
The most currently needed expressions are of type "(x >= const) & (x <= const)".