Context class - z3 library

Constructors

Context(Config _originalConfig): Creates a new context.

Properties

boolSort → BoolSort: The type of booleans.
latefinal
builtinProbes → Map<String, BuiltinProbe>: A map of all of the built in probes.
latefinal
builtinTactics → Map<String, BuiltinTactic>: A map of all of the built in tactics.
latefinal
charSort → CharSort: The type of characters.
latefinal
config → ContextConfig: The configuration for this context that can be modified after creation.
latefinal
falseExpr → Expr: The false expression.
latefinal
fpaRna → Expr: The rounding mode to round to nearest ties to away.
latefinal
fpaRne → Expr: The rounding mode to round to nearest ties to even.
latefinal
fpaRoundingModeSort → FpaRoundingModeSort: The type of a floating point rounding mode enum.
latefinal
fpaRoundNearestTiesToAway → Expr: The rounding mode to round to nearest ties to away, alias for fpaRna.
latefinal
fpaRoundNearestTiesToEven → Expr: The rounding mode to round to nearest ties to even, alias for fpaRne.
latefinal
fpaRoundTowardNegative → Expr: The rounding mode to round toward negative, alias for fpaRtn.
latefinal
fpaRoundTowardPositive → Expr: The rounding mode to round toward positive, alias for fpaRtp.
latefinal
fpaRoundTowardZero → Expr: The rounding mode to round toward zero, alias for fpaRtz.
latefinal
fpaRtn → Expr: The rounding mode to round toward negative.
latefinal
fpaRtp → Expr: The rounding mode to round toward positive.
latefinal
fpaRtz → Expr: The rounding mode to round toward zero.
latefinal
hashCode → int: The hash code for this object.
no setterinherited
intSort → IntSort: The type of integers.
latefinal
paramDesc → ParamDescs: Parameter descriptions for config.
latefinal
realSort → RealSort: The type of real numbers (integers, floats, rationals, irrationals).
latefinal
runtimeType → Type: A representation of the runtime type of the object.
no setterinherited
simplifyParamDescriptions → ParamDescs: Gets a description of all of the available parameters to the simplify function.
no setter
stringSort → StringSort: The type of strings.
latefinal
trueExpr → Expr: The true expression.
latefinal

Methods

astToString(AST ast) → String: Prints an AST to a string.
benchmarkToSmtlib({required String name, required String logic, required String status, required String attributes, required List<AST> assumptions, required AST formula}) → String: Convert the given benchmark into a SMT-LIB string.
declare<T extends AST>(T ast) → T: Declare an AST element in the current context, for most AST elements this is not necessary as they are automatically declared when constructed.
declareDatatype(Sym name, List<Constructor> constructors) → DatatypeInfo: Declare a datatype with the given name and constructors.
declareDatatypes(Map<Sym, List<Constructor>> datatypes) → Map<Sym, DatatypeInfo>: Declare mutually recursive datatypes given a map from their name to their constructors.
declareEnum(Sym name, List<Sym> elements) → EnumInfo: Declares an enum with the given name and elements.
declareList(Sym name, Sort element) → ListInfo: Declares a list with the given name and element type.
declareTuple(Sym name, Map<Sym, Sort> fields) → TupleInfo: Declares a tuple with the given name and fields.
defineRecursiveFunc(RecursiveFunc decl, AST body, [List<Expr> args = const []]) → void: Define the body of a recursive function declared using RecursiveFunc.
emptyParams() → Params: Create an empty params object.
eval(String str) → String: Evaluate an SMT-LIB string, returning the result as a string.
funcDeclsEqual(FuncDecl a, FuncDecl b) → bool: Check if two FuncDecls are equal.
getDatatypeInfo(DatatypeSort sort) → DatatypeInfo: Gets the DatatypeInfo for the given sort.
getExprApp(Expr app) → App?: Get the App representing an expression, this gives you access to the underlying FuncDecl and parameters.
getSort(Expr value) → Sort: Get the sort of an Expr.
getSortId(Sort sort) → int: Get a unique id of a Sort.
getSortName(Sort sort) → Sym: Get the name of a Sort.
lambdaConst(List<ConstVar> args, Expr body) → Lambda: Creates a Lambda quantifier.
noSuchMethod(Invocation invocation) → dynamic: Invoked when a nonexistent method or property is accessed.
inherited
optimize() → Optimize: Create an optimization context.
parse(String str, {Map<Sym, Sort> sorts = const {}, Map<Sym, FuncDecl> decls = const {}}) → List<AST>: Parse a SMT-LIB string, returning all of its assertions.
parser() → ParserContext: Create a context for parsing and evaluating SMT-LIB strings.
pbGe(Map<Expr, int> args, int k) → Expr: Create the pseudo-boolean relation p1 + p2 + ... + pn >= k.
pbLe(Map<Expr, int> args, int k) → Expr: Create the pseudo-boolean relation p1 + p2 + ... + pn <= k.
probe(double value) → Probe: Create a constant probe that always evaluates to value.
setASTPrintMode(ASTPrintMode mode) → void: Sets the ASTPrintMode of the current context used in astToString and some other places.
simpleSolver() → Solver: Create a simple incremental solver.
simplify<A extends Expr>(Expr expr, [Params? params]) → A: Simplifies an expression using basic algebraic rules and constant folding.
solver({LogicKind? logic}) → Solver: Creates a solver.
sortsEqual(Sort a, Sort b) → bool: Check if two Sorts are equal.
substitute<A extends Expr>(A ast, Map<Expr, Expr> substitutions) → A: Substitutes expressions in expr where the keys of substitutions are replaced with their corresponding values.
substituteFuncs<A extends Expr>(Expr expr, Map<FuncDecl, Expr> substitutions) → A: Substitute the arguments to FuncDecls in expr with the expressions in to.
substituteVars<A extends Expr>(Expr expr, List<Expr> to) → A: Substitute BoundVars in expr with the expressions in to.
toString() → String: A string representation of this object.
inherited
translateTo<A extends AST>(Context other, A ast) → A: Translate the given AST element to another context.
updateTerm<A extends Expr>(A expr, List<Expr> args) → A: Updates the arguments of an App, Lambda, Exists, or Forall.

Operators

operator ==(Object other) → bool: The equality operator.
inherited