bv_utils.cpp File Reference

+ Include dependency graph for bv_utils.cpp:

Definition at line 240 of file bv_utils.cpp.

To provide a bitwise model of < or <=.

parameters: bvts for each input and whether they are signed and whether

a model of < or <= is required.

Returns

A literalt that models the value of the comparison.

Definition at line 1426 of file bv_utils.cpp.

Generates the encoding of a full adder.

The optimal encoding is the default.

parameters: a, b, carry_in are the literals representing inputs

Returns

return value is the literal for the sum, carry_out gets the output carry

Definition at line 149 of file bv_utils.cpp.