如何在cvc4中使用c++ API旋转位向量

Question

我尝试使用cvc4中的位向量旋转C++ API，但是当涉及到运算符表达式时，这个API有点混乱。

使用以下代码(摘录)：

#include <iostream>
#include <cvc4/cvc4.h>

using namespace std;
using namespace CVC4;

int main() {
    ExprManager em;
    SmtEngine smt(&em);
    smt.setLogic("QF_BV");
    Type bitvector32 = em.mkBitVectorType(32);
    Integer i = Integer(1, 10);      
    BitVector bv = BitVector(32, i);     
    Expr expr = em->mkConst(bv);

    BitVectorRotateLeft bv_rl = BitVectorRotateLeft(1);                   
    Expr e_bv_rl = em->mkConst(bv_rl);                                       
    Expr e_op_rl = em->operatorOf(kind::BITVECTOR_ROTATE_LEFT_OP);           
    Expr e_op_e  = em->mkExpr(e_op_rl, e_bv_rl);                              
    Expr e       = em->mkExpr(Kind::BITVECTOR_ROTATE_LEFT, e_op_e, expr); 

    return 0;
}

执行此操作将产生以下结果：

terminate called after throwing an instance of 'CVC4::IllegalArgumentException'
  what():  Illegal argument detected
CVC4::Expr CVC4::ExprManager::mkExpr(CVC4::Expr, CVC4::Expr)

  `opExpr' is a bad argument; expected (opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED) to hold
This Expr constructor is for parameterized kinds only
Aborted

有人知道如何处理cvc4的操作符构造吗？

Answer 1

有关旋转左表达式的正确结构，请参见下面的内容。通常，每当您有一个本身就是表达式的表达式运算符时，只需调用mkExpr并将运算符表达式作为第一个参数来应用。

int main() {
  ExprManager em;
  SmtEngine smt(&em);
  smt.setLogic("QF_BV");
  Type bitvector32 = em.mkBitVectorType(32);
  BitVector bv = BitVector(32, 1U);     
  Expr expr = em.mkConst(bv);

  BitVectorRotateLeft bv_rl = BitVectorRotateLeft(1);                   
  Expr e_bv_rl = em.mkConst(bv_rl);                                       
  Expr e  = em.mkExpr(e_bv_rl, expr);                              
  cout << e;

  return 0;
}