Как повернуть битвектор в cvc4 с помощью API c ++

Question

Как повернуть битвектор в cvc4 с помощью API c ++

Я пытаюсь повернуть битовый вектор в 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?

0

c++cvc4

Решение

Другие решения

Других решений пока нет …

Источник

Accepted Answer

Ниже приведена правильная конструкция выражения поворота влево. В общем, когда у вас есть оператор выражения, который сам является выражением, вы применяете его, просто вызывая 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;
}

2