Project

General

Profile

Actions
Copy link

Task #5177

closed

[solver] Implement function templates

Added by Andrei Tatarnikov over 10 years ago. Updated about 10 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Andrei Tatarnikov
Category:
-
Target version:
0.3
Start date:
07/31/2014
Due date:
% Done:

100%

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

Description

Реализовать возможность расширять фонкциональность солвера операциями, основанными на шаблонах функций (Описывают семейство похожих функций, опрерирующих разными типами данных. Например, битовыми векторами разной длины). Солвер должен генерировать нужную функцию из семейства, описанного шаблоном, в зависимости от типа операндов.

Actions
Copy link
 #1

Updated by Andrei Tatarnikov over 10 years ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 100

Реализовано в r549. Следующие операции реализованы как шаблоны функций и зарегистрированы в Z3 (в нашей обёртке):

ABS
MIN
MAX
BVANDR
BVNANDR
BVORR
BVNORR
BVXORR
BVXNORR

Теперь можно создавать и решать ограничения, использующие данные операции, как если бы эти операции были стандартными операциями SMT-LIB и поддерживались в Microsoft Research Z3.

Actions
Copy link
 #2

Updated by Andrei Tatarnikov about 10 years ago

  • Status changed from Resolved to Closed
  • Published in build set to 140915
Actions
Copy link

Also available in: Atom PDF