How to rotate a bitvector in cvc4 using c++ API

Question

I try to rotate a bitvector in cvc4 using the C++ API, but the API is a little bit confusing when it comes to operator expressions.

Using the following code (extract):

#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;
}

Executing this yields:

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

Does anybody know how to deal with the operator construct of cvc4?

Answer 1

See below for the correct construction of a rotate left expression. In general, whenever you have an expression operator that is itself an expression, you apply it by simply calling mkExpr and passing the operator expression as the first argument.

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