z3 C++ api模运算整数

Question

有没有办法用z3 C++ api做整数模运算？

我试图做这样的事情：

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

似乎有只为bitvectors模操作？

我错过了什么吗？

最佳 托比亚斯

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);