Types & classes — github.com/Z3Prover/z3

CodeHub MCPcopy Create free account

hub / github.com/Z3Prover/z3 / types & classes

Types & classes5,965 in github.com/Z3Prover/z3

⨍ Functions 43,174◇ Types & classes 5,965

↓ 2,035 callersClassmk_pp

src/ast/ast_pp.h:25

↓ 1,927 callersClassrational

src/util/rational.h:23

↓ 728 callersClassctx

src/nlsat/nlsat_solver.h:51

↓ 612 callersClassmk_ismt2_pp

\brief Internal wrapper (for debugging purposes only) */

src/ast/ast_smt2_pp.h:116

↓ 595 callersClassstr

src/ast/seq_decl_plugin.h:279

↓ 554 callersClasssymbol

src/util/symbol.h:31

↓ 451 callersClassmk_bounded_pp

src/ast/ast_ll_pp.h:42

↓ 382 callersClassliteral

\brief The literal b is represented by the value 2*b, and the literal (not b) by the value 2*b + 1 */

src/util/sat_literal.h:39

↓ 328 callersClassdefault_exception

src/util/z3_exception.h:39

↓ 325 callersClassmpq

src/util/mpq.h:24

↓ 272 callersClasssymbol

src/api/c++/z3++.h:55

↓ 259 callersClassbuiltin_name

\brief Auxiliary data-structure used to initialize the parser symbol tables. */

src/ast/ast.h:1012

↓ 238 callersClassexpr

src/api/c++/z3++.h:63

↓ 202 callersClasssize

src/ast/datatype_decl_plugin.h:123

↓ 177 callersClassvalue

src/ast/sls/sls_seq_plugin.h:28

↓ 172 callersClassparams_ref

src/util/params.h:32

↓ 165 callersClasssort

src/ast/ast.h:620

↓ 155 callersClasscmd_exception

src/util/cmd_context_types.h:47

↓ 153 callersClassineq

src/math/lp/nla_types.h:34

↓ 139 callersClassparameter

\brief Interpreted function declarations and sorts may have parameters that are used to encode extra information associated with them. */

src/ast/ast.h:102

↓ 128 callersClassfunc_decl_info

\brief Extra information that may be attached to interpreted function decls. */

src/ast/ast.h:397

↓ 127 callersClassmonomial

src/math/polynomial/polynomial.h:45

↓ 123 callersClasscheck

src/smt/mam.cpp:146

↓ 116 callersClassmpz

src/util/mpz.h:81

↓ 105 callersClassvisit

src/solver/slice_solver.cpp:47

↓ 96 callersClasstactic_exception

src/tactic/tactic_exception.h:24

↓ 86 callersClassvar

src/math/simplex/model_based_opt.h:44

↓ 84 callersClassis_relevant

↓ 77 callersClassfm

src/qe/lite/qe_lite_tactic.cpp:992

↓ 73 callersClassinf_rational

src/util/inf_rational.h:29

↓ 67 callersClassmk_ll_pp

src/ast/ast_ll_pp.h:29

↓ 63 callersClasszstring

src/util/zstring.h:30

↓ 62 callersClassplugin

src/ast/euf/euf_plugin.h:29

↓ 60 callersClassMKException

scripts/mk_exception.py:7

↓ 58 callersClassdependent_expr

src/ast/simplifiers/dependent_expr.h:24

↓ 56 callersClassZ3Exception

src/api/python/z3/z3types.py:12

↓ 54 callersClassext_numeral

src/smt/old_interval.h:24

↓ 51 callersClassrw

src/tactic/arith/factor_tactic.cpp:236

↓ 50 callersClassenode_pp

src/smt/smt_context.h:71

↓ 48 callersInterfaceRCFNum

src/api/js/src/high-level/types.ts:2109

↓ 48 callersClassexpr_offset

src/ast/substitution/expr_offset.h:28

↓ 47 callersClassBoolRef

All Boolean expressions are instances of this class.

src/api/python/z3/z3.py:1654

↓ 45 callersClasslit

src/sat/smt/q_clause.h:28

↓ 45 callersClassterm

namespace is_ground_ns

src/qe/mbp/mbp_term_graph.h:39

↓ 44 callersClassadd_def

src/ast/sls/sls_arith_base.h:185

↓ 44 callersClassparams

src/util/params.h:29

↓ 41 callersClassBitVecRef

Bit-vector expressions.

src/api/python/z3/z3.py:3649

↓ 41 callersClassenode_class

src/ast/euf/euf_enode.h:272

↓ 40 callersClassfunc_decl

src/api/c++/z3++.h:62

↓ 39 callersClassapply

src/smt/theory_seq.h:223

↓ 39 callersClassenode_parents

src/ast/euf/euf_enode.h:263

