Как повернуть битвектор в 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; 
}