Арифметическая операция над переменной bo3 Z3

Question

У меня есть куча логических переменных в Z3, скажем ai, bj, а также ck, чтобы сформулировать мою проблему SAT. Однако в моей задаче есть три арифметических ограничения:

a1 + a2 + a3 + ... + an = 1
b1 + b2 + b3 + ... + bn = 0
c1 + c2 + c3 + ... + cn <= 1

Как я могу сформулировать эти три арифметических ограничения, используя Z3 API, не меняя тип переменной (т. Е. Все логические по умолчанию)?

Answer 1

Вы можете встраивать логические выражения в выражение if, например, вы можете написать

  if(a1,1,0) + if(a2,1,2) + ...

Как особенность специального назначения, также возможно вводить ограничения мощности непосредственно с помощью встроенных операторов мощности на этом этапе из API C,.NET и Java, но не в Python и Ocaml. Кроме того, тактика lia2pb преобразует цели, использующие выражения if-then-else (как указано выше), и преобразует их в псевдобулевые ограничения.