Skip to content

Commit da7d3bd

Browse files
committed
implement SMT-LIB2 repeat
The SMT-LIB2 'repeat' function replicates the given operand a given number of times. This commit maps this SMT-LIB2 function to our replicate_exprt.
1 parent 5f42fb7 commit da7d3bd

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/solvers/smt2/smt2_parser.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -675,7 +675,9 @@ exprt smt2_parsert::function_application()
675675
}
676676
else if(id == ID_repeat)
677677
{
678-
return nil_exprt();
678+
auto i = from_integer(index, integer_typet());
679+
auto width = to_unsignedbv_type(op[0].type()).get_width() * index;
680+
return replication_exprt(i, op[0], unsignedbv_typet(width));
679681
}
680682
else
681683
return nil_exprt();

0 commit comments

Comments
 (0)