Context class
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
-