diff --git a/CHANGELOG b/CHANGELOG index 1d4611d33..8d6d9cd54 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -6,6 +6,7 @@ * SystemVerilog: fix for #-# and #=# for empty matches * SystemVerilog: fix for |-> and |=> for empty matches * LTL/SVA to Buechi with --buechi +* SMV: abs, bool, count, max, min, toint, word1 # EBMC 5.6 diff --git a/regression/smv/expressions/smv_abs1.desc b/regression/smv/expressions/smv_abs1.desc new file mode 100644 index 000000000..ff2a71c9d --- /dev/null +++ b/regression/smv/expressions/smv_abs1.desc @@ -0,0 +1,13 @@ +KNOWNBUG +smv_abs1.smv + +^\[.*\] abs\(0\) = 0: PROVED .*$ +^\[.*\] abs\(1\) = 1: PROVED .*$ +^\[.*\] abs\(2\) = 2: PROVED .*$ +^\[.*\] abs\(-1\) = 1: PROVED .*$ +^\[.*\] abs\(-2\) = 2: PROVED .*$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Unary minus on ranges does not work. diff --git a/regression/smv/expressions/smv_abs1.smv b/regression/smv/expressions/smv_abs1.smv new file mode 100644 index 000000000..a6dafa10f --- /dev/null +++ b/regression/smv/expressions/smv_abs1.smv @@ -0,0 +1,7 @@ +MODULE main + +CTLSPEC abs(0) = 0 +CTLSPEC abs(1) = 1 +CTLSPEC abs(2) = 2 +CTLSPEC abs(-1) = 1 +CTLSPEC abs(-2) = 2 diff --git a/regression/smv/expressions/smv_bool1.desc b/regression/smv/expressions/smv_bool1.desc new file mode 100644 index 000000000..039b99f06 --- /dev/null +++ b/regression/smv/expressions/smv_bool1.desc @@ -0,0 +1,11 @@ +CORE +smv_bool1.smv + +^\[.*\] !bool\(0\): PROVED .*$ +^\[.*\] bool\(1\): PROVED .*$ +^\[.*\] bool\(2\): PROVED .*$ +^\[.*\] !bool\(0ud1_0\): PROVED .*$ +^\[.*\] bool\(0ud1_1\): PROVED .*$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/smv/expressions/smv_bool1.smv b/regression/smv/expressions/smv_bool1.smv new file mode 100644 index 000000000..431339d97 --- /dev/null +++ b/regression/smv/expressions/smv_bool1.smv @@ -0,0 +1,7 @@ +MODULE main + +CTLSPEC !bool(0) +CTLSPEC bool(1) +CTLSPEC bool(2) +CTLSPEC !bool(uwconst(0, 1)) +CTLSPEC bool(uwconst(1, 1)) diff --git a/regression/smv/expressions/smv_count1.desc b/regression/smv/expressions/smv_count1.desc new file mode 100644 index 000000000..3486c98a6 --- /dev/null +++ b/regression/smv/expressions/smv_count1.desc @@ -0,0 +1,12 @@ +CORE broken-smt-backend +smv_count1.smv + +^\[.*\] count\(FALSE\) = 0: PROVED .*$ +^\[.*\] count\(TRUE\) = 1: PROVED .*$ +^\[.*\] count\(FALSE, TRUE\) = 1: PROVED .*$ +^\[.*\] count\(TRUE, FALSE\) = 1: PROVED .*$ +^\[.*\] count\(TRUE, TRUE, TRUE\) = 3: PROVED .*$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/expressions/smv_count1.smv b/regression/smv/expressions/smv_count1.smv new file mode 100644 index 000000000..7983a4916 --- /dev/null +++ b/regression/smv/expressions/smv_count1.smv @@ -0,0 +1,7 @@ +MODULE main + +CTLSPEC count(FALSE) = 0 +CTLSPEC count(TRUE) = 1 +CTLSPEC count(FALSE, TRUE) = 1 +CTLSPEC count(TRUE, FALSE) = 1 +CTLSPEC count(TRUE, TRUE, TRUE) = 3 diff --git a/regression/smv/expressions/smv_max1.desc b/regression/smv/expressions/smv_max1.desc new file mode 100644 index 000000000..d62f75415 --- /dev/null +++ b/regression/smv/expressions/smv_max1.desc @@ -0,0 +1,11 @@ +CORE +smv_max1.smv + +^\[.*\] max\(0, 1\) = 1: PROVED .*$ +^\[.*\] max\(-1, -2\) = -1: PROVED .*$ +^\[.*\] max\(-1, 1\) = 1: PROVED .*$ +^\[.*\] max\(1, 2\) = 2: PROVED .*$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/expressions/smv_max1.smv b/regression/smv/expressions/smv_max1.smv new file mode 100644 index 000000000..c8ae6654b --- /dev/null +++ b/regression/smv/expressions/smv_max1.smv @@ -0,0 +1,6 @@ +MODULE main + +CTLSPEC max(0, 1) = 1 +CTLSPEC max(-1, -2) = -1 +CTLSPEC max(-1, 1) = 1 +CTLSPEC max(1, 2) = 2 diff --git a/regression/smv/expressions/smv_min1.desc b/regression/smv/expressions/smv_min1.desc new file mode 100644 index 000000000..36cc58e55 --- /dev/null +++ b/regression/smv/expressions/smv_min1.desc @@ -0,0 +1,11 @@ +CORE +smv_min1.smv + +^\[.*\] min\(0, 1\) = 0: PROVED .*$ +^\[.*\] min\(-1, -2\) = -2: PROVED .*$ +^\[.*\] min\(-1, 1\) = -1: PROVED .*$ +^\[.*\] min\(1, 2\) = 1: PROVED .*$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/expressions/smv_min1.smv b/regression/smv/expressions/smv_min1.smv new file mode 100644 index 000000000..8f95c7bec --- /dev/null +++ b/regression/smv/expressions/smv_min1.smv @@ -0,0 +1,6 @@ +MODULE main + +CTLSPEC min(0, 1) = 0 +CTLSPEC min(-1, -2) = -2 +CTLSPEC min(-1, 1) = -1 +CTLSPEC min(1, 2) = 1 diff --git a/regression/smv/expressions/smv_toint1.desc b/regression/smv/expressions/smv_toint1.desc new file mode 100644 index 000000000..805020b83 --- /dev/null +++ b/regression/smv/expressions/smv_toint1.desc @@ -0,0 +1,14 @@ +KNOWNBUG +smv_toint1.smv + +^\[.*\] toint\(0\) = 0: PROVED .*$ +^\[.*\] toint\(1\) = 1: PROVED .*$ +^\[.*\] toint\(FALSE\) = 0: PROVED .*$ +^\[.*\] toint\(TRUE\) = 1: PROVED .*$ +^\[.*\] toint\(0ud8_1\) = 1: PROVED .*$ +^\[.*\] toint\(-0sd8_1\) = -1: PROVED .*$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Missing typecasts. diff --git a/regression/smv/expressions/smv_toint1.smv b/regression/smv/expressions/smv_toint1.smv new file mode 100644 index 000000000..8a37f6c59 --- /dev/null +++ b/regression/smv/expressions/smv_toint1.smv @@ -0,0 +1,8 @@ +MODULE main + +CTLSPEC toint(0) = 0 +CTLSPEC toint(1) = 1 +CTLSPEC toint(FALSE) = 0 +CTLSPEC toint(TRUE) = 1 +CTLSPEC toint(uwconst(1, 8)) = 1 +CTLSPEC toint(swconst(-1, 8)) = -1 diff --git a/regression/smv/expressions/smv_word1.desc b/regression/smv/expressions/smv_word1.desc new file mode 100644 index 000000000..bc2d61233 --- /dev/null +++ b/regression/smv/expressions/smv_word1.desc @@ -0,0 +1,9 @@ +CORE +smv_word1.smv + +^\[.*\] word1\(FALSE\) = 0ud1_0: PROVED .*$ +^\[.*\] word1\(TRUE\) = 0ud1_1: PROVED .*$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/expressions/smv_word1.smv b/regression/smv/expressions/smv_word1.smv new file mode 100644 index 000000000..154998465 --- /dev/null +++ b/regression/smv/expressions/smv_word1.smv @@ -0,0 +1,4 @@ +MODULE main + +CTLSPEC word1(FALSE) = uwconst(0, 1) +CTLSPEC word1(TRUE) = uwconst(1, 1) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 8769bea75..c2f4ddd0d 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -17,12 +17,18 @@ IREP_ID_ONE(F) IREP_ID_ONE(E) IREP_ID_ONE(G) IREP_ID_ONE(X) +IREP_ID_ONE(smv_abs) IREP_ID_ONE(smv_bitimplies) +IREP_ID_ONE(smv_bool) +IREP_ID_ONE(smv_count) IREP_ID_ONE(smv_extend) +IREP_ID_ONE(smv_max) +IREP_ID_ONE(smv_min) IREP_ID_ONE(smv_next) IREP_ID_ONE(smv_iff) IREP_ID_TWO(C_smv_iff, "#smv_iff") IREP_ID_ONE(smv_resize) +IREP_ID_ONE(smv_toint) IREP_ID_ONE(smv_set) IREP_ID_ONE(smv_setin) IREP_ID_ONE(smv_setnotin) @@ -32,6 +38,7 @@ IREP_ID_ONE(smv_swconst) IREP_ID_ONE(smv_union) IREP_ID_ONE(smv_unsigned_cast) IREP_ID_ONE(smv_uwconst) +IREP_ID_ONE(smv_word1) IREP_ID_ONE(smv_H) IREP_ID_ONE(smv_bounded_H) IREP_ID_ONE(smv_O) diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index 8ab58b3e7..7d9ca12ed 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -831,6 +831,27 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src) else if(src.id() == ID_smv_unsigned_cast) return convert_function_application("unsigned", src); + else if(src.id() == ID_smv_abs) + return convert_function_application("abs", src); + + else if(src.id() == ID_smv_bool) + return convert_function_application("bool", src); + + else if(src.id() == ID_smv_count) + return convert_function_application("count", src); + + else if(src.id() == ID_smv_max) + return convert_function_application("max", src); + + else if(src.id() == ID_smv_min) + return convert_function_application("min", src); + + else if(src.id() == ID_smv_toint) + return convert_function_application("toint", src); + + else if(src.id() == ID_smv_word1) + return convert_function_application("word1", src); + else if(src.id() == ID_typecast) { return convert_typecast(to_typecast_expr(src)); diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index c51f3c2d5..471303b12 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -94,6 +94,12 @@ Function: init stack_expr(x_result).add_to_operands(std::move(lhs), std::move(rhs)); } +static void unary(YYSTYPE &result, const irep_idt &id, YYSTYPE &op) +{ + init(result, id); + mto(result, op); +} + /*******************************************************************\ Function: j_binary @@ -234,6 +240,7 @@ static void new_module(YYSTYPE &module) %token xor_Token "xor" %token xnor_Token "xnor" %token self_Token "self" +%token toint_Token "toint" %token TRUE_Token "TRUE" %token FALSE_Token "FALSE" %token count_Token "count" @@ -684,6 +691,9 @@ term : constant | variable_identifier | '(' formula ')' { $$=$2; } | NOT_Token term { init($$, ID_not); mto($$, $2); } + | "abs" '(' term ')' { unary($$, ID_smv_abs, $3); } + | "max" '(' term ',' term ')' { binary($$, $3, ID_smv_max, $5); } + | "min" '(' term ',' term ')' { binary($$, $3, ID_smv_min, $5); } | term AND_Token term { j_binary($$, $1, ID_and, $3); } | term OR_Token term { j_binary($$, $1, ID_or, $3); } | term xor_Token term { j_binary($$, $1, ID_xor, $3); } @@ -706,11 +716,15 @@ term : constant | term GTGT_Token term { binary($$, $1, ID_shr, $3); } | term LTLT_Token term { binary($$, $1, ID_shl, $3); } | term COLONCOLON_Token term { binary($$, $1, ID_concatenation, $3); } + | "word1" '(' term ')' { unary($$, ID_smv_word1, $3); } + | "bool" '(' term ')' { unary($$, ID_smv_bool, $3); } + | "toint" '(' term ')' { unary($$, ID_smv_toint, $3); } + | "count" '(' term_list ')' { $$=$3; stack_expr($$).id(ID_smv_count); } | swconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_swconst, $5); } | uwconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_uwconst, $5); } - | signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); } - | unsigned_Token '(' term ')' { init($$, ID_smv_unsigned_cast); mto($$, $3); } - | sizeof_Token '(' term ')' { init($$, ID_smv_sizeof); mto($$, $3); } + | signed_Token '(' term ')' { unary($$, ID_smv_signed_cast, $3); } + | unsigned_Token '(' term ')' { unary($$, ID_smv_unsigned_cast, $3); } + | sizeof_Token '(' term ')' { unary($$, ID_smv_sizeof, $3); } | extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); } | resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); } | term union_Token term { binary($$, $1, ID_smv_union, $3); } @@ -791,6 +805,11 @@ set_body_expr: | set_body_expr ',' formula { $$=$1; mto($$, $3); } ; +term_list: + term { init($$); mto($$, $1); } + | term_list ',' term { $$=$1; mto($$, $3); } + ; + identifier : IDENTIFIER_Token | QIDENTIFIER_Token { diff --git a/src/smvlang/scanner.l b/src/smvlang/scanner.l index a69c9894e..289115877 100644 --- a/src/smvlang/scanner.l +++ b/src/smvlang/scanner.l @@ -121,6 +121,7 @@ void newlocation(YYSTYPE &x) "extend" token(extend_Token); "resize" token(resize_Token); "sizeof" token(sizeof_Token); +"toint" token(toint_Token); "uwconst" token(uwconst_Token); "swconst" token(swconst_Token); diff --git a/src/smvlang/smv_expr.h b/src/smvlang/smv_expr.h index 680608260..293e76809 100644 --- a/src/smvlang/smv_expr.h +++ b/src/smvlang/smv_expr.h @@ -11,6 +11,52 @@ Author: Daniel Kroening, dkr@amazon.com #include +class smv_abs_exprt : public unary_exprt +{ +public: + smv_abs_exprt(exprt __op, typet __type) + : unary_exprt{ID_smv_abs, std::move(__op), std::move(__type)} + { + } +}; + +inline const smv_abs_exprt &to_smv_abs_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_abs); + smv_abs_exprt::check(expr); + return static_cast(expr); +} + +inline smv_abs_exprt &to_smv_abs_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_abs); + smv_abs_exprt::check(expr); + return static_cast(expr); +} + +class smv_bool_exprt : public unary_exprt +{ +public: + smv_bool_exprt(exprt __op, typet __type) + : unary_exprt{ID_smv_bool, std::move(__op), std::move(__type)} + { + } +}; + +inline const smv_bool_exprt &to_smv_bool_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_bool); + smv_bool_exprt::check(expr); + return static_cast(expr); +} + +inline smv_bool_exprt &to_smv_bool_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_bool); + smv_bool_exprt::check(expr); + return static_cast(expr); +} + class smv_resize_exprt : public binary_exprt { public: @@ -117,6 +163,52 @@ inline smv_extend_exprt &to_smv_extend_expr(exprt &expr) return static_cast(expr); } +class smv_max_exprt : public binary_exprt +{ +public: + smv_max_exprt(exprt __lhs, exprt __rhs) + : binary_exprt{std::move(__lhs), ID_smv_max, std::move(__rhs)} + { + } +}; + +inline const smv_max_exprt &to_smv_max_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_max); + smv_max_exprt::check(expr); + return static_cast(expr); +} + +inline smv_max_exprt &to_smv_max_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_max); + smv_max_exprt::check(expr); + return static_cast(expr); +} + +class smv_min_exprt : public binary_exprt +{ +public: + smv_min_exprt(exprt __lhs, exprt __rhs) + : binary_exprt{std::move(__lhs), ID_smv_min, std::move(__rhs)} + { + } +}; + +inline const smv_min_exprt &to_smv_min_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_min); + smv_min_exprt::check(expr); + return static_cast(expr); +} + +inline smv_min_exprt &to_smv_min_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_min); + smv_min_exprt::check(expr); + return static_cast(expr); +} + class smv_unsigned_cast_exprt : public unary_exprt { public: @@ -164,4 +256,50 @@ inline smv_signed_cast_exprt &to_smv_signed_cast_expr(exprt &expr) return static_cast(expr); } +class smv_toint_exprt : public unary_exprt +{ +public: + smv_toint_exprt(exprt __op, typet __type) + : unary_exprt{ID_smv_toint, std::move(__op), std::move(__type)} + { + } +}; + +inline const smv_toint_exprt &to_smv_toint_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_toint); + smv_toint_exprt::check(expr); + return static_cast(expr); +} + +inline smv_toint_exprt &to_smv_toint_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_toint); + smv_toint_exprt::check(expr); + return static_cast(expr); +} + +class smv_word1_exprt : public unary_exprt +{ +public: + smv_word1_exprt(exprt __op, typet __type) + : unary_exprt{ID_smv_word1, std::move(__op), std::move(__type)} + { + } +}; + +inline const smv_word1_exprt &to_smv_word1_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_word1); + smv_word1_exprt::check(expr); + return static_cast(expr); +} + +inline smv_word1_exprt &to_smv_word1_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_word1); + smv_word1_exprt::check(expr); + return static_cast(expr); +} + #endif // CPROVER_SMV_EXPR_H diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index afb103da6..f5bc8ea2e 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1091,6 +1091,111 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode) expr = from_integer(value, type).with_source_location(expr.source_location()); } + else if(expr.id() == ID_smv_abs) + { + auto &op = to_unary_expr(expr).op(); + typecheck_expr_rec(op, mode); + if(op.type().id() == ID_range) + { + // ok + auto &range_type = to_range_type(op.type()); + auto abs = [](mp_integer i) + { + if(i < 0) + i.negate(); + return i; + }; + expr.type() = + range_typet{abs(range_type.get_from()), abs(range_type.get_to())}; + } + else + { + throw errort().with_location(expr.source_location()) + << "abs expects integer"; + } + } + else if(expr.id() == ID_smv_bool) + { + auto &op = to_unary_expr(expr).op(); + typecheck_expr_rec(op, mode); + if( + op.type().id() == ID_bool || op.type().id() == ID_unsignedbv || + op.type().id() == ID_signedbv || op.type().id() == ID_range) + { + // ok + } + else + throw errort().with_location(expr.source_location()) + << "bool expects boolean, integer or word"; + + expr.type() = bool_typet{}; + } + else if(expr.id() == ID_smv_count) + { + auto &multi_ary_expr = to_multi_ary_expr(expr); + for(auto &op : multi_ary_expr.operands()) + { + typecheck_expr_rec(op, mode); + if(op.type().id() != ID_bool) + throw errort().with_location(op.source_location()) + << "count expects boolean arguments"; + } + expr.type() = range_typet{0, multi_ary_expr.operands().size()}; + } + else if(expr.id() == ID_smv_max || expr.id() == ID_smv_min) + { + auto &binary_expr = to_binary_expr(expr); + + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + + binary_expr.type() = type_union( + binary_expr.lhs().type(), + binary_expr.rhs().type(), + expr.source_location()); + + if(binary_expr.type().id() == ID_range) + { + // ok + } + else + throw errort().with_location(expr.source_location()) + << "min/max expect integers"; + + convert_expr_to(binary_expr.lhs(), binary_expr.type()); + convert_expr_to(binary_expr.rhs(), binary_expr.type()); + } + else if(expr.id() == ID_smv_toint) + { + auto &op = to_unary_expr(expr).op(); + typecheck_expr_rec(op, mode); + if(op.type().id() == ID_bool) + { + expr.type() = range_typet{0, 1}; + } + else if(op.type().id() == ID_unsignedbv || op.type().id() == ID_signedbv) + { + auto &op_type = to_integer_bitvector_type(op.type()); + expr.type() = range_typet{op_type.smallest(), op_type.largest()}; + } + else if(op.type().id() == ID_range) + { + // leave as is + expr.type() = op.type(); + } + else + throw errort().with_location(expr.source_location()) + << "toint expects boolean, integer or word"; + } + else if(expr.id() == ID_smv_word1) + { + auto &op = to_unary_expr(expr).op(); + typecheck_expr_rec(op, mode); + if(op.type().id() != ID_bool) + throw errort().with_location(op.source_location()) + << "word1 expects boolean argument"; + expr.type() = unsignedbv_typet{1}; + } else if( expr.id() == ID_shr || expr.id() == ID_shl || expr.id() == ID_lshr || expr.id() == ID_ashr) @@ -1289,11 +1394,88 @@ Function: smv_typecheckt::lower_node void smv_typecheckt::lower_node(exprt &expr) const { - if(expr.id() == ID_smv_extend) + if(expr.id() == ID_smv_abs) + { + // turn into if + auto &op = to_smv_abs_expr(expr).op(); + PRECONDITION(op.type().id() == ID_range); + auto &range_type = to_range_type(op.type()); + if(range_type.get_from() >= 0) + expr = op; // no change + else if(range_type.get_to() < 0) + { + // always negative + expr = unary_minus_exprt{op, expr.type()}; + } + else + { + expr = if_exprt{ + binary_relation_exprt{op, ID_ge, from_integer(0, op.type())}, + typecast_exprt{op, expr.type()}, + unary_minus_exprt{op, expr.type()}, + expr.type()}; + } + } + else if(expr.id() == ID_smv_bool) + { + // turn into equality + auto &op = to_smv_bool_expr(expr).op(); + if(op.type().id() == ID_bool) + expr = op; + else if(op.type().id() == ID_range) + { + auto &range = to_range_type(op.type()); + if(range.includes(0)) + expr = notequal_exprt{op, to_range_type(op.type()).zero_expr()}; + else + expr = true_exprt{}; + } + else if(op.type().id() == ID_unsignedbv) + { + expr = notequal_exprt{op, to_unsignedbv_type(op.type()).zero_expr()}; + } + else + PRECONDITION(false); + } + else if(expr.id() == ID_smv_count) + { + // turn into sum + exprt::operandst addends; + + addends.reserve(expr.operands().size()); + auto zero = from_integer(0, expr.type()); + auto one = from_integer(1, expr.type()); + + for(auto &op : expr.operands()) + addends.push_back(if_exprt{op, one, zero}); + + expr = plus_exprt{std::move(addends), expr.type()}; + } + else if(expr.id() == ID_smv_extend) { auto &smv_extend = to_smv_extend_expr(expr); expr = typecast_exprt{smv_extend.lhs(), smv_extend.type()}; } + else if(expr.id() == ID_smv_max) + { + // turn into if + auto &max_expr = to_smv_max_expr(expr); + expr = if_exprt{ + binary_relation_exprt{max_expr.lhs(), ID_ge, max_expr.rhs()}, + max_expr.lhs(), + max_expr.rhs(), + max_expr.type()}; + } + else if(expr.id() == ID_smv_min) + { + // turn into if + auto &min_expr = to_smv_min_expr(expr); + expr = if_exprt{ + binary_relation_exprt{min_expr.lhs(), ID_le, min_expr.rhs()}, + min_expr.lhs(), + min_expr.rhs(), + min_expr.type()}; + } else if(expr.id() == ID_smv_resize) { auto &smv_resize = to_smv_resize_expr(expr); @@ -1334,6 +1516,18 @@ void smv_typecheckt::lower_node(exprt &expr) const lhs.type() == rhs.type(), "lhs/rhs of in must have same type"); } } + else if(expr.id() == ID_smv_toint) + { + auto &op = to_smv_toint_expr(expr).op(); + expr = typecast_exprt{op, expr.type()}; + } + else if(expr.id() == ID_smv_word1) + { + auto &op = to_smv_word1_expr(expr).op(); + auto zero = from_integer(0, expr.type()); + auto one = from_integer(1, expr.type()); + expr = if_exprt{op, std::move(one), std::move(zero)}; + } } /*******************************************************************\