summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r--src/api/cvc4cpp.cpp18
1 files changed, 9 insertions, 9 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0a365a4d5..31453b618 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1189,26 +1189,26 @@ uint32_t Op::getIndices() const
switch (k)
{
case BITVECTOR_REPEAT:
- i = d_expr->getConst<BitVectorRepeat>().repeatAmount;
+ i = d_expr->getConst<BitVectorRepeat>().d_repeatAmount;
break;
case BITVECTOR_ZERO_EXTEND:
- i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount;
+ i = d_expr->getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
break;
case BITVECTOR_SIGN_EXTEND:
- i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount;
+ i = d_expr->getConst<BitVectorSignExtend>().d_signExtendAmount;
break;
case BITVECTOR_ROTATE_LEFT:
- i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount;
+ i = d_expr->getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
break;
case BITVECTOR_ROTATE_RIGHT:
- i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount;
+ i = d_expr->getConst<BitVectorRotateRight>().d_rotateRightAmount;
break;
- case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().size; break;
+ case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().d_size; break;
case FLOATINGPOINT_TO_UBV:
- i = d_expr->getConst<FloatingPointToUBV>().bvs.size;
+ i = d_expr->getConst<FloatingPointToUBV>().bvs.d_size;
break;
case FLOATINGPOINT_TO_SBV:
- i = d_expr->getConst<FloatingPointToSBV>().bvs.size;
+ i = d_expr->getConst<FloatingPointToSBV>().bvs.d_size;
break;
case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().getIndex(); break;
default:
@@ -1232,7 +1232,7 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const
if (k == BITVECTOR_EXTRACT)
{
CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>();
- indices = std::make_pair(ext.high, ext.low);
+ indices = std::make_pair(ext.d_high, ext.d_low);
}
else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback