Index

A

all_smt() (efmc.smttools.pysmt_solver.PySMTSolver method) assert_assertions() (efmc.smttools.smtlib_solver.SMTLIBSolver method) ast_and() (in module efmc.verifytools.boogie.ast) ast_boolean_exprs() (in module efmc.verifytools.boogie.ast) ast_constants() (in module efmc.verifytools.boogie.ast) ast_group_bin() (in module efmc.verifytools.boogie.ast) ast_or() (in module efmc.verifytools.boogie.ast) ast_primitive_boolean_exprs() (in module efmc.verifytools.boogie.ast) AstAssert (class in efmc.verifytools.boogie.ast) AstAssignment (class in efmc.verifytools.boogie.ast) AstAssume (class in efmc.verifytools.boogie.ast) AstBinding (class in efmc.verifytools.boogie.ast) AstBinExpr (class in efmc.verifytools.boogie.ast) (class in efmc.verifytools.daikon.inv_ast) AstBlock (class in efmc.verifytools.boogie.ast) AstBody (class in efmc.verifytools.boogie.ast) AstBuilder (class in efmc.verifytools.boogie.ast) (class in efmc.verifytools.daikon.inv_ast) AstFalse (class in efmc.verifytools.boogie.ast) (class in efmc.verifytools.daikon.inv_ast) AstFuncExpr (class in efmc.verifytools.boogie.ast) AstGoto (class in efmc.verifytools.boogie.ast) AstHasValues (class in efmc.verifytools.daikon.inv_ast) AstHavoc (class in efmc.verifytools.boogie.ast)

AstId (class in efmc.verifytools.boogie.ast) (class in efmc.verifytools.daikon.inv_ast) AstImplementation (class in efmc.verifytools.boogie.ast) AstInRange (class in efmc.verifytools.daikon.inv_ast) AstIntType (class in efmc.verifytools.boogie.ast) AstIsBoolean (class in efmc.verifytools.daikon.inv_ast) AstIsConstMod (class in efmc.verifytools.daikon.inv_ast) AstIsEven (class in efmc.verifytools.daikon.inv_ast) AstIsOneOf (class in efmc.verifytools.daikon.inv_ast) AstIsPow2 (class in efmc.verifytools.daikon.inv_ast) AstLabel (class in efmc.verifytools.boogie.ast) AstNode (class in efmc.verifytools.common.ast) AstNumber (class in efmc.verifytools.boogie.ast) (class in efmc.verifytools.daikon.inv_ast) AstOneExprStmt (class in efmc.verifytools.boogie.ast) AstProgram (class in efmc.verifytools.boogie.ast) AstReturn (class in efmc.verifytools.boogie.ast) AstStmt (class in efmc.verifytools.boogie.ast) AstTrue (class in efmc.verifytools.boogie.ast) (class in efmc.verifytools.daikon.inv_ast) AstUnExpr (class in efmc.verifytools.boogie.ast) (class in efmc.verifytools.daikon.inv_ast) AstWhile (class in efmc.verifytools.boogie.ast) atom() (in module efmc.frontends.mini_sygus_parser) average() (in module efmc.verifytools.common.util)

B

binary_interpolant() (efmc.smttools.pysmt_solver.PySMTSolver method) bitblast() (in module efmc.smttools.mapped_blast)

boogie_to_efmc() (in module efmc.frontends.boogie2efmc) BoogieToEFMCConverter (class in efmc.frontends.boogie2efmc) build_sygus_cnt() (in module efmc.smttools.sygus_solver)

C

c_to_efmc() (in module efmc.frontends.c2efmc) CHCParser (class in efmc.frontends.chc_parser) check_portfolio() (efmc.smttools.pysmt_solver.PySMTSolver method) check_sat() (efmc.smttools.smtlib_solver.SMTLIBSolver method) check_sat_assuming() (efmc.smttools.smtlib_solver.SMTLIBSolver method) check_sat_from_scratch() (efmc.smttools.smtlib_solver.SMTLIBSolver method) check_sat_with_pushpop_scope() (efmc.smttools.smtlib_solver.SMTLIBSolver method) check_with_pysmt() (efmc.smttools.pysmt_solver.PySMTSolver method) clear_buffers() (efmc.smttools.smtlib_solver.SmtlibProc method)

collect_vars() (in module efmc.smttools.mapped_blast) conservative_tautology() (in module efmc.verifytools.tools.vc_check) convert() (efmc.smttools.pysmt_solver.PySMTSolver static method) convert_bv_literal() (in module efmc.smttools.sygus_solver) convert_file_to_transition_system() (efmc.frontends.boogie2efmc.BoogieToEFMCConverter method) (efmc.frontends.c2efmc.CToEFMCConverter method) convert_loop_to_transition_system() (efmc.frontends.boogie2efmc.BoogieToEFMCConverter method) convert_string_literal() (in module efmc.smttools.sygus_solver) convert_sygus_expr_to_z3() (in module efmc.smttools.sygus_solver) CToEFMCConverter (class in efmc.frontends.c2efmc)

