bv_utils.cpp File Reference

#include "bv_utils.h"
#include <util/arith_tools.h>
#include <list>
#include <utility>

Include dependency graph for bv_utils.cpp:

Go to the source code of this file.

Macros
#define	OPTIMAL_FULL_ADDER
	Generates the encoding of a full adder.
#define	COMPACT_CARRY
#define	COMPACT_LT_OR_LE
	To provide a bitwise model of < or <=.

Macro Definition Documentation

COMPACT_CARRY

#define COMPACT_CARRY

Definition at line 230 of file bv_utils.cpp.

COMPACT_LT_OR_LE

#define COMPACT_LT_OR_LE

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 1399 of file bv_utils.cpp.

OPTIMAL_FULL_ADDER

#define OPTIMAL_FULL_ADDER

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 139 of file bv_utils.cpp.