0

我尝试使用 C++ API 在 cvc4 中旋转位向量，但是当涉及到运算符表达式时，该 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 的运算符构造吗？

4

1 回答 1

2

有关左旋转表达式的正确构造，请参见下文。通常，只要您有一个本身就是表达式的表达式运算符，您只需调用 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;
}
于 2017-01-05T18:19:26.050 回答