refine_arithmetic.cpp File Reference

#include "bv_refinement.h"
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/bv_arithmetic.h>
#include <util/expr_util.h>
#include <util/floatbv_expr.h>
#include <util/ieee_float.h>
#include <solvers/floatbv/float_utils.h>
#include <solvers/prop/literal_expr.h>

Include dependency graph for refine_arithmetic.cpp:

Go to the source code of this file.

Macros
#define	MAX_INTEGER_UNDERAPPROX   3
#define	MAX_FLOAT_UNDERAPPROX   10

Macro Definition Documentation

MAX_FLOAT_UNDERAPPROX

#define MAX_FLOAT_UNDERAPPROX   10

Definition at line 23 of file refine_arithmetic.cpp.

MAX_INTEGER_UNDERAPPROX

#define MAX_INTEGER_UNDERAPPROX   3

Definition at line 22 of file refine_arithmetic.cpp.