Fixedpoint class
Properties
-
hashCode
→ int
-
The hash code for this object.
no setterinherited
-
runtimeType
→ Type
-
A representation of the runtime type of the object.
no setterinherited
Methods
-
addConstraint(AST axiom, int level)
→ void
-
-
addCover(int level, FuncDecl pred, AST property)
→ void
-
-
addFact(FuncDecl relation, List<int> args)
→ void
-
-
addRule(AST rule, Z3_symbol name)
→ void
-
-
addSmtlib(String s)
→ List<AST>
-
-
addSmtlibFile(File file)
→ List<AST>
-
-
assertConstraint(AST axiom)
→ void
-
-
getAnswer()
→ AST
-
-
getAssertions()
→ List<Expr>
-
-
getCoverDelta(int level, FuncDecl pred)
→ void
-
-
getHelp()
→ String
-
-
getNumLevels(FuncDecl pred)
→ void
-
-
getParamDescriptions()
→ ParamDescs
-
-
getReasonUnknown()
→ String
-
-
getRules()
→ List<Expr>
-
-
getStatistics()
→ Stats
-
-
noSuchMethod(Invocation invocation)
→ dynamic
-
Invoked when a nonexistent method or property is accessed.
inherited
-
query(AST query)
→ bool
-
-
queryRelations(List<FuncDecl> relations)
→ bool
-
-
registerRelation(FuncDecl relation)
→ void
-
-
setOnLemma(void f(AST, int level)?)
→ void
-
-
setOnPredecessor(void f()?)
→ void
-
-
setOnReduceApply(AST? f(FuncDecl func, List<AST> args)?)
→ void
-
-
setOnReduceAssign(List<AST> f(List<AST> args, List<AST> outs)?)
→ void
-
-
setOnUnfold(void f()?)
→ void
-
-
setParams(Params params)
→ void
-
-
setPredicateRepresentation(FuncDecl relation, List<Sym> kinds)
→ void
-
-
toString([])
→ String
-
A string representation of this object.
override
-
updateRule(AST rule, Z3_symbol name)
→ void
-
