Index

A

accepts() (aria.automata.symautomata.sfa.SFA method) add_arc() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) add_state() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) aria.automata.aalpy.automata module aria.automata.symautomata.alphabet module aria.automata.symautomata.cfggenerator module aria.automata.symautomata.cfgpda module aria.automata.symautomata.dfa module aria.automata.symautomata.pda module aria.automata.symautomata.pdastring module aria.automata.symautomata.pythondfa module aria.automata.symautomata.regex module aria.automata.symautomata.sfa module aria.efmc.llmtools.llm_local module aria.efmc.llmtools.llm_tool module aria.efmc.llmtools.llm_utils module aria.efmc.llmtools.logger module aria.efmc.verifytools.boogie.ast module aria.efmc.verifytools.common.ast module aria.efmc.verifytools.common.parser module aria.efmc.verifytools.common.util module aria.efmc.verifytools.daikon.inv_ast module aria.efmc.verifytools.daikon.inv_grammar module aria.efmc.verifytools.tools.vc_check module

ast_and() (in module aria.efmc.verifytools.boogie.ast) ast_boolean_exprs() (in module aria.efmc.verifytools.boogie.ast) ast_constants() (in module aria.efmc.verifytools.boogie.ast) ast_group_bin() (in module aria.efmc.verifytools.boogie.ast) ast_or() (in module aria.efmc.verifytools.boogie.ast) ast_primitive_boolean_exprs() (in module aria.efmc.verifytools.boogie.ast) AstAssert (class in aria.efmc.verifytools.boogie.ast) AstAssignment (class in aria.efmc.verifytools.boogie.ast) AstAssume (class in aria.efmc.verifytools.boogie.ast) AstBinding (class in aria.efmc.verifytools.boogie.ast) AstBinExpr (class in aria.efmc.verifytools.boogie.ast) (class in aria.efmc.verifytools.daikon.inv_ast) AstBlock (class in aria.efmc.verifytools.boogie.ast) AstBody (class in aria.efmc.verifytools.boogie.ast) AstBuilder (class in aria.efmc.verifytools.boogie.ast) (class in aria.efmc.verifytools.daikon.inv_ast) AstFalse (class in aria.efmc.verifytools.boogie.ast) (class in aria.efmc.verifytools.daikon.inv_ast) AstFuncExpr (class in aria.efmc.verifytools.boogie.ast) AstGoto (class in aria.efmc.verifytools.boogie.ast) AstHasValues (class in aria.efmc.verifytools.daikon.inv_ast) AstHavoc (class in aria.efmc.verifytools.boogie.ast) AstId (class in aria.efmc.verifytools.boogie.ast) (class in aria.efmc.verifytools.daikon.inv_ast) AstImplementation (class in aria.efmc.verifytools.boogie.ast) AstInRange (class in aria.efmc.verifytools.daikon.inv_ast) AstIntType (class in aria.efmc.verifytools.boogie.ast) AstIsBoolean (class in aria.efmc.verifytools.daikon.inv_ast) AstIsConstMod (class in aria.efmc.verifytools.daikon.inv_ast) AstIsEven (class in aria.efmc.verifytools.daikon.inv_ast) AstIsOneOf (class in aria.efmc.verifytools.daikon.inv_ast) AstIsPow2 (class in aria.efmc.verifytools.daikon.inv_ast) AstLabel (class in aria.efmc.verifytools.boogie.ast) AstNode (class in aria.efmc.verifytools.common.ast) AstNumber (class in aria.efmc.verifytools.boogie.ast) (class in aria.efmc.verifytools.daikon.inv_ast) AstOneExprStmt (class in aria.efmc.verifytools.boogie.ast) AstProgram (class in aria.efmc.verifytools.boogie.ast) AstReturn (class in aria.efmc.verifytools.boogie.ast) AstStmt (class in aria.efmc.verifytools.boogie.ast) AstTrue (class in aria.efmc.verifytools.boogie.ast) (class in aria.efmc.verifytools.daikon.inv_ast) AstUnExpr (class in aria.efmc.verifytools.boogie.ast) (class in aria.efmc.verifytools.daikon.inv_ast) AstWhile (class in aria.efmc.verifytools.boogie.ast) average() (in module aria.efmc.verifytools.common.util)

B

bfs() (in module aria.automata.symautomata.dfa) bfs_queue (aria.automata.symautomata.cfggenerator.CFGGenerator attribute)

bitvec() (aria.automata.symautomata.sfa.Z3Predicate class method) built-in function execute()

