Context class

Constructors

Context(Config _originalConfig)

Properties

boolSort → BoolSort

late, final

builtinProbes → Map<String, BuiltinProbe>

late, final

builtinTactics → Map<String, BuiltinTactic>

late, final

charSort → CharSort

late, final

config → ContextConfig

late, final

falseExpr → Expr

late, final

fpaRna → Expr

late, final

fpaRne → Expr

late, final

fpaRoundingModeSort → FpaRoundingModeSort

late, final

fpaRoundNearestTiesToAway → Expr

late, final

fpaRoundNearestTiesToEven → Expr

late, final

fpaRoundTowardNegative → Expr

late, final

fpaRoundTowardPositive → Expr

late, final

fpaRoundTowardZero → Expr

late, final

fpaRtn → Expr

late, final

fpaRtp → Expr

late, final

fpaRtz → Expr

late, final

hashCode → int

The hash code for this object.

no setter, inherited

intSort → IntSort

late, final

paramDesc → ParamDescs

late, final

realSort → RealSort

late, final

runtimeType → Type

A representation of the runtime type of the object.

no setter, inherited

simplifyParamDescriptions → ParamDescs

no setter

stringSort → StringSort

late, final

trueExpr → Expr

late, final

Methods

astToString(AST ast) → String

benchmarkToSmtlib({required String name, required String logic, required String status, required String attributes, required List<AST> assumptions, required AST formula}) → String

declare<T extends AST>(T ast) → T

declareDatatype(Sym name, List<Constructor> constructors) → DatatypeInfo

declareDatatypes(Map<Sym, List<Constructor>> datatypes) → Map<Sym, DatatypeInfo>

declareEnum(Sym name, List<Sym> elements) → EnumInfo

declareList(Sym name, Sort element) → ListInfo

declareTuple(Sym name, Map<Sym, Sort> fields) → TupleInfo

defineRecursiveFunc(RecursiveFunc decl, AST body, [List<Expr> args = const []]) → void

emptyParams() → Params

eval(String str) → String

funcDeclsEqual(FuncDecl a, FuncDecl b) → bool

getDatatypeInfo(DatatypeSort sort) → DatatypeInfo

getExprApp(Expr app) → App?

getSort(Expr value) → Sort

getSortId(Sort sort) → int

getSortName(Sort sort) → Sym

lambdaConst(List<ConstVar> args, Expr body) → Lambda

noSuchMethod(Invocation invocation) → dynamic

Invoked when a nonexistent method or property is accessed.

inherited

optimize() → Optimize

parse(String str, {Map<Sym, Sort> sorts = const {}, Map<Sym, FuncDecl> decls = const {}}) → List<AST>

parser() → ParserContext

pbGe(Map<Expr, int> args, int k) → Expr

pbLe(Map<Expr, int> args, int k) → Expr

probe(double value) → Probe

setASTPrintMode(ASTPrintMode mode) → void

simpleSolver() → Solver

simplify(AST ast, [Params? params]) → AST

solver({LogicKind? logic}) → Solver

sortsEqual(Sort a, Sort b) → bool

substitute(AST ast, List<AST> from, List<AST> to) → AST

substituteFuncs(AST ast, List<FuncDecl> from, List<AST> to) → AST

substituteVars(AST ast, List<AST> to) → AST

toString() → String

A string representation of this object.

inherited

translateTo<A extends AST>(Context other, A ast) → A

updateTerm(AST ast, List<AST> args) → AST

Operators

operator ==(Object other) → bool

The equality operator.

inherited