bv_refinementt::infot Struct Reference

#include <bv_refinement.h>

Inheritance diagram for bv_refinementt::infot:

Collaboration diagram for bv_refinementt::infot:

Public Attributes
const namespacet *	ns =nullptr
propt *	prop =nullptr
Public Attributes inherited from bv_refinementt::configt
ui_message_handlert::uit	ui =ui_message_handlert::uit::PLAIN
unsigned	max_node_refinement =5
	Max number of times we refine a formula node. More...
bool	refine_arrays =true
	Enable array refinement. More...
bool	refine_arithmetic =true
	Enable arithmetic refinement. More...

Detailed Description

Definition at line 35 of file bv_refinement.h.

Member Data Documentation

ns

const namespacet* bv_refinementt::infot::ns =nullptr

Definition at line 37 of file bv_refinement.h.

Referenced by cbmc_solverst::get_bv_refinement(), cbmc_solverst::get_string_refinement(), and validate().

prop

propt* bv_refinementt::infot::prop =nullptr

Definition at line 38 of file bv_refinement.h.

Referenced by cbmc_solverst::get_bv_refinement(), cbmc_solverst::get_string_refinement(), and validate().

---

The documentation for this struct was generated from the following file:

• solvers/refinement/bv_refinement.h