C

CFGGenerator (class in aria.automata.symautomata.cfggenerator) CfgPDA (class in aria.automata.symautomata.cfgpda) checkIfBothAreNeeded() (aria.automata.symautomata.regex.Regex method) checkIfSameStateNotNeeded() (aria.automata.symautomata.regex.Regex method) cleaner() (aria.automata.symautomata.regex.Regex method) cleanerS() (aria.automata.symautomata.regex.Regex method) CNFGenerator (class in aria.automata.symautomata.cfggenerator) complement() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) complete() (aria.automata.symautomata.sfa.SFA method)

concretize() (aria.automata.symautomata.sfa.SFA method) conjunction() (aria.automata.symautomata.sfa.Predicate method) (aria.automata.symautomata.sfa.SetPredicate method) (aria.automata.symautomata.sfa.Z3Predicate method) conservative_tautology() (in module aria.efmc.verifytools.tools.vc_check) consume_input() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) copy() (aria.automata.symautomata.sfa.SFA method) createalphabet() (in module aria.automata.symautomata.alphabet) cross_product() (aria.automata.symautomata.pythondfa.PythonDFA method)

D

DaikonInvParser (class in aria.efmc.verifytools.daikon.inv_grammar) define() (aria.automata.symautomata.pythondfa.PythonDFA method) determinize() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) DFAArc (class in aria.automata.symautomata.pythondfa) DFAState (class in aria.automata.symautomata.pythondfa)

diff() (aria.automata.symautomata.pda.PDA method) difference() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) disjunction() (aria.automata.symautomata.sfa.Predicate method) (aria.automata.symautomata.sfa.SetPredicate method) (aria.automata.symautomata.sfa.Z3Predicate method)

E

empty() (aria.automata.symautomata.pythondfa.PythonDFA method) error() (in module aria.efmc.verifytools.common.util) execute() built-in function

existsPath() (aria.automata.symautomata.regex.Regex method) expr_read() (in module aria.efmc.verifytools.boogie.ast)

F

fatal() (in module aria.efmc.verifytools.common.util) find() (aria.automata.symautomata.pythondfa.Syms method) findWhichSymbolsFromOtherStatesConnectToMe() (aria.automata.symautomata.regex.Regex method) fixBrzozowskiAdvanced() (aria.automata.symautomata.regex.Regex method)

fixBrzozowskiBackwardLoopRemoval() (aria.automata.symautomata.regex.Regex method) fixminimized() (aria.automata.symautomata.pythondfa.PythonDFA method) flattenList() (in module aria.efmc.verifytools.common.util) flattenSet() (in module aria.efmc.verifytools.common.util) from_acceptor() (aria.automata.symautomata.sfa.SFA class method)

G

generalizeConstTraceVars() (in module aria.efmc.verifytools.tools.vc_check) generate() (aria.automata.symautomata.cfggenerator.CFGGenerator method) get_regex() (aria.automata.symautomata.regex.Regex method) get_witness() (aria.automata.symautomata.sfa.Predicate method) (aria.automata.symautomata.sfa.SetPredicate method) (aria.automata.symautomata.sfa.SFA method) (aria.automata.symautomata.sfa.Z3Predicate method)

getMaxInternalPath() (aria.automata.symautomata.regex.Regex method) grammar (aria.automata.symautomata.cfggenerator.CFGGenerator attribute)

H

hopcroft() (aria.automata.symautomata.pythondfa.PythonDFA method)

I

infer() (aria.efmc.llmtools.llm_local.LLMLocal method) (aria.efmc.llmtools.llm_utils.LLM method) infer_with_deepseek_model() (aria.efmc.llmtools.llm_utils.LLM method) infer_with_glm_model() (aria.efmc.llmtools.llm_utils.LLM method) infer_with_openai_compatible_model() (aria.efmc.llmtools.llm_local.LLMLocal method) InfixExprParser (class in aria.efmc.verifytools.common.parser) init() (aria.automata.symautomata.pdastring.PdaString method) init_from_acceptor() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) initial_states() (aria.automata.symautomata.sfa.SFA method) intersect() (aria.automata.symautomata.pythondfa.PythonDFA method)

