Project

General

Profile

Actions

Task #4523

open

Implementing a solver for simple constraints

Added by Alexander Kamkin over 10 years ago. Updated almost 9 years ago.

Status:
New
Priority:
Immediate
Category:
Solver
Target version:
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

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

Also available in: Atom PDF