z3 c++ api 带整数的模运算

Question

有没有办法用 z3 c++ api 对整数进行模运算？

我正在尝试做这样的事情：

var = context->int_const("foo");
var = var + 1; 
expr = var % 5;

似乎只有位向量的模运算？

我错过了什么吗？

最好的 托比亚斯

Answer 1

有两种操作，具体取决于您期望负数的语义。它们被暴露为“mod”和“rem”。有关算术运算的语义记录在 http://smtlib.cs.uiowa.edu/theories-Ints.shtml 上。

    /* \brief mod operator */
    friend expr mod(expr const& a, expr const& b);
    friend expr mod(expr const& a, int b);
    friend expr mod(int a, expr const& b);

    /* \brief rem operator */
    friend expr rem(expr const& a, expr const& b);
    friend expr rem(expr const& a, int b);
    friend expr rem(int a, expr const& b);