D

DaikonInvParser (class in efmc.verifytools.daikon.inv_grammar) demo_parser() (in module efmc.frontends.mini_sygus_parser)

dimacs_visitor() (in module efmc.smttools.mapped_blast) dimacs_visitor_numeric() (in module efmc.smttools.mapped_blast)

E

efmc.frontends module efmc.frontends.boogie2efmc module efmc.frontends.c2efmc module efmc.frontends.chc_parser module efmc.frontends.mini_sygus_parser module efmc.llmtools.llm_local module efmc.llmtools.llm_tool module efmc.llmtools.llm_utils module efmc.llmtools.logger module efmc.smttools.mapped_blast module efmc.smttools.pysmt_solver module efmc.smttools.smt_exceptions module

efmc.smttools.smtlib_solver module efmc.smttools.sygus_solver module efmc.verifytools.boogie.ast module efmc.verifytools.common.ast module efmc.verifytools.common.parser module efmc.verifytools.common.util module efmc.verifytools.daikon.inv_ast module efmc.verifytools.daikon.inv_grammar module efmc.verifytools.tools.vc_check module efsmt() (efmc.smttools.pysmt_solver.PySMTSolver method) error() (in module efmc.verifytools.common.util) expr_read() (in module efmc.verifytools.boogie.ast) extract_loops_from_program() (efmc.frontends.boogie2efmc.BoogieToEFMCConverter method)

F

fatal() (in module efmc.verifytools.common.util) flattenList() (in module efmc.verifytools.common.util)

flattenSet() (in module efmc.verifytools.common.util) fmls (efmc.frontends.chc_parser.CHCParser attribute)

G

generalizeConstTraceVars() (in module efmc.verifytools.tools.vc_check) get_expr_values() (efmc.smttools.smtlib_solver.SMTLIBSolver method) get_grammar() (in module efmc.frontends.mini_sygus_parser) get_nonterminals() (in module efmc.frontends.mini_sygus_parser) get_sort_sexpr() (in module efmc.smttools.sygus_solver)

get_start() (in module efmc.frontends.mini_sygus_parser) get_terms_prods() (in module efmc.frontends.mini_sygus_parser) get_transition_system() (efmc.frontends.chc_parser.CHCParser method) (efmc.frontends.mini_sygus_parser.SyGusInVParser method) get_unsat_core() (efmc.smttools.smtlib_solver.SMTLIBSolver method) ground_quantifier() (in module efmc.frontends.chc_parser)

I

infer() (efmc.llmtools.llm_local.LLMLocal method) (efmc.llmtools.llm_utils.LLM method) infer_with_deepseek_model() (efmc.llmtools.llm_utils.LLM method) infer_with_glm_model() (efmc.llmtools.llm_utils.LLM method) infer_with_openai_compatible_model() (efmc.llmtools.llm_local.LLMLocal method)

InfixExprParser (class in efmc.verifytools.common.parser) init_symbols() (efmc.frontends.mini_sygus_parser.SyGusInVParser method) input_to_list() (in module efmc.frontends.mini_sygus_parser) invoke() (efmc.llmtools.llm_tool.LLMTool method) is_literal() (in module efmc.smttools.mapped_blast) is_started() (efmc.smttools.smtlib_solver.SmtlibProc method)

L

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

LLMToolOutput (class in efmc.llmtools.llm_tool) Logger (class in efmc.llmtools.logger) loopInvOverfittedCtrex() (in module efmc.verifytools.tools.vc_check) loopInvSafetyCtrex() (in module efmc.verifytools.tools.vc_check)

M

map_bitvector() (in module efmc.smttools.mapped_blast) module efmc.frontends efmc.frontends.boogie2efmc efmc.frontends.c2efmc efmc.frontends.chc_parser efmc.frontends.mini_sygus_parser efmc.llmtools.llm_local efmc.llmtools.llm_tool efmc.llmtools.llm_utils efmc.llmtools.logger efmc.smttools.mapped_blast efmc.smttools.pysmt_solver efmc.smttools.smt_exceptions efmc.smttools.smtlib_solver efmc.smttools.sygus_solver efmc.verifytools.boogie.ast efmc.verifytools.common.ast efmc.verifytools.common.parser efmc.verifytools.common.util efmc.verifytools.daikon.inv_ast efmc.verifytools.daikon.inv_grammar efmc.verifytools.tools.vc_check

N

nodups() (in module efmc.verifytools.common.util)

nonempty() (in module efmc.verifytools.common.util) normalize() (in module efmc.verifytools.boogie.ast)

O

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

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

P