intersection() (aria.automata.symautomata.sfa.SFA method) invert() (aria.automata.symautomata.pythondfa.PythonDFA method) invoke() (aria.efmc.llmtools.llm_tool.LLMTool method) is_empty() (aria.automata.symautomata.sfa.SFA method) is_equivalent() (aria.automata.symautomata.sfa.Predicate method) (aria.automata.symautomata.sfa.SetPredicate method) (aria.automata.symautomata.sfa.SFA method) (aria.automata.symautomata.sfa.Z3Predicate method) is_sat() (aria.automata.symautomata.sfa.Predicate method) (aria.automata.symautomata.sfa.SetPredicate method) (aria.automata.symautomata.sfa.Z3Predicate method) items() (aria.automata.symautomata.pythondfa.Syms method)

L

LLM (class in aria.efmc.llmtools.llm_utils) LLMLocal (class in aria.efmc.llmtools.llm_local) LLMTool (class in aria.efmc.llmtools.llm_tool) LLMToolInput (class in aria.efmc.llmtools.llm_tool) LLMToolOutput (class in aria.efmc.llmtools.llm_tool)

load() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) Logger (class in aria.efmc.llmtools.logger) loopInvOverfittedCtrex() (in module aria.efmc.verifytools.tools.vc_check) loopInvSafetyCtrex() (in module aria.efmc.verifytools.tools.vc_check)

M

main() (in module aria.automata.symautomata.regex) (in module aria.automata.symautomata.sfa) maxstate (aria.automata.symautomata.cfggenerator.CFGGenerator attribute) minimize() (aria.automata.symautomata.pythondfa.PythonDFA method) module aria.automata.aalpy.automata aria.automata.symautomata.alphabet aria.automata.symautomata.cfggenerator aria.automata.symautomata.cfgpda aria.automata.symautomata.dfa aria.automata.symautomata.pda aria.automata.symautomata.pdastring aria.automata.symautomata.pythondfa aria.automata.symautomata.regex aria.automata.symautomata.sfa aria.efmc.llmtools.llm_local aria.efmc.llmtools.llm_tool aria.efmc.llmtools.llm_utils aria.efmc.llmtools.logger aria.efmc.verifytools.boogie.ast aria.efmc.verifytools.common.ast aria.efmc.verifytools.common.parser aria.efmc.verifytools.common.util aria.efmc.verifytools.daikon.inv_ast aria.efmc.verifytools.daikon.inv_grammar aria.efmc.verifytools.tools.vc_check

N

negate() (aria.automata.symautomata.sfa.Predicate method) (aria.automata.symautomata.sfa.SetPredicate method) (aria.automata.symautomata.sfa.Z3Predicate method)

next_rule() (aria.automata.symautomata.cfggenerator.CNFGenerator method) nodups() (in module aria.efmc.verifytools.common.util) nonempty() (in module aria.efmc.verifytools.common.util) normalize() (in module aria.efmc.verifytools.boogie.ast)

O

onAssert() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onAssignment() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onAssume() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onAtom() (aria.efmc.verifytools.boogie.ast.AstBuilder method) (aria.efmc.verifytools.common.parser.InfixExprParser method) (aria.efmc.verifytools.daikon.inv_ast.AstBuilder method) (aria.efmc.verifytools.daikon.inv_grammar.DaikonInvParser method) onBlock() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onBody() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onGoto() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onHavoc() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onImplementationDecl() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onLabeledStatement() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onLABinOp() (aria.efmc.verifytools.boogie.ast.AstBuilder method) (aria.efmc.verifytools.common.parser.InfixExprParser method) (aria.efmc.verifytools.daikon.inv_ast.AstBuilder method) (aria.efmc.verifytools.daikon.inv_grammar.DaikonInvParser method) onLocalVarDecl() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onNABinOp() (aria.efmc.verifytools.boogie.ast.AstBuilder method) (aria.efmc.verifytools.common.parser.InfixExprParser method) (aria.efmc.verifytools.daikon.inv_ast.AstBuilder method) (aria.efmc.verifytools.daikon.inv_grammar.DaikonInvParser method)

onProgram() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onRABinOp() (aria.efmc.verifytools.boogie.ast.AstBuilder method) (aria.efmc.verifytools.common.parser.InfixExprParser method) (aria.efmc.verifytools.daikon.inv_ast.AstBuilder method) (aria.efmc.verifytools.daikon.inv_grammar.DaikonInvParser method) onReturn() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onTernaryOp() (aria.efmc.verifytools.daikon.inv_ast.AstBuilder method) (aria.efmc.verifytools.daikon.inv_grammar.DaikonInvParser method) onType() (aria.efmc.verifytools.boogie.ast.AstBuilder method) onUnaryOp() (aria.efmc.verifytools.boogie.ast.AstBuilder method) (aria.efmc.verifytools.common.parser.InfixExprParser method) (aria.efmc.verifytools.daikon.inv_ast.AstBuilder method) (aria.efmc.verifytools.daikon.inv_grammar.DaikonInvParser method) onVariaryOp() (aria.efmc.verifytools.daikon.inv_ast.AstBuilder method) (aria.efmc.verifytools.daikon.inv_grammar.DaikonInvParser method) onWhile() (aria.efmc.verifytools.boogie.ast.AstBuilder method)

