Fortress

Сделаю.

Реализовал операцию в виде метода со следующей сигнатурой:

public static SolverOperation makeSolverOperation(EVerilogOperation type, int times, BigInteger bitVector)

класс HDLOperations

r71

В общем случае репликация применяется к выражениям; число повторений - также выражение: expression1{expression2}.

BVREPL лучше сделать обыкновенной бинарной операцией (первый аргумент - вектор, второй - число повторений).

Саша, я нашел в языке SMT-LIB параметризованную операцию repeat, которая довольно похожа на репликацию.

((_ repeat i) (_ BitVec m) (_ BitVec i*m))
- ((_ repeat i) x) means concatenate i copies of x


К сожалению, в качестве числа повторений тут может выступать только число типа Int. Нельзя ни подставить туда переменную типа Int, ни арифметическое выражение.

Насколько я понимаю, данную операцию (а также все параметризованные) нужно хранить так же, как и все обычные операции языка SMT-LIB, но в транслятор добавить специальный кусок кода для правильного отображения параметров операций на SMT-LIB. Верно?

Нужно сделать так, чтобы в качестве первого аргумента (параметра repeat) можно было задавать произвольную операцию. При отображении в SMT-LIB нужно ругаться, если операция не является константной (или даже не является числом).

В этом случае я смогу представить все операции Verilog (кроме вызовов функций) с помощью API.

Это предварительное представление. Следующий этап - вычисление константных выражений (константные выражения схлопнутся в числа, и проблем с отображением в SMT-LIB не будет).

Реализовал поддержку операции repeat, а также вычисление константных выражений. В числа сейчас схлопываются только Integer'ы, в будущем можно расширить данный функционал и на все существующие в библиотеке типы.

r82