整数でのz3 C++ apiのモジュロ演算

Question

整数を使ってz3 C++ apiでモジュロ演算を行う方法はありますか？ビットベクトルのための唯一のモジュロ演算があるようです

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

：

私はこのような何かをしようとしていますか？

何か不足していますか？

ベスト トビアス

Answer 1

あなたが負の数のために何を期待セマンティクスに応じて2つの操作があります。彼らは "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);