RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3_1_1array.html below:

Z3: array< T > Class Template Reference

Detailed Description template<typename T>
class z3::array< T >

Definition at line 451 of file z3++.h.

Constructor & Destructor Documentation ◆ array() [1/2]

Definition at line 457 of file z3++.h.

457

:m_array(

new

T[sz]),m_size(sz) {}

◆ array() [2/2]

Definition at line 2317 of file z3++.h.

2317

:m_array(

new

T[v.size()]), m_size(v.size()) {

2318 for

(

unsigned

i = 0; i < m_size; i++) {

Member Function Documentation ◆ operator[]() [1/2]

Definition at line 462 of file z3++.h.

462

{ assert(0 <= i); assert(

static_cast<unsigned>

(i) < m_size);

return

m_array[i]; }

◆ operator[]() [2/2] T const& operator[] ( int i ) const inline

Definition at line 463 of file z3++.h.

463

{ assert(0 <= i); assert(

static_cast<unsigned>

(i) < m_size);

return

m_array[i]; }

◆ ptr() [1/2]

Definition at line 465 of file z3++.h.

465

{

return

m_array.get(); }

◆ ptr() [2/2]

Definition at line 464 of file z3++.h.

464

{

return

m_array.get(); }

Referenced by constructors::add(), context::array_sort(), goal::as_expr(), context::bv_val(), optimize::check(), solver::check(), user_propagator_base::conflict(), constructor_list::constructor_list(), context::datatype(), context::datatypes(), context::enumeration_sort(), z3::exists(), z3::forall(), context::function(), z3::lambda(), func_decl::operator()(), context::parse_file(), context::parse_string(), user_propagator_base::propagate(), fixedpoint::query(), constructors::query(), z3::re_intersect(), context::recdef(), context::recfun(), z3::select(), z3::store(), expr::substitute(), solver::to_smt2(), fixedpoint::to_string(), solver::trail(), context::tuple_sort(), and context::user_propagate_function().

◆ resize() void resize ( unsigned sz ) inline ◆ size()

Definition at line 461 of file z3++.h.

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), context::array_sort(), BitVecNumRef::as_signed_long(), z3::exists(), z3::forall(), z3::lambda(), user_propagator_base::propagate(), fixedpoint::query(), z3::re_intersect(), context::recdef(), context::recfun(), z3::select(), z3::store(), BitVecSortRef::subsort(), solver::to_smt2(), fixedpoint::to_string(), and context::user_propagate_function().

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4