Fortress

А пример кода для воспроизведения можно прислать?

Каюсь, неправильно сформулировал: проблема возникает не на этапе сложения, а на этапе выполнения операции (EQ INTEGER -2975976114)

ConstraintBuilder builder = new ConstraintBuilder();

builder.setName("Arithmetic");
builder.setKind(ConstraintKind.FORMULA_BASED);
builder.setDescription("Arithmetic constraint");

NodeVariable a = new NodeVariable(builder.addVariable("a", DataType.INTEGER));
NodeValue value = new NodeValue(DataType.INTEGER.valueOf("-1487988057", 10));
NodeExpr sum = new NodeExpr(StandardOperation.ADD, value, value);

builder.setInnerRep(new Formulas(new NodeExpr(StandardOperation.EQ, a, sum)));
onstraint c = builder.build();
c.getKind().getDefaultSolverId().getSolver().solve(c);

Ошибка происходит при попытке распарсить результат Z3 - число -2975976114. Оно не вмещается в тип Java int, который используется в Fortress для реализации типа SMT-LIB Int.

int x1 = -1487988057;
int y1 = -2975976114; // Не скомпилируется

int x2 = Integer.valueOf("-1487988057");
int y2 = Integer.valueOf("-2975976114"); // Сгенерирует исключение

Чтобы поддерживать числа, выходящие за пределы Java int, нужно менять внутреннюю реализацию DataTypeId.LOGIC_INTEGER (перейти на long или BigInteger). Должен заметить, что тип SMT-LIB Int - безразмерный и не будет переполняться, какие бы числа не складывалить. Если нужно работать с данными фиксированного размера, то нужно использовать битовые вектора.

Мне кажется, имеет смысл добавить переполняемый знаковый целочисленный тип данных, соответствующий int'у из Java и integer'у из Verilog'а, для которого будет выполняться равенство -1487988057 - 1487988057 = 1318991182.

В SMT-LIB есть только один тип Int и он работает так:

Код, сгенерированый Fortress:

(declare-const a Int)
(assert  (= a (+ (- 1487988057) (- 1487988057))))
(check-sat)
(get-value ( a))
(get-model)
(exit)

sat
((a (- 2975976114)))
(model 
  (define-fun a () Int
    (- 2975976114))
)

Int фиксированный длины нужно будет реализовывать как обёртку вокруг BIT_VECTOR. Т.е., что бы для данного ограничения генерировался код

(declare-const a (_ BitVec 32))
(assert  (= a (bvadd (bvneg (_ bv1487988057 32)) (bvneg (_ bv1487988057 32)))))
(check-sat)
(get-value ( a))
(get-model)
(exit)

который даст результат:

sat
((a #x4e9e354e))
(model 
  (define-fun a () (_ BitVec 32)
    #x4e9e354e)
)

#x4e9e354e - это 1318991182

Такое ограничение можно написать самостоятельно. Методы преобразования int в битововый вектор и обратно в классе BitVector есть. Нужно ли это автоматизировать пусть решает Саша.

Андрей, "чуть попозже" длится 2 месяца.