parse() (efmc.verifytools.daikon.inv_grammar.DaikonInvParser method) parse_boogie() (in module efmc.frontends) parse_boogie_file() (efmc.frontends.boogie2efmc.BoogieToEFMCConverter method) parse_c() (in module efmc.frontends) parse_c_file() (efmc.frontends.c2efmc.CToEFMCConverter method) parse_chc() (in module efmc.frontends) parse_chc_string() (efmc.frontends.chc_parser.CHCParser method) parse_expr_ast() (in module efmc.verifytools.daikon.inv_ast) parse_sexpression() (in module efmc.frontends.mini_sygus_parser) parse_sygus() (in module efmc.frontends) parse_sygus_solution() (in module efmc.smttools.sygus_solver) parseAst() (in module efmc.verifytools.boogie.ast)

parseExprAst() (in module efmc.verifytools.boogie.ast) Parser (class in efmc.verifytools.common.parser) pop() (efmc.smttools.smtlib_solver.SMTLIBSolver method) powerset() (in module efmc.verifytools.common.util) pp_exc() (in module efmc.verifytools.common.util) print_console() (efmc.llmtools.llm_local.SimpleLogger method) (efmc.llmtools.logger.Logger method) print_log() (efmc.llmtools.llm_local.SimpleLogger method) (efmc.llmtools.logger.Logger method) process_func() (efmc.frontends.mini_sygus_parser.SyGusInVParser method) proj_id_last() (in module efmc.smttools.mapped_blast) push() (efmc.smttools.smtlib_solver.SMTLIBSolver method) PySMTSolver (class in efmc.smttools.pysmt_solver)

R

randomToken() (in module efmc.verifytools.common.util) read_from_tokens() (in module efmc.frontends.mini_sygus_parser) recv() (efmc.smttools.smtlib_solver.SmtlibProc method) reduce_nodes() (in module efmc.verifytools.common.ast)

replace() (in module efmc.verifytools.common.ast) replace_fun_with_synthesized_one() (in module efmc.smttools.sygus_solver) reset() (efmc.smttools.smtlib_solver.SMTLIBSolver method) run_with_timeout() (efmc.llmtools.llm_local.LLMLocal method) (efmc.llmtools.llm_utils.LLM method)

S

send() (efmc.smttools.smtlib_solver.SmtlibProc method) sequence_interpolant() (efmc.smttools.pysmt_solver.PySMTSolver method) SimpleLogger (class in efmc.llmtools.llm_local) SMTError SmtlibError SmtlibProc (class in efmc.smttools.smtlib_solver) SMTLIBSolver (class in efmc.smttools.smtlib_solver) solve_sygus() (in module efmc.smttools.sygus_solver) solve_with_pdr() (efmc.frontends.chc_parser.CHCParser method) SolverError

split() (in module efmc.verifytools.common.util) start() (efmc.smttools.smtlib_solver.SmtlibProc method) stmt_changed() (in module efmc.verifytools.boogie.ast) stmt_read() (in module efmc.verifytools.boogie.ast) stop() (efmc.smttools.smtlib_solver.SmtlibProc method) (efmc.smttools.smtlib_solver.SMTLIBSolver method) substitutions() (in module efmc.verifytools.tools.vc_check) sygus_to_z3() (in module efmc.smttools.sygus_solver) SyGusInVParser (class in efmc.frontends.mini_sygus_parser) SyGuSParsingError synthesize_function() (in module efmc.smttools.sygus_solver)

T

test() (in module efmc.smttools.pysmt_solver) test_blast() (in module efmc.smttools.mapped_blast) test_parse() (in module efmc.frontends.chc_parser) test_parse2() (in module efmc.frontends.chc_parser) test_parse3() (in module efmc.frontends.chc_parser) to_dimacs() (in module efmc.smttools.mapped_blast) to_dimacs_numeric() (in module efmc.smttools.mapped_blast) to_pysmt_vars() (in module efmc.smttools.pysmt_solver) to_sexpr() (efmc.frontends.mini_sygus_parser.SyGusInVParser method)

to_sexpr_misc() (efmc.frontends.mini_sygus_parser.SyGusInVParser method) tokenize() (in module efmc.frontends.mini_sygus_parser) traceConstantVars() (in module efmc.verifytools.tools.vc_check) translate_smt2formula_to_cnf() (in module efmc.smttools.mapped_blast) translate_smt2formula_to_cnf_file() (in module efmc.smttools.mapped_blast) translate_smt2formula_to_numeric_clauses() (in module efmc.smttools.mapped_blast) tryAndVerify() (in module efmc.verifytools.tools.vc_check) tryAndVerify_impl() (in module efmc.verifytools.tools.vc_check) tryAndVerifyLvl() (in module efmc.verifytools.tools.vc_check) tryAndVerifyWithSplitterPreds() (in module efmc.verifytools.tools.vc_check)

U

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