Skip to content

Commit 21997b2

Browse files
author
thk123
committed
Add documentation to convert_bitvector
1 parent 015b284 commit 21997b2

File tree

1 file changed

+5
-3
lines changed

1 file changed

+5
-3
lines changed

src/solvers/flattening/boolbv.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -152,9 +152,11 @@ bvt boolbvt::conversion_failed(const exprt &expr)
152152
return prop.new_variables(width);
153153
}
154154

155-
/// TODO
156-
/// \param expr: TODO
157-
/// \return TODO
155+
/// Converts an expression into its gate-level representation and returns a
156+
/// vector of literals corresponding to the outputs of the Boolean circuit.
157+
/// \param expr: Expression to convert
158+
/// \return A vector of literals corresponding to the outputs of the Boolean
159+
/// circuit
158160
/// \throws bitvector_conversion_exceptiont raised if converting byte_extraction
159161
/// goes wrong.
160162
/// TODO: extend for other types of conversion exception (diffblue/cbmc#2103).

0 commit comments

Comments
 (0)