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