Project

General

Profile

Actions
Copy link

Task #4523

open

Implementing a solver for simple constraints

Added by Alexander Kamkin about 11 years ago. Updated over 9 years ago.

Status:
New
Priority:
Immediate
Assignee:
Artem Kotsynyak
Category:
Solver
Target version:
0.4
Start date:
10/03/2013
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Published in build:

Description

Цель - генерация рандомизированных данных, удовлетворяющих несложным ограничениям (constrained random generation).

  1. Определить и описать в Wiki класс рассматриваемых ограничений.
  2. Реализовать солвер (постараться добиться равномерного распределение данных, удовлетворяющих ограничениям).
  3. Протестировать солвер (не берется за сложные ограничения, решает простые ограничения, решает их правильно, распределение данных близко к равномерному).

Files

Download all files
ispras_z3_temp804273368088899473.smt2 (507 Bytes) ispras_z3_temp804273368088899473.smt2 sample of NOT-AND-EQ simple constraint Sergey Smolov, 03/16/2015 05:57 PM
ispras_z3_temp5723932898750597270.smt2 (134 Bytes) ispras_z3_temp5723932898750597270.smt2 sample of AND-OR-EQ simple constraint Sergey Smolov, 03/16/2015 05:57 PM
smt2-files.zip (14.6 MB) smt2-files.zip Sergey Smolov, 03/25/2015 01:40 PM
Actions
Copy link
 #1

Updated by Alexander Kamkin about 11 years ago

Генератор случайных чисел лучше взять из MicroTESK и перенести в Java Constraint Solver API.

Actions
Copy link
 #2

Updated by Alexander Kamkin almost 11 years ago

  • Subject changed from Создание солвера простых ограничений to [solver] Создание солвера простых ограничений
Actions
Copy link
 #3

Updated by Alexander Kamkin over 10 years ago

Андрей перенесет рандомизатор, но где солвер?

Actions
Copy link
 #4

Updated by Alexander Kamkin about 10 years ago

Что с этой задачей?

Actions
Copy link
 #5

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.

Actions
Copy link
 #6

Updated by Alexander Kamkin almost 10 years ago

  • Subject changed from [solver] Создание солвера простых ограничений to [solver] Implementing a solver for simple constraints
Actions
Copy link Download all files
 #7

Updated by Sergey Smolov almost 10 years ago

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.

Actions
Copy link
 #9

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
Actions
Copy link
 #10

Updated by Alexander Kamkin over 9 years ago

  • Target version changed from 0.3 to 0.4
Actions
Copy link
 #11

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)".

Actions
Copy link

Also available in: Atom PDF