Skip to content

Commit 2dc7bee

Browse files
romainbrenguierromainbrenguier
committed
Replacing throws by invariants in boolbv convert
1 parent f1d787b commit 2dc7bee

File tree

1 file changed

+20
-59
lines changed

1 file changed

+20
-59
lines changed

‎src/solvers/flattening/boolbv.cpp‎

Lines changed: 20 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -433,13 +433,7 @@ bvt boolbvt::convert_function_application(
433433

434434
literalt boolbvt::convert_rest(const exprt &expr)
435435
{
436-
if(expr.type().id()!=ID_bool)
437-
{
438-
error() << "boolbvt::convert_rest got non-boolean operand: "
439-
<< expr.pretty() << eom;
440-
throw 0;
441-
}
442-
436+
PRECONDITION(expr.type().id() == ID_bool);
443437
const exprt::operandst &operands=expr.operands();
444438

445439
if(expr.id()==ID_typecast)
@@ -451,9 +445,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
451445
return convert_verilog_case_equality(to_binary_relation_expr(expr));
452446
else if(expr.id()==ID_notequal)
453447
{
454-
if(expr.operands().size()!=2)
455-
throw "notequal expects two operands";
456-
448+
DATA_INVARIANT(expr.operands().size() == 2, "notequal expects two operands");
457449
return !convert_equality(equal_exprt(expr.op0(), expr.op1()));
458450
}
459451
else if(expr.id()==ID_ieee_float_equal ||
@@ -480,57 +472,37 @@ literalt boolbvt::convert_rest(const exprt &expr)
480472
else if(expr.id()==ID_index)
481473
{
482474
bvt bv=convert_index(to_index_expr(expr));
483-
484-
if(bv.size()!=1)
485-
throw "convert_index returned non-bool bitvector";
486-
475+
CHECK_RETURN(bv.size() == 1);
487476
return bv[0];
488477
}
489478
else if(expr.id()==ID_member)
490479
{
491480
bvt bv=convert_member(to_member_expr(expr));
492-
493-
if(bv.size()!=1)
494-
throw "convert_member returned non-bool bitvector";
495-
481+
CHECK_RETURN(bv.size() == 1);
496482
return bv[0];
497483
}
498484
else if(expr.id()==ID_case)
499485
{
500486
bvt bv=convert_case(expr);
501-
502-
if(bv.size()!=1)
503-
throw "convert_case returned non-bool bitvector";
504-
487+
CHECK_RETURN(bv.size() == 1);
505488
return bv[0];
506489
}
507490
else if(expr.id()==ID_cond)
508491
{
509492
bvt bv=convert_cond(expr);
510-
511-
if(bv.size()!=1)
512-
throw "convert_cond returned non-bool bitvector";
513-
493+
CHECK_RETURN(bv.size() == 1);
514494
return bv[0];
515495
}
516496
else if(expr.id()==ID_sign)
517497
{
518-
if(expr.operands().size()!=1)
519-
throw "sign expects one operand";
520-
498+
DATA_INVARIANT(expr.operands().size() == 1, "sign expects one operand");
521499
const bvt &bv=convert_bv(operands[0]);
522-
523-
if(bv.empty())
524-
throw "sign operator takes one non-empty operand";
525-
526-
if(operands[0].type().id()==ID_signedbv)
500+
CHECK_RETURN(!bv.empty());
501+
const irep_idt type_id = operands[0].type().id();
502+
if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
527503
return bv[bv.size()-1];
528-
else if(operands[0].type().id()==ID_unsignedbv)
504+
if(type_id == ID_unsignedbv)
529505
return const_literal(false);
530-
else if(operands[0].type().id()==ID_fixedbv)
531-
return bv[bv.size()-1];
532-
else if(operands[0].type().id()==ID_floatbv)
533-
return bv[bv.size()-1];
534506
}
535507
else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
536508
expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
@@ -542,64 +514,53 @@ literalt boolbvt::convert_rest(const exprt &expr)
542514
return convert_overflow(expr);
543515
else if(expr.id()==ID_isnan)
544516
{
545-
if(expr.operands().size()!=1)
546-
throw "isnan expects one operand";
547-
517+
DATA_INVARIANT(expr.operands().size() == 1, "isnan expects one operand");
548518
const bvt &bv=convert_bv(operands[0]);
549519

550520
if(expr.op0().type().id()==ID_floatbv)
551521
{
552522
float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
553523
return float_utils.is_NaN(bv);
554524
}
555-
else if(expr.op0().type().id()==ID_fixedbv)
525+
else if(expr.op0().type().id() == ID_fixedbv)
556526
return const_literal(false);
557527
}
558528
else if(expr.id()==ID_isfinite)
559529
{
560-
if(expr.operands().size()!=1)
561-
throw "isfinite expects one operand";
562-
530+
DATA_INVARIANT(expr.operands().size() == 1, "isfinite expects one operand");
563531
const bvt &bv=convert_bv(operands[0]);
564-
565532
if(expr.op0().type().id()==ID_floatbv)
566533
{
567534
float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
568535
return prop.land(
569536
!float_utils.is_infinity(bv),
570537
!float_utils.is_NaN(bv));
571538
}
572-
else if(expr.op0().type().id()==ID_fixedbv)
539+
else if(expr.op0().type().id() == ID_fixedbv)
573540
return const_literal(true);
574541
}
575542
else if(expr.id()==ID_isinf)
576543
{
577-
if(expr.operands().size()!=1)
578-
throw "isinf expects one operand";
579-
544+
DATA_INVARIANT(expr.operands().size() == 1, "isinf expects one operand");
580545
const bvt &bv=convert_bv(operands[0]);
581-
582546
if(expr.op0().type().id()==ID_floatbv)
583547
{
584548
float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
585549
return float_utils.is_infinity(bv);
586550
}
587-
else if(expr.op0().type().id()==ID_fixedbv)
551+
else if(expr.op0().type().id() == ID_fixedbv)
588552
return const_literal(false);
589553
}
590554
else if(expr.id()==ID_isnormal)
591555
{
592-
if(expr.operands().size()!=1)
593-
throw "isnormal expects one operand";
594-
595-
const bvt &bv=convert_bv(operands[0]);
596-
556+
DATA_INVARIANT(expr.operands().size() == 1, "isnormal expects one operand");
597557
if(expr.op0().type().id()==ID_floatbv)
598558
{
559+
const bvt &bv = convert_bv(operands[0]);
599560
float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
600561
return float_utils.is_normal(bv);
601562
}
602-
else if(expr.op0().type().id()==ID_fixedbv)
563+
else if(expr.op0().type().id() == ID_fixedbv)
603564
return const_literal(true);
604565
}
605566

0 commit comments

Comments
 (0)