0

C++ API を使用して cvc4 で bitvector を回転させようとしましたが、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 に答える