↓ 39 callersClassf2f

src/ast/format.h:43

↓ 39 callersClasssymbol

src/cmd_context/cmd_util.h:62

↓ 36 callersClassallocator

src/util/dependency.h:277

↓ 36 callersClassindices

src/qe/mbp/mbp_arrays.cpp:1043

↓ 36 callersEnumupdate

src/sat/smt/euf_relevancy.h:118

↓ 35 callersClasseval

src/qe/nlarith_util.h:117

↓ 35 callersClasspush_back_vector

src/util/trail.h:210

↓ 35 callersClassvalue_trail

src/util/trail.h:34

↓ 34 callersClassAstVector

A collection (vector) of ASTs.

src/api/python/z3/z3.py:6086

↓ 34 callersClasstactic

src/api/c++/z3++.h:66

↓ 32 callersClasschecker

src/math/hilbert/hilbert_basis.cpp:174

↓ 31 callersClassexpr2var

\brief The mapping between Z3 expressions and (low level) variables. */

src/ast/expr2var.h:31

↓ 31 callersClassinterval

src/math/realclosure/realclosure.cpp:81

↓ 30 callersClassArithRef

Integer and Real expressions.

src/api/python/z3/z3.py:2523

↓ 30 callersClassoverflow_exception

src/util/checked_int64.h:31

↓ 29 callersClassbool_rewriter

\brief Apply basic Boolean rewriting operations. Only depth 1 simplifications are performed. Note: there are no recursive calls. Note: ar

src/ast/rewriter/bool_rewriter.h:51

↓ 29 callersClassmpbq

src/math/polynomial/algebraic_numbers.h:34

↓ 29 callersClasssigned_var

src/math/lp/nla_defs.h:22

↓ 29 callersClassui64

src/util/rational.h:68

↓ 28 callersClassenode_args

src/ast/euf/euf_enode.h:254

↓ 28 callersClassfind

find an `app` that is an application of a defined function

src/ast/recfun_decl_plugin.cpp:387

↓ 27 callersClasss_integer

src/util/s_integer.h:23

↓ 26 callersClasssort

src/api/c++/z3++.h:59

↓ 25 callersClassdependent_eq

src/ast/simplifiers/extract_eqs.h:30

↓ 25 callersClasspdd

src/math/dd/dd_pdd.h:45

↓ 24 callersClassb_justification

\brief Proof like object used to track dependencies of boolean propagation. The idea is to reduce the cost of dependency tracking for the most

src/smt/smt_b_justification.h:31

↓ 24 callersClassescaped

src/util/util.h:436

↓ 24 callersClassmark

src/util/region.h:61

↓ 23 callersStructSolver

Solver represents a Z3 solver.

src/api/go/solver.go:40

↓ 23 callersClasscache

\brief Functor for creating unique polynomials and caching results of operations */

src/math/polynomial/polynomial_cache.h:28

↓ 23 callersClasseq

src/util/tbv.h:97

↓ 23 callersClasseval

src/sat/smt/q_eval.h:28

↓ 23 callersClassvar

src/ast/ast.h:836

↓ 22 callersClassFuncDeclRef

Function declaration. Every constant and function have an associated declaration. The declaration assigns a name, a sort (i.e., type), and for fu

src/api/python/z3/z3.py:775

↓ 22 callersClassfmt

src/util/z3_exception.h:42

↓ 22 callersClasssort_info

\brief Extra information that may be attached to interpreted sorts. */

src/ast/ast.h:359

↓ 22 callersClasstrail

src/util/trail.h:27

↓ 22 callersClassundef_var_assignment

\brief Wrapper for temporarily unassigning a given variable y. That is, given an assignment M, M' = undef_var_assignment(M, y) is identical

src/nlsat/nlsat_assignment.h:91

↓ 21 callersClasscollect

src/ast/pattern/pattern_inference.h:113

↓ 21 callersClasseq

src/tactic/core/symmetry_reduce_tactic.cpp:213

↓ 21 callersClassi64

src/util/rational.h:65

↓ 20 callersClassaig_lit

src/tactic/aig/aig.cpp:29

↓ 20 callersClassvc

src/util/sorting_network.h:153

↓ 19 callersClassFPRef

Floating-point expressions.

src/api/python/z3/z3.py:9883

↓ 19 callersClassfound

src/tactic/probe.cpp:506

↓ 19 callersClassfound

src/tactic/arith/probe_arith.cpp:133

↓ 19 callersClasslist

src/util/list.h:25

↓ 18 callersClassarith_util

src/ast/arith_decl_plugin.h:88

↓ 18 callersClasseq_pp_ll

src/ast/euf/euf_ac_plugin.h:327

next →1–100 of 5,965, ranked by callers