RetroSearch Browse

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

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

Z3: ast Class Reference

std::ostream & operator<< (std::ostream &out, ast const &n) bool eq (ast const &a, ast const &b) Return true if the ASTs are structurally identical. More...

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

◆ ast() [1/3]

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

Referenced by FuncDeclRef::__call__(), AstRef::__deepcopy__(), AstRef::__del__(), SortRef::__eq__(), SortRef::__ne__(), DatatypeSortRef::accessor(), FuncDeclRef::arity(), AstRef::as_ast(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), PatternRef::as_ast(), QuantifierRef::as_ast(), FuncDeclRef::as_func_decl(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), DatatypeSortRef::constructor(), ArraySortRef::domain(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FPSortRef::ebits(), QuantifierRef::is_exists(), QuantifierRef::is_forall(), QuantifierRef::is_lambda(), SeqSortRef::is_string(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), DatatypeSortRef::num_constructors(), QuantifierRef::num_no_patterns(), QuantifierRef::num_patterns(), QuantifierRef::num_vars(), FuncDeclRef::params(), QuantifierRef::pattern(), QuantifierRef::qid(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), FPSortRef::sbits(), BitVecSortRef::size(), FiniteDomainSortRef::size(), QuantifierRef::skolem_id(), QuantifierRef::var_name(), QuantifierRef::var_sort(), and QuantifierRef::weight().

◆ ast() [2/3]

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

void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)

Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...

◆ ast() [3/3]

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

◆ ~ast()

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

void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)

Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...

◆ hash()

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

Z3_error_code check_error() const

unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)

Return a hash code for the given AST. The hash code is structural but two different AST objects can m...

Referenced by AstRef::__hash__().

◆ kind() ◆ operator bool() ◆ operator Z3_ast() operator Z3_ast ( ) const inline ◆ operator=() ast& operator= ( ast const & s ) inline

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

565

object::operator=(s);

◆ to_string() std::string to_string ( ) const inline

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

Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)

Convert the given AST node into a string.

◆ eq bool eq ( ast const & a, ast const & b ) friend ◆ operator<< std::ostream& operator<< ( std::ostream & out, ast const & n ) friend ◆ m_ast

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

Referenced by expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), expr::as_binary(), ast::ast(), expr::bool_value(), expr::denominator(), expr::get_decimal_string(), expr::get_sort(), expr::get_string(), expr::get_u32string(), ast::hash(), expr::id(), expr::is_algebraic(), expr::is_exists(), expr::is_forall(), expr::is_lambda(), expr::is_numeral(), expr::is_numeral_i(), expr::is_numeral_i64(), expr::is_numeral_u(), expr::is_numeral_u64(), expr::is_string_value(), expr::is_well_sorted(), ast::kind(), expr::loop(), expr::mk_from_ieee_bv(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), expr::mk_to_ieee_bv(), expr::numerator(), ast::operator bool(), expr::operator Z3_app(), ast::operator Z3_ast(), func_decl::operator Z3_func_decl(), sort::operator Z3_sort(), ast::operator=(), expr::simplify(), expr::substitute(), ast::to_string(), and ast::~ast().

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