digraph "Graphical Class Hierarchy"
{
 // LATEX_PDF_SIZE
  edge [fontname="Helvetica",fontsize="10",labelfontname="Helvetica",labelfontsize="10"];
  node [fontname="Helvetica",fontsize="10",shape=record];
  rankdir="LR";
  Node0 [label="IComparable",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_i_comparable.html",tooltip=" "];
  Node0 -> Node1 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node1 [label="AST",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_a_s_t.html",tooltip="The abstract syntax tree (AST) class."];
  Node1 -> Node2 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node2 [label="Expr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_expr.html",tooltip="Expressions are terms."];
  Node2 -> Node3 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node3 [label="ArithExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_arith_expr.html",tooltip="Arithmetic expressions (int/real)"];
  Node3 -> Node4 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node4 [label="AlgebraicNum",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_algebraic_num.html",tooltip="Algebraic numbers"];
  Node3 -> Node5 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node5 [label="IntExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_int_expr.html",tooltip="Int expressions"];
  Node5 -> Node6 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node6 [label="IntNum",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_int_num.html",tooltip="Integer Numerals"];
  Node3 -> Node7 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node7 [label="RealExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_real_expr.html",tooltip="Real expressions"];
  Node7 -> Node8 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node8 [label="RatNum",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_rat_num.html",tooltip="Rational Numerals"];
  Node2 -> Node9 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node9 [label="ArrayExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_array_expr.html",tooltip="Array expressions"];
  Node9 -> Node10 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node10 [label="Lambda",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_lambda.html",tooltip="Lambda expressions."];
  Node2 -> Node11 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node11 [label="BitVecExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_bit_vec_expr.html",tooltip="Bit-vector expressions"];
  Node11 -> Node12 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node12 [label="BitVecNum",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_bit_vec_num.html",tooltip="Bit-vector numerals"];
  Node2 -> Node13 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node13 [label="BoolExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_bool_expr.html",tooltip="Boolean expressions"];
  Node13 -> Node14 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node14 [label="Quantifier",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_quantifier.html",tooltip="Quantifier expressions."];
  Node2 -> Node15 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node15 [label="DatatypeExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_datatype_expr.html",tooltip="Datatype expressions"];
  Node2 -> Node16 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node16 [label="FPExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_f_p_expr.html",tooltip="FloatingPoint Expressions"];
  Node16 -> Node17 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node17 [label="FPNum",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_f_p_num.html",tooltip="FloatiungPoint Numerals"];
  Node2 -> Node18 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node18 [label="FPRMExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_f_p_r_m_expr.html",tooltip="FloatingPoint RoundingMode Expressions"];
  Node18 -> Node19 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node19 [label="FPRMNum",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_f_p_r_m_num.html",tooltip="Floating-point rounding mode numerals"];
  Node2 -> Node20 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node20 [label="FiniteDomainExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_finite_domain_expr.html",tooltip="Finite-domain expressions"];
  Node20 -> Node21 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node21 [label="FiniteDomainNum",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_finite_domain_num.html",tooltip="Finite-domain numerals"];
  Node2 -> Node22 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node22 [label="ReExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_re_expr.html",tooltip="Regular expression expressions"];
  Node2 -> Node23 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node23 [label="SeqExpr",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_seq_expr.html",tooltip="Sequence expressions"];
  Node1 -> Node24 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node24 [label="FuncDecl",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_func_decl.html",tooltip="Function declarations."];
  Node1 -> Node25 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node25 [label="Pattern",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_pattern.html",tooltip="Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o..."];
  Node1 -> Node26 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node26 [label="Sort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_sort.html",tooltip="The Sort class implements type information for ASTs."];
  Node26 -> Node27 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node27 [label="ArithSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_arith_sort.html",tooltip="An arithmetic sort, i.e., Int or Real."];
  Node27 -> Node28 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node28 [label="IntSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_int_sort.html",tooltip="An Integer sort"];
  Node27 -> Node29 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node29 [label="RealSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_real_sort.html",tooltip="A real sort"];
  Node26 -> Node30 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node30 [label="ArraySort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_array_sort.html",tooltip="Array sorts."];
  Node26 -> Node31 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node31 [label="BitVecSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_bit_vec_sort.html",tooltip="Bit-vector sorts."];
  Node26 -> Node32 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node32 [label="BoolSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_bool_sort.html",tooltip="A Boolean sort."];
  Node26 -> Node33 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node33 [label="DatatypeSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_datatype_sort.html",tooltip="Datatype sorts."];
  Node26 -> Node34 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node34 [label="EnumSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_enum_sort.html",tooltip="Enumeration sorts."];
  Node26 -> Node35 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node35 [label="FPRMSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_f_p_r_m_sort.html",tooltip="The FloatingPoint RoundingMode sort"];
  Node26 -> Node36 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node36 [label="FPSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_f_p_sort.html",tooltip="FloatingPoint sort"];
  Node26 -> Node37 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node37 [label="FiniteDomainSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_finite_domain_sort.html",tooltip="Finite domain sorts."];
  Node26 -> Node38 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node38 [label="ListSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_list_sort.html",tooltip="List sorts."];
  Node26 -> Node39 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node39 [label="ReSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_re_sort.html",tooltip="A regular expression sort"];
  Node26 -> Node40 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node40 [label="RelationSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_relation_sort.html",tooltip="Relation sorts."];
  Node26 -> Node41 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node41 [label="SeqSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_seq_sort.html",tooltip="A Sequence sort"];
  Node26 -> Node42 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node42 [label="SetSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_set_sort.html",tooltip="Set sorts."];
  Node26 -> Node43 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node43 [label="TupleSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_tuple_sort.html",tooltip="Tuple sorts."];
  Node26 -> Node44 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node44 [label="UninterpretedSort",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_uninterpreted_sort.html",tooltip="Uninterpreted Sorts"];
  Node65 [label="IDisposable",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_i_disposable.html",tooltip=" "];
  Node65 -> Node66 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node66 [label="Context",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_context.html",tooltip="The main interaction with Z3 happens via the Context."];
  Node65 -> Node45 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node45 [label="Z3Object",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_z3_object.html",tooltip="Internal base class for interfacing with native Z3 objects. Should not be used externally."];
  Node45 -> Node1 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node45 -> Node46 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node46 [label="ASTVector",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_a_s_t_vector.html",tooltip="Vectors of ASTs."];
  Node45 -> Node47 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node47 [label="ApplyResult",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_apply_result.html",tooltip="ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub..."];
  Node45 -> Node48 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node48 [label="Constructor",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_constructor.html",tooltip="Constructors are used for datatype sorts."];
  Node45 -> Node49 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node49 [label="ConstructorList",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_constructor_list.html",tooltip="Lists of constructors"];
  Node45 -> Node50 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node50 [label="Fixedpoint",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_fixedpoint.html",tooltip="Object for managing fixedpoints"];
  Node45 -> Node51 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node51 [label="FuncInterp",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_func_interp.html",tooltip="A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit..."];
  Node45 -> Node52 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node52 [label="FuncInterp.Entry",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_func_interp_1_1_entry.html",tooltip="An Entry object represents an element in the finite map used to encode a function interpretation."];
  Node45 -> Node53 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node53 [label="Goal",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_goal.html",tooltip="A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ..."];
  Node45 -> Node54 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node54 [label="Model",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_model.html",tooltip="A Model contains interpretations (assignments) of constants and functions."];
  Node45 -> Node55 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node55 [label="Optimize",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_optimize.html",tooltip="Object for managing optimization context"];
  Node45 -> Node56 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node56 [label="ParamDescrs",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_param_descrs.html",tooltip="A ParamDescrs describes a set of parameters."];
  Node45 -> Node57 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node57 [label="Params",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_params.html",tooltip="A Params objects represents a configuration in the form of Symbol/value pairs."];
  Node45 -> Node58 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node58 [label="Probe",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_probe.html",tooltip="Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh..."];
  Node45 -> Node59 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node59 [label="Solver",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_solver.html",tooltip="Solvers."];
  Node45 -> Node60 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node60 [label="Statistics",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_statistics.html",tooltip="Objects of this class track statistical information about solvers."];
  Node45 -> Node61 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node61 [label="Symbol",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_symbol.html",tooltip="Symbols are used to name several term and type constructors."];
  Node61 -> Node62 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node62 [label="IntSymbol",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_int_symbol.html",tooltip="Numbered symbols"];
  Node61 -> Node63 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node63 [label="StringSymbol",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_string_symbol.html",tooltip="Named symbols"];
  Node45 -> Node64 [dir="back",color="midnightblue",fontsize="10",style="solid",fontname="Helvetica"];
  Node64 [label="Tactic",height=0.2,width=0.4,color="black", fillcolor="white", style="filled",URL="$class_microsoft_1_1_z3_1_1_tactic.html",tooltip="Tactics are the basic building block for creating custom solvers for specific problem domains...."];
}