P

parse() (aria.efmc.verifytools.daikon.inv_grammar.DaikonInvParser method) parse_expr_ast() (in module aria.efmc.verifytools.daikon.inv_ast) parseAst() (in module aria.efmc.verifytools.boogie.ast) parseExprAst() (in module aria.efmc.verifytools.boogie.ast) Parser (class in aria.efmc.verifytools.common.parser) partitionAlphabet() (aria.automata.symautomata.regex.Regex method) PDA (class in aria.automata.symautomata.pda) PdaString (class in aria.automata.symautomata.pdastring)

powerset() (in module aria.efmc.verifytools.common.util) pp_exc() (in module aria.efmc.verifytools.common.util) Predicate (class in aria.automata.symautomata.sfa) print_console() (aria.efmc.llmtools.llm_local.SimpleLogger method) (aria.efmc.llmtools.logger.Logger method) print_log() (aria.efmc.llmtools.llm_local.SimpleLogger method) (aria.efmc.llmtools.logger.Logger method) printer() (aria.automata.symautomata.pdastring.PdaString method) PythonDFA (class in aria.automata.symautomata.pythondfa)

R

randomToken() (in module aria.efmc.verifytools.common.util) reduce_nodes() (in module aria.efmc.verifytools.common.ast) Regex (class in aria.automata.symautomata.regex) replace() (in module aria.efmc.verifytools.common.ast)

replaceAlphabet() (aria.automata.symautomata.regex.Regex method) replaceAlphabetMixed() (aria.automata.symautomata.regex.Regex method) resolved (aria.automata.symautomata.cfggenerator.CFGGenerator attribute) run_with_timeout() (aria.efmc.llmtools.llm_local.LLMLocal method) (aria.efmc.llmtools.llm_utils.LLM method)

S

save() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) set_final() (aria.automata.symautomata.sfa.SFA method) set_universe() (aria.automata.symautomata.sfa.Predicate method) (aria.automata.symautomata.sfa.SetPredicate method) SetPredicate (class in aria.automata.symautomata.sfa) SFA (class in aria.automata.symautomata.sfa) SFAArc (class in aria.automata.symautomata.sfa) SFAState (class in aria.automata.symautomata.sfa)

shortest_string() (aria.automata.symautomata.pda.PDA method) SimpleLogger (class in aria.efmc.llmtools.llm_local) split() (in module aria.efmc.verifytools.common.util) star() (aria.automata.symautomata.regex.Regex method) stmt_changed() (in module aria.efmc.verifytools.boogie.ast) stmt_read() (in module aria.efmc.verifytools.boogie.ast) substitutions() (in module aria.efmc.verifytools.tools.vc_check) symmetric_difference() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method) Syms (class in aria.automata.symautomata.pythondfa)

T

to_regex() (aria.automata.symautomata.sfa.SFA method) top() (aria.automata.symautomata.sfa.Predicate method) (aria.automata.symautomata.sfa.Z3Predicate method) trace_partial_input() (aria.automata.symautomata.pythondfa.PythonDFA method) traceConstantVars() (in module aria.efmc.verifytools.tools.vc_check)

tropical_weight() (in module aria.automata.symautomata.pythondfa) TropicalWeight() (in module aria.automata.symautomata.pythondfa) tryAndVerify() (in module aria.efmc.verifytools.tools.vc_check) tryAndVerify_impl() (in module aria.efmc.verifytools.tools.vc_check) tryAndVerifyLvl() (in module aria.efmc.verifytools.tools.vc_check) tryAndVerifyWithSplitterPreds() (in module aria.efmc.verifytools.tools.vc_check)

U

union() (aria.automata.symautomata.pythondfa.PythonDFA method) (aria.automata.symautomata.sfa.SFA method)

unique() (in module aria.efmc.verifytools.common.util)

Y

yyparse() (aria.automata.symautomata.cfgpda.CfgPDA method)

Z

Z3Predicate (class in aria.automata.symautomata.sfa)