Project

General

Profile

Task #5177

[solver] Implement function templates

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

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

100%

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

Description

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

History

#1

Updated by Andrei Tatarnikov over 5 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.

#2

Updated by Andrei Tatarnikov about 5 years ago

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

Also available in: Atom PDF