Skip to content

Commit 607aec2

Browse files
committed
Document nondet_padding_exprt class
1 parent bf987e4 commit 607aec2

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/solvers/smt2_incremental/encoding/nondet_padding.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,10 @@
1313
class nondet_padding_exprt;
1414
void validate_expr(const nondet_padding_exprt &padding);
1515

16+
/// This expression serves as a placeholder for the bits which have non
17+
/// deterministic value in a larger bit vector. It is inserted in contexts where
18+
/// a subset of the bits are assigned to an expression and the remainder are
19+
/// left unspecified.
1620
class nondet_padding_exprt : public expr_protectedt
1721
{
1822
public:

0 commit comments

Comments
 (0)