Index

_

__call__() (kdrag.kernel.Proof method) (kdrag.Proof method) __contains__() (kdrag.rewrite.Order class method)

__getitem__() (kdrag.rewrite.Order class method) __iter__() (kdrag.rewrite.Order class method) __len__() (kdrag.rewrite.Order class method) __matmul__() (kdrag.contrib.hoare.Hoare method)

A

a (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) abstract_arith() (in module kdrag.theories.real), [1] accessor_def() (in module kdrag.printers.lean), [1] accessor_lemmas() (in module kdrag.datatype), [1] accessor_num() (in module kdrag.datatype), [1] add (in module kdrag.notation) add() (in module kdrag.solvers.kb.multiset), [1] (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.SATSolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) add_lemma() (kdrag.Lemma method) (kdrag.tactics.Lemma method) add_note() (kdrag.kernel.LemmaError method) (kdrag.rewrite.RewriteRuleException method) add_term() (kdrag.solvers.egraph.EGraph method) addr (kdrag.contrib.pcode.asmspec.Assert attribute) (kdrag.contrib.pcode.asmspec.Assign attribute) (kdrag.contrib.pcode.asmspec.Assume attribute) (kdrag.contrib.pcode.asmspec.BoolStmt attribute) (kdrag.contrib.pcode.asmspec.Cut attribute) (kdrag.contrib.pcode.asmspec.Entry attribute) (kdrag.contrib.pcode.asmspec.Exit attribute) addrmap (kdrag.contrib.pcode.asmspec.AsmSpec attribute) admit (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) admit() (kdrag.Lemma method) (kdrag.tactics.Lemma method) all_narrow() (in module kdrag.rewrite), [1] all_pairs() (in module kdrag.solvers.kb), [1] all_values() (in module kdrag.utils), [1] allconsts (kdrag.contrib.yosys.SmtModInfo attribute) allseqs (kdrag.contrib.yosys.SmtModInfo attribute) alpha_eq() (in module kdrag.utils), [1] alpha_norm() (in module kdrag.utils), [1]

Always (class in kdrag.contrib.pcode.asmspec) and_ (in module kdrag.notation) annot (kdrag.tactics.LemmaCallback attribute) antipattern() (in module kdrag.utils), [1] anyconsts (kdrag.contrib.yosys.SmtModInfo attribute) anyseqs (kdrag.contrib.yosys.SmtModInfo attribute) apply() (in module kdrag.rewrite), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) arb_bnd() (in module kdrag.theories.real.arb), [1] arb_ge() (in module kdrag.theories.real.arb), [1] arb_gt() (in module kdrag.theories.real.arb), [1] arb_le_ax() (in module kdrag.theories.real.arb), [1] arb_lt_ax() (in module kdrag.theories.real.arb), [1] arb_over_of_mid_rad() (in module kdrag.theories.real.arb), [1] arg() (in module kdrag.smt), [1] (kdrag.contrib.expr.ExprRef method) args (kdrag.kernel.Defn attribute) (kdrag.kernel.LemmaError attribute) (kdrag.rewrite.RewriteRuleException attribute) arity() (kdrag.contrib.expr.FuncDeclRef method) asize (kdrag.contrib.yosys.SmtModInfo attribute) AsmSpec (class in kdrag.contrib.pcode.asmspec) assemble_and_check() (in module kdrag.contrib.pcode.asmspec), [1] assemble_and_check_str() (in module kdrag.contrib.pcode.asmspec), [1] assemble_and_gen_vcs() (in module kdrag.contrib.pcode.asmspec), [1] Assert (class in kdrag.contrib.pcode.asmspec) assert_and_track() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) assert_eq() (kdrag.property.TypeClass method) asserts (kdrag.contrib.yosys.SmtModInfo attribute) Assign (class in kdrag.contrib.pcode.asmspec) assign() (kdrag.contrib.hoare.Hoare class method) assoc_comm() (in module kdrag.property), [1] assoc_norm() (in module kdrag.property), [1] Assume (class in kdrag.contrib.pcode.asmspec) assumes (kdrag.contrib.yosys.SmtModInfo attribute) assumption() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ast_size_sexpr() (in module kdrag.utils), [1] AstRef (class in kdrag.contrib.expr) auto() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ax (kdrag.kernel.Defn attribute) axiom() (in module kdrag) (in module kdrag.kernel), [1]

B

b (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) backward_rule() (in module kdrag.rewrite), [1] BaseSolver (class in kdrag.solvers) basic() (in module kdrag.solvers.kb), [1] beta() (in module kdrag.rewrite), [1]

BigUnion() (in module kdrag.theories.set), [1] BinaryContext (class in kdrag.contrib.pcode) binop() (in module kdrag.hypothesis), [1] binops() (in module kdrag.hypothesis), [1] binpath() (in module kdrag.solvers), [1] bits (kdrag.contrib.pcode.MemState attribute) BitVecN (in module kdrag.theories.bitvec) BitVecNConst() (in module kdrag.theories.bitvec), [1] BitVecNVal() (in module kdrag.theories.bitvec), [1] BitVecSort() (in module kdrag.theories.bitvec), [1] body (kdrag.kernel.Defn attribute) BoolSort() (in module kdrag.smt), [1] BoolStmt (class in kdrag.contrib.pcode.asmspec) bound() (kdrag.solvers.gappa.GappaSolver method) bound_ax() (in module kdrag.theories.real.arb), [1] bounds() (in module kdrag.theories.real.arb), [1] BVNot() (in module kdrag.theories.bitvec), [1]

C

c (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) c_of_expr() (in module kdrag.printers.c), [1] Calc (class in kdrag) (class in kdrag.tactics) call_yosys_functional() (in module kdrag.contrib.yosys), [1] cases() (kdrag.Lemma method) (kdrag.tactics.Lemma method) cause (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) cb (kdrag.tactics.LemmaCallback attribute) cells (kdrag.contrib.yosys.SmtModInfo attribute) check() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.SATSolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) check_tptp_status() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) children() (kdrag.contrib.expr.ExprRef method)

clear() (kdrag.Lemma method) (kdrag.tactics.Lemma method) clocks (kdrag.contrib.yosys.SmtModInfo attribute) cmds (kdrag.contrib.hoare.Hoare attribute) collect_decls() (in module kdrag.solvers), [1] collect_sorts() (in module kdrag.solvers), [1] comm_norm() (in module kdrag.property), [1] compares() (in module kdrag.hypothesis), [1] compile_and_link() (in module kdrag.printers.c), [1] compile_and_link_defn() (in module kdrag.printers.c), [1] compile_c() (in module kdrag.printers.c), [1] compile_rust() (in module kdrag.printers.rust), [1] complement() (in module kdrag.theories.set), [1] compose() (in module kdrag.kernel), [1] conc (kdrag.rewrite.Rule attribute) Cond (class in kdrag.notation) cond() (in module kdrag) (in module kdrag.notation), [1] conde() (in module kdrag.notation), [1] Cons() (in module kdrag.theories.list), [1] consider() (in module kdrag.kernel), [1] Const() (in module kdrag.contrib.expr), [1] (kdrag.contrib.pcode.MemState class method) constructor_num() (in module kdrag.datatype), [1] Consts() (in module kdrag.contrib.expr), [1] consts() (in module kdrag.utils), [1] Context (class in kdrag.contrib.expr) copy() (kdrag.Lemma method) (kdrag.solvers.egraph.EGraph method) (kdrag.tactics.Lemma method) cos_bnd() (in module kdrag.theories.real.arb), [1] count() (in module kdrag.solvers.kb.multiset), [1] (kdrag.contrib.pcode.asmspec.VerificationCondition method) (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.tactics.Goal method) counter (kdrag.contrib.expr.Context attribute) countermodel() (kdrag.contrib.pcode.asmspec.VerificationCondition method) covers (kdrag.contrib.yosys.SmtModInfo attribute) cstring() (in module kdrag.printers.c), [1] ctx (kdrag.contrib.expr.AstRef attribute) (kdrag.contrib.expr.ExprRef attribute) (kdrag.contrib.expr.FuncDeclRef attribute) (kdrag.contrib.expr.SortRef attribute) (kdrag.contrib.expr.TypeVarRef attribute) (kdrag.tactics.Goal attribute) ctype_of_sort() (in module kdrag.printers.c), [1] Cut (class in kdrag.contrib.pcode.asmspec)

D

Datalog (class in kdrag.solvers.datalog) datatype() (in module kdrag.reflect), [1] datatype_call() (in module kdrag.datatype), [1] datatype_iter() (in module kdrag.datatype), [1] datatype_len() (in module kdrag.datatype), [1] datatype_match_() (in module kdrag.datatype), [1] datatype_replace() (in module kdrag.datatype), [1] decl() (in module kdrag.smt), [1] (kdrag.contrib.expr.ExprRef method) decl_axiom() (in module kdrag.printers.lean), [1] decl_index() (in module kdrag.rewrite), [1] decl_sig() (in module kdrag.printers.lean), [1] declare_sig() (kdrag.solvers.datalog.Datalog method) DeclareSort() (in module kdrag.smt), [1] decls() (in module kdrag.utils), [1] deduce() (in module kdrag.solvers.kb.multiset), [1] (in module kdrag.solvers.kb.string), [1]

def_eq() (in module kdrag.rewrite), [1] default (kdrag.reflect.KnuckleClosure attribute) define() (in module kdrag) (in module kdrag.kernel), [1] (kdrag.notation.SortDispatch method) define_fix() (in module kdrag.kernel), [1] define_fun() (in module kdrag.datatype), [1] Defn (class in kdrag.kernel) defns (in module kdrag.kernel) diff() (in module kdrag.theories.real.sympy), [1] (in module kdrag.theories.set), [1] diff_shim() (in module kdrag.theories.real.sympy), [1] disassemble() (kdrag.contrib.pcode.BinaryContext method) distinct_lemmas() (in module kdrag.datatype), [1] div (in module kdrag.notation) domain() (kdrag.contrib.expr.FuncDeclRef method) dot() (kdrag.solvers.egraph.EGraph method)

E

eclasses() (kdrag.solvers.egraph.EGraph method) EgglogSolver (class in kdrag.solvers.egglog) EGraph (class in kdrag.solvers.egraph) einstan() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) ematch() (kdrag.solvers.egraph.EGraph method) empty() (kdrag.tactics.Goal class method) Entry (class in kdrag.contrib.pcode.asmspec) Enum() (in module kdrag.datatype), [1] EProverTHFSolver (class in kdrag.solvers) eq (in module kdrag.notation) EQ (kdrag.rewrite.Order attribute) Eq() (in module kdrag.smt), [1] eq() (in module kdrag.smt), [1] (kdrag.Calc method) (kdrag.contrib.expr.AstRef method) (kdrag.contrib.expr.ExprRef method) (kdrag.contrib.expr.FuncDeclRef method) (kdrag.contrib.expr.SortRef method) (kdrag.contrib.expr.TypeVarRef method) (kdrag.Lemma method) (kdrag.tactics.Calc method) (kdrag.tactics.Lemma method) eval_() (in module kdrag.reflect), [1] execute1() (kdrag.contrib.pcode.BinaryContext method) execute1_schema() (kdrag.contrib.pcode.BinaryContext method) execute_insn() (in module kdrag.contrib.pcode.asmspec), [1] execute_spec_stmts() (in module kdrag.contrib.pcode.asmspec), [1] executeBinary() (in module kdrag.contrib.pcode), [1] executeBranch() (kdrag.contrib.pcode.BinaryContext method) executeCBranch() (in module kdrag.contrib.pcode), [1]

executeCurrentOp() (kdrag.contrib.pcode.BinaryContext method) executeInsn() (kdrag.contrib.pcode.BinaryContext method) executeLoad() (in module kdrag.contrib.pcode), [1] executePopcount() (in module kdrag.contrib.pcode), [1] executeSignExtend() (in module kdrag.contrib.pcode), [1] executeStore() (in module kdrag.contrib.pcode), [1] executeSubpiece() (in module kdrag.contrib.pcode), [1] executeUnary() (in module kdrag.contrib.pcode), [1] exists() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ExistsUnique() (in module kdrag.notation), [1] Exit (class in kdrag.contrib.pcode.asmspec) exp_bnd() (in module kdrag.theories.real.arb), [1] expand() (in module kdrag.theories.real.sympy), [1] expr (kdrag.contrib.pcode.asmspec.Always attribute) (kdrag.contrib.pcode.asmspec.Assert attribute) (kdrag.contrib.pcode.asmspec.Assign attribute) (kdrag.contrib.pcode.asmspec.Assume attribute) (kdrag.contrib.pcode.asmspec.BoolStmt attribute) (kdrag.contrib.pcode.asmspec.Cut attribute) (kdrag.contrib.pcode.asmspec.Entry attribute) (kdrag.contrib.pcode.asmspec.Exit attribute) expr() (in module kdrag.reflect), [1] (kdrag.notation.Cond method) expr_kind() (in module kdrag.smt), [1] expr_to_smtlib() (in module kdrag.solvers), [1] expr_to_tptp() (in module kdrag.solvers), [1] ExprRef (class in kdrag.contrib.expr) ext() (kdrag.Lemma method) (kdrag.tactics.Lemma method) extract() (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.egraph.EGraph method)

F

factor() (in module kdrag.theories.real.sympy), [1] failures (kdrag.contrib.pcode.asmspec.Results attribute) fallthruOp() (kdrag.contrib.pcode.BinaryContext method) find() (kdrag.solvers.egraph.EGraph method) find_calls() (in module kdrag.utils), [1] Finite() (in module kdrag.theories.set), [1] finsize() (in module kdrag.printers), [1] FinSort() (in module kdrag.theories.real.vec), [1] fix() (kdrag.Lemma method) (kdrag.tactics.Lemma method) FixedSort() (in module kdrag.theories.fixed), [1] fixes() (kdrag.Lemma method) (kdrag.tactics.Lemma method) flint_bnd() (in module kdrag.theories.real.arb), [1] flint_eq_ax_unsafe() (in module kdrag.theories.real.arb), [1] forall() (kdrag.kernel.Proof method) (kdrag.Proof method) ForAllI() (in module kdrag.tactics), [1] forallI() (in module kdrag.tactics), [1]

forget() (in module kdrag.kernel), [1] forget2() (in module kdrag.kernel), [1] forward_rule() (in module kdrag.rewrite), [1] free_in() (in module kdrag.utils), [1] free_vars() (in module kdrag.utils), [1] fresh_const() (in module kdrag.kernel), [1] fresh_symbol() (in module kdrag.theories.real.sympy), [1] FreshConst() (in module kdrag.contrib.expr), [1] freshen() (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) from_expr() (kdrag.rewrite.RewriteRule class method) from_file() (kdrag.contrib.yosys.VerilogModule class method) fromBV() (in module kdrag.theories.bitvec), [1] full_simp() (in module kdrag.rewrite), [1] func_kind() (in module kdrag.smt), [1] funcdecl_smtlib() (in module kdrag.solvers), [1] FuncDeclRef (class in kdrag.contrib.expr) Function() (in module kdrag.contrib.expr), [1] (in module kdrag.smt), [1]

G

gappa_of_bool() (in module kdrag.solvers.gappa), [1] gappa_of_real() (in module kdrag.solvers.gappa), [1] GappaSolver (class in kdrag.solvers.gappa) ge (in module kdrag.notation) ge() (kdrag.Calc method) (kdrag.tactics.Calc method) generalize() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) generate() (in module kdrag.utils), [1] GenericProof (class in kdrag.property) get() (in module kdrag.theories.option), [1] (kdrag.property.GenericProof method) get_id() (in module kdrag.smt), [1] (kdrag.contrib.expr.AstRef method) (kdrag.contrib.expr.ExprRef method) (kdrag.contrib.expr.FuncDeclRef method) (kdrag.contrib.expr.SortRef method) (kdrag.contrib.expr.TypeVarRef method)

get_lemma() (kdrag.Lemma method) (kdrag.tactics.Lemma method) get_proof() (kdrag.solvers.egraph.EGraph method) get_reg() (kdrag.contrib.pcode.BinaryContext method) get_registry() (kdrag.property.TypeClass class method) get_regs() (kdrag.contrib.pcode.BinaryContext method) get_vars() (in module kdrag.solvers.prolog), [1] getitem (in module kdrag.notation) getvalue() (kdrag.contrib.pcode.MemState method) getvalue_ram() (kdrag.contrib.pcode.MemState method) ghost_env (kdrag.contrib.pcode.asmspec.TraceState attribute) (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) globals (kdrag.reflect.KnuckleClosure attribute) Goal (class in kdrag.tactics) goal (kdrag.tactics.Goal attribute) GR (kdrag.rewrite.Order attribute) gt (in module kdrag.notation) gt() (kdrag.Calc method) (kdrag.tactics.Calc method)

H

have() (kdrag.Lemma method) (kdrag.tactics.Lemma method) herb() (in module kdrag.kernel), [1]

Hoare (class in kdrag.contrib.hoare) huet() (in module kdrag.solvers.kb), [1] huet_smt2_file() (in module kdrag.solvers.kb), [1] hyp (kdrag.rewrite.Rule attribute)

I

idem_norm() (in module kdrag.property), [1] in_range() (in module kdrag.theories.float), [1] in_terms() (kdrag.solvers.egraph.EGraph method) index() (kdrag.contrib.pcode.asmspec.VerificationCondition method) (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.tactics.Goal method) induct (in module kdrag.notation) induct() (in module kdrag.theories.int), [1] (in module kdrag.theories.seq), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) induct_inductive() (in module kdrag.kernel), [1] induct_list() (in module kdrag.theories.seq), [1] induct_nat() (in module kdrag.theories.int), [1] induct_nat_strong() (in module kdrag.theories.int), [1] Inductive() (in module kdrag) (in module kdrag.kernel), [1] InductiveRel() (in module kdrag.datatype), [1] infer_sort() (in module kdrag.reflect), [1] init_constrs (kdrag.contrib.yosys.VerilogModule attribute) init_mem() (kdrag.contrib.pcode.BinaryContext method) init_proj() (in module kdrag.printers.rust), [1] inj_lemmas() (in module kdrag.datatype), [1] Injective() (in module kdrag.theories.set), [1] input_sort (kdrag.contrib.yosys.VerilogModule attribute) inputs (kdrag.contrib.yosys.SmtModInfo attribute) install_solvers() (in module kdrag.solvers), [1] install_solvers2() (in module kdrag.solvers), [1] instan() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) instan2() (in module kdrag.kernel), [1] integ_shim() (in module kdrag.theories.real.sympy), [1]

integrate() (in module kdrag.theories.real.sympy), [1] inter() (in module kdrag.theories.set), [1] interp() (in module kdrag.solvers.prolog), [1] interp_flint() (in module kdrag.theories.real.arb), [1] interp_pred() (in module kdrag.solvers.prolog), [1] interp_term() (in module kdrag.solvers.prolog), [1] intros() (kdrag.Lemma method) (kdrag.tactics.Lemma method) IntSort() (in module kdrag.smt), [1] invert (in module kdrag.notation) is_accessor() (in module kdrag.smt), [1] is_app() (in module kdrag.smt), [1] is_constructor() (in module kdrag.smt), [1] is_defined() (in module kdrag.kernel), [1] is_empty() (kdrag.tactics.Goal method) is_eq() (kdrag.solvers.egraph.EGraph method) is_finite() (in module kdrag.theories.float), [1] is_if() (in module kdrag.smt), [1] is_neg() (in module kdrag.smt), [1] is_option() (in module kdrag.theories.option), [1] is_power() (in module kdrag.smt), [1] is_proof() (in module kdrag.kernel), [1] is_recognizer() (in module kdrag.smt), [1] is_schema_var() (in module kdrag.kernel), [1] is_set() (in module kdrag.theories.set), [1] is_strict_subterm() (in module kdrag.utils), [1] is_subterm() (in module kdrag.utils), [1] is_trivial() (in module kdrag.solvers.kb), [1] is_uninterp() (in module kdrag.smt), [1] is_valid_c_identifier() (in module kdrag.printers.c), [1] is_valid_c_identifier_strict() (in module kdrag.printers.c), [1] is_value() (in module kdrag.utils), [1] IsFinite() (in module kdrag.theories.float), [1] ite() (kdrag.contrib.hoare.Hoare class method) iter() (kdrag.solvers.egraph.EGraph method)

J

Judgement (class in kdrag.kernel)

K

k (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) KB() (in module kdrag.solvers.kb.multiset), [1] (in module kdrag.solvers.kb.string), [1] kbo() (in module kdrag.rewrite), [1] kdify() (in module kdrag.theories.real.sympy), [1] kdrag module kdrag.all module kdrag.config module kdrag.contrib module kdrag.contrib.data_modulo module kdrag.contrib.expr module kdrag.contrib.hoare module kdrag.contrib.pcode module kdrag.contrib.pcode.asmspec module kdrag.contrib.telescope module kdrag.contrib.yosys module kdrag.datatype module kdrag.hypothesis module kdrag.kernel module kdrag.notation module kdrag.parsers module kdrag.parsers.smtlib module kdrag.parsers.tptp module kdrag.parsers.trs module kdrag.printers module kdrag.printers.c module kdrag.printers.lean module kdrag.printers.rust module kdrag.printers.verilog module kdrag.property module kdrag.reflect module kdrag.rewrite module kdrag.smt module

kdrag.solvers module kdrag.solvers.aprove module kdrag.solvers.datalog module kdrag.solvers.egglog module kdrag.solvers.egraph module kdrag.solvers.gappa module kdrag.solvers.kb module kdrag.solvers.kb.multiset module kdrag.solvers.kb.string module kdrag.solvers.ljt module kdrag.solvers.prolog module kdrag.tactics module kdrag.theories module kdrag.theories.bitvec module kdrag.theories.bool module kdrag.theories.fixed module kdrag.theories.float module kdrag.theories.fun module kdrag.theories.int module kdrag.theories.list module kdrag.theories.nat module kdrag.theories.option module kdrag.theories.real module kdrag.theories.real.arb module kdrag.theories.real.complex module kdrag.theories.real.extended module kdrag.theories.real.geometry module kdrag.theories.real.interval module kdrag.theories.real.ndarray module kdrag.theories.real.sympy module kdrag.theories.real.vec module kdrag.theories.regex module kdrag.theories.seq module kdrag.theories.set module kdrag.utils module kind() (kdrag.contrib.expr.SortRef method) KnuckleClosure (class in kdrag.reflect)

L

label (kdrag.contrib.pcode.asmspec.Assert attribute) (kdrag.contrib.pcode.asmspec.Assign attribute) (kdrag.contrib.pcode.asmspec.Assume attribute) (kdrag.contrib.pcode.asmspec.BoolStmt attribute) (kdrag.contrib.pcode.asmspec.Cut attribute) (kdrag.contrib.pcode.asmspec.Entry attribute) (kdrag.contrib.pcode.asmspec.Exit attribute) lam (kdrag.reflect.KnuckleClosure attribute) le (in module kdrag.notation) le() (kdrag.Calc method) (kdrag.tactics.Calc method) LeanSolver (class in kdrag.solvers) left() (kdrag.Lemma method) (kdrag.tactics.Lemma method) Lemma (class in kdrag) (class in kdrag.tactics) lemma() (kdrag.property.GenericProof method)

lemma_db() (in module kdrag.utils), [1] LemmaCallback (class in kdrag.tactics) LemmaError LeoIIISolver (class in kdrag.solvers) let() (kdrag.solvers.egglog.EgglogSolver method) lhs (kdrag.rewrite.RewriteRule attribute) limit() (in module kdrag.theories.real.sympy), [1] link() (in module kdrag.printers.c), [1] List() (in module kdrag.theories.list), [1] list() (in module kdrag.theories.list), [1] load() (kdrag.contrib.pcode.BinaryContext method) locals (kdrag.reflect.KnuckleClosure attribute) lookup() (kdrag.property.TypeClass class method) lpo() (in module kdrag.rewrite), [1] lt (in module kdrag.notation) lt() (kdrag.Calc method) (kdrag.tactics.Calc method)

M

m (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) main_ctx() (in module kdrag.contrib.expr), [1] mangle_decl() (in module kdrag.solvers), [1] mangle_decl_smtlib() (in module kdrag.solvers), [1] mangle_name() (in module kdrag.solvers.egglog), [1] matmul (in module kdrag.notation) maximize (kdrag.contrib.yosys.SmtModInfo attribute) mem (kdrag.contrib.pcode.MemState attribute) member() (in module kdrag.theories.set), [1] memories (kdrag.contrib.yosys.SmtModInfo attribute) MemSorts (in module kdrag.contrib.pcode) MemState (class in kdrag.contrib.pcode) memstate (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) (kdrag.contrib.pcode.SimState attribute) min_float64 (in module kdrag.theories.float) minimize (kdrag.contrib.yosys.SmtModInfo attribute) model_registers() (kdrag.contrib.pcode.BinaryContext method) module kdrag kdrag.all kdrag.config kdrag.contrib kdrag.contrib.data_modulo kdrag.contrib.expr kdrag.contrib.hoare kdrag.contrib.pcode kdrag.contrib.pcode.asmspec kdrag.contrib.telescope kdrag.contrib.yosys kdrag.datatype kdrag.hypothesis kdrag.kernel kdrag.notation kdrag.parsers kdrag.parsers.smtlib kdrag.parsers.tptp kdrag.parsers.trs kdrag.printers kdrag.printers.c kdrag.printers.lean kdrag.printers.rust kdrag.printers.verilog kdrag.property kdrag.reflect kdrag.rewrite kdrag.smt kdrag.solvers kdrag.solvers.aprove kdrag.solvers.datalog kdrag.solvers.egglog kdrag.solvers.egraph kdrag.solvers.gappa kdrag.solvers.kb kdrag.solvers.kb.multiset kdrag.solvers.kb.string kdrag.solvers.ljt kdrag.solvers.prolog kdrag.tactics kdrag.theories kdrag.theories.bitvec kdrag.theories.bool kdrag.theories.fixed kdrag.theories.float kdrag.theories.fun kdrag.theories.int kdrag.theories.list kdrag.theories.nat kdrag.theories.option kdrag.theories.real kdrag.theories.real.arb kdrag.theories.real.complex kdrag.theories.real.extended kdrag.theories.real.geometry kdrag.theories.real.interval kdrag.theories.real.ndarray kdrag.theories.real.sympy kdrag.theories.real.vec kdrag.theories.regex kdrag.theories.seq kdrag.theories.set kdrag.utils

modus() (in module kdrag.kernel), [1] ms_order() (in module kdrag.solvers.kb.multiset), [1] mul (in module kdrag.notation) multipattern_match() (in module kdrag.datatype), [1] MultiSolver (class in kdrag.solvers)

N

n (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) name (kdrag.contrib.pcode.asmspec.Assign attribute) (kdrag.kernel.Defn attribute) name() (kdrag.contrib.expr.FuncDeclRef method) (kdrag.contrib.expr.SortRef method)

namedtuple_of_constructor() (in module kdrag.reflect), [1] NanoCopISolver (class in kdrag.solvers) nbe() (in module kdrag.reflect), [1] ne (in module kdrag.notation) neg (in module kdrag.notation) newgoal() (kdrag.Lemma method) (kdrag.tactics.Lemma method) NewType() (in module kdrag) (in module kdrag.datatype), [1] NGE (kdrag.rewrite.Order attribute) Nil() (in module kdrag.theories.list), [1] no_overflow() (in module kdrag.theories.float), [1] None_() (in module kdrag.theories.option), [1] NoOverflow() (in module kdrag.theories.float), [1] normalize() (in module kdrag.contrib.telescope), [1] num_args() (in module kdrag.smt), [1] (kdrag.contrib.expr.ExprRef method)

O

occurs() (in module kdrag.utils), [1] of_datatype() (in module kdrag.printers.lean), [1] of_defn() (in module kdrag.printers.c), [1] of_expr() (in module kdrag.printers.lean), [1] of_file() (kdrag.contrib.pcode.asmspec.AsmSpec class method) of_sort() (in module kdrag.printers.lean), [1] (in module kdrag.printers.rust), [1] open_binder() (in module kdrag.utils), [1] open_binder_unhygienic() (in module kdrag.utils), [1]

Option() (in module kdrag.theories.option), [1] or_ (in module kdrag.notation) Order (class in kdrag.rewrite) orient() (in module kdrag.solvers.kb), [1] otherwise() (kdrag.notation.Cond method) output_sort (kdrag.contrib.yosys.VerilogModule attribute) outputs (kdrag.contrib.yosys.SmtModInfo attribute) overlap() (in module kdrag.solvers.kb.multiset), [1] overlaps() (in module kdrag.solvers.kb.string), [1]

P

path_cond (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) (kdrag.contrib.pcode.SimState attribute) pattern_match() (in module kdrag.datatype), [1] pc (kdrag.contrib.pcode.SimState attribute) pc_of_addr() (in module kdrag.contrib.pcode), [1] perf_event() (in module kdrag.config), [1] pf (kdrag.rewrite.RewriteRule attribute) (kdrag.rewrite.Rule attribute) pmatch() (in module kdrag.utils), [1] pmatch_fo() (in module kdrag.utils), [1] pmatch_rec() (in module kdrag.utils), [1] pop() (kdrag.Lemma method) (kdrag.tactics.Lemma method) pop_goal() (kdrag.Lemma method) (kdrag.tactics.Lemma method) PopCount() (in module kdrag.theories.bitvec), [1] post (kdrag.contrib.hoare.Hoare attribute) pre (kdrag.contrib.hoare.Hoare attribute) predefined (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) predefined_names (kdrag.solvers.egglog.EgglogSolver attribute) predefined_sorts (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

pretty_insn() (in module kdrag.contrib.pcode), [1] pretty_op() (in module kdrag.contrib.pcode), [1] prolog() (in module kdrag.solvers.prolog), [1] prompt() (in module kdrag.utils), [1] Proof (class in kdrag) (class in kdrag.kernel) proof() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) prove() (in module kdrag) (in module kdrag.kernel), [1] (in module kdrag.solvers.ljt), [1] (in module kdrag.tactics), [1] prune() (in module kdrag.utils), [1] push() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

Q

qed() (kdrag.Calc method) (kdrag.Lemma method) (kdrag.tactics.Calc method) (kdrag.tactics.Lemma method) QExists() (in module kdrag) (in module kdrag.notation), [1]

QForAll() (in module kdrag) (in module kdrag.notation), [1] QLambda() (in module kdrag.notation), [1] quant_kind_eq() (in module kdrag.utils), [1] quantifier_call() (in module kdrag.notation), [1] query() (kdrag.solvers.VampireSolver method) quickcheck() (in module kdrag.hypothesis), [1]

R

radd (in module kdrag.notation) Range() (in module kdrag.theories.set), [1] range() (kdrag.contrib.expr.FuncDeclRef method) RealSort() (in module kdrag.smt), [1] reason (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) reasons (kdrag.contrib.hoare.Hoare attribute) (kdrag.solvers.egraph.EGraph attribute) rebuild() (kdrag.solvers.egraph.EGraph method) recognizer_lemmas() (in module kdrag.datatype), [1] reflect() (in module kdrag.reflect), [1] register() (kdrag.notation.SortDispatch method) (kdrag.property.GenericProof method) (kdrag.property.TypeClass class method) registers (kdrag.contrib.yosys.SmtModInfo attribute) reify() (in module kdrag.reflect), [1] rel (in module kdrag.datatype) replace() (in module kdrag.solvers.kb.multiset), [1] (in module kdrag.solvers.kb.string), [1] res (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) ReSort() (in module kdrag.theories.regex), [1] Results (class in kdrag.contrib.pcode.asmspec)

rewrite() (in module kdrag.rewrite), [1] (in module kdrag.solvers.kb.multiset), [1] (in module kdrag.solvers.kb.string), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) rewrite1() (in module kdrag.rewrite), [1] rewrite1_rule() (in module kdrag.rewrite), [1] rewrite_of_expr() (in module kdrag.rewrite), [1] rewrite_once() (in module kdrag.rewrite), [1] rewrite_slow() (in module kdrag.rewrite), [1] RewriteRule (class in kdrag.rewrite) RewriteRuleException rhs (kdrag.rewrite.RewriteRule attribute) right() (kdrag.Lemma method) (kdrag.tactics.Lemma method) rlemma() (in module kdrag.theories.real), [1] rmul (in module kdrag.notation) roots (kdrag.solvers.egraph.EGraph attribute) round_up_neg (in module kdrag.theories.float) Rule (class in kdrag.rewrite) rule_of_expr() (in module kdrag.rewrite), [1] run() (in module kdrag.solvers), [1] (kdrag.solvers.datalog.Datalog method) (kdrag.solvers.egglog.EgglogSolver method) run_all_paths() (in module kdrag.contrib.pcode.asmspec), [1] run_aprove() (in module kdrag.solvers.aprove), [1] run_cmd() (kdrag.solvers.egglog.EgglogSolver method) run_lean() (in module kdrag.printers.lean), [1] run_string() (in module kdrag.solvers.prolog), [1] rust_module_template() (in module kdrag.printers.rust), [1] rw() (kdrag.Lemma method) (kdrag.solvers.egraph.EGraph method) (kdrag.tactics.Lemma method)

S

sanity_check_consistency() (in module kdrag.utils), [1] SATSolver (class in kdrag.solvers) SchemaVar() (in module kdrag.kernel), [1] SchemaVars() (in module kdrag.tactics), [1] search() (in module kdrag) (in module kdrag.utils), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) search_decl() (in module kdrag.utils), [1] search_expr() (in module kdrag.utils), [1] select64() (in module kdrag.theories.bitvec), [1] SelectConcat() (in module kdrag.theories.bitvec), [1] Seq() (in module kdrag.theories.seq), [1] seq() (in module kdrag.theories.seq), [1] series() (in module kdrag.theories.real.sympy), [1] Set() (in module kdrag.theories.set), [1] set() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) set_reg() (kdrag.contrib.pcode.BinaryContext method) setvalue() (kdrag.contrib.pcode.MemState method) setvalue_ram() (kdrag.contrib.pcode.MemState method) shim_ho() (in module kdrag.theories.real.sympy), [1] shortlex() (in module kdrag.solvers.kb.multiset), [1] shortlex_swap() (in module kdrag.solvers.kb.string), [1] show() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sig (kdrag.tactics.Goal attribute) simp() (in module kdrag) (in module kdrag.rewrite), [1] (in module kdrag.tactics), [1] (in module kdrag.theories.real.sympy), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) simp1() (in module kdrag.rewrite), [1] simp2() (in module kdrag.rewrite), [1] simp_tac() (in module kdrag.tactics), [1] simplify() (in module kdrag.solvers.kb), [1] (in module kdrag.solvers.kb.string), [1] (in module kdrag.theories.real.sympy), [1] simplify_terms() (kdrag.solvers.egraph.EGraph method) SimState (class in kdrag.contrib.pcode) sin_bnd() (in module kdrag.theories.real.arb), [1]

sin_lower() (in module kdrag.theories.real), [1] skip() (kdrag.contrib.hoare.Hoare class method) skolem() (in module kdrag.kernel), [1] smt2tptp() (in module kdrag.solvers), [1] smt_datatype_val() (in module kdrag.hypothesis), [1] smt_generic_val() (in module kdrag.hypothesis), [1] smt_metadata() (in module kdrag.contrib.yosys), [1] smt_seq_val() (in module kdrag.hypothesis), [1] smtlib_datatypes() (in module kdrag.solvers), [1] SmtModInfo (class in kdrag.contrib.yosys) solve() (in module kdrag.theories.real.sympy), [1] solver (kdrag.solvers.egraph.EGraph attribute) solver_classes (kdrag.solvers.MultiSolver attribute) Some() (in module kdrag.theories.option), [1] sort() (in module kdrag.smt), [1] sort_axiom() (in module kdrag.printers.lean), [1] sort_kind() (in module kdrag.smt), [1] sort_occurs() (in module kdrag.hypothesis), [1] sort_of_type() (in module kdrag.reflect), [1] sort_to_tptp() (in module kdrag.solvers), [1] SortDispatch (class in kdrag.notation) SortRef (class in kdrag.contrib.expr) sorts() (in module kdrag.utils), [1] split() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sqrt_bnd() (in module kdrag.theories.real), [1] sqrt_lower() (in module kdrag.theories.real), [1] sqrt_upper() (in module kdrag.theories.real), [1] start (kdrag.contrib.pcode.asmspec.TraceState attribute) (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) state (kdrag.contrib.pcode.asmspec.TraceState attribute) state_sort (kdrag.contrib.yosys.VerilogModule attribute) StoreConcat() (in module kdrag.theories.bitvec), [1] strengthen_pre() (kdrag.contrib.hoare.Hoare method) Struct() (in module kdrag) (in module kdrag.datatype), [1] sub (in module kdrag.notation) sub() (in module kdrag.solvers.kb.multiset), [1] subseq() (in module kdrag.solvers.kb.string), [1] subset() (in module kdrag.theories.set), [1] subst() (in module kdrag.tactics), [1] substitute() (kdrag.contrib.pcode.BinaryContext method) substitute_ghost() (in module kdrag.contrib.pcode.asmspec), [1] substitute_schema_vars() (in module kdrag.kernel), [1] subterms() (in module kdrag.utils), [1] successes (kdrag.contrib.pcode.asmspec.Results attribute) sum_shim() (in module kdrag.theories.real.sympy), [1] summation() (in module kdrag.theories.real.sympy), [1] Surjective() (in module kdrag.theories.set), [1] sym_execute() (kdrag.contrib.pcode.BinaryContext method) symm() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sympify() (in module kdrag.theories.real.sympy), [1]

T

tan_bnd() (in module kdrag.theories.real.arb), [1] terms (kdrag.solvers.egraph.EGraph attribute) test() (in module kdrag.parsers.smtlib), [1] (in module kdrag.parsers.tptp), [1] (in module kdrag.parsers.trs), [1] test_pcode() (in module kdrag.contrib.pcode), [1] TExists() (in module kdrag.contrib.telescope), [1] TForAll() (in module kdrag.contrib.telescope), [1] then() (kdrag.notation.Cond method) thm (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) to_expr() (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) to_int (in module kdrag.notation) to_real (in module kdrag.notation)

to_verilog() (in module kdrag.printers.verilog), [1] toBV() (in module kdrag.theories.bitvec), [1] top_goal() (kdrag.Lemma method) (kdrag.tactics.Lemma method) tptp2smt() (in module kdrag.solvers), [1] trace (kdrag.contrib.pcode.asmspec.TraceState attribute) (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) TraceState (class in kdrag.contrib.pcode.asmspec) trans_fun (kdrag.contrib.yosys.VerilogModule attribute) translate() (kdrag.contrib.pcode.BinaryContext method) translate_tuple_args() (in module kdrag.theories.real.sympy), [1] TweeSolver (class in kdrag.solvers) type_of_sort() (in module kdrag.reflect), [1] TypeClass (class in kdrag.property) TypeVarRef (class in kdrag.contrib.expr)

U

uf (kdrag.solvers.egraph.EGraph attribute) unfold() (in module kdrag.rewrite), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) unify() (in module kdrag.utils), [1] unify_db() (in module kdrag.utils), [1] union() (in module kdrag.theories.set), [1] (kdrag.solvers.egraph.EGraph method) Unit() (in module kdrag.theories.list), [1] (in module kdrag.theories.seq), [1] unsat_core() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

V

val_of_sort() (in module kdrag.hypothesis), [1] VampireSolver (class in kdrag.solvers) VampireTHFSolver (class in kdrag.solvers) Vec() (in module kdrag.theories.real.vec), [1] Vec0() (in module kdrag.theories.real.vec), [1] VerificationCondition (class in kdrag.contrib.pcode.asmspec)

verify() (kdrag.contrib.pcode.asmspec.VerificationCondition method) verilog_decl() (in module kdrag.printers.verilog), [1] verilog_of_expr() (in module kdrag.printers.verilog), [1] VerilogModule (class in kdrag.contrib.yosys) vs (kdrag.rewrite.RewriteRule attribute) (kdrag.rewrite.Rule attribute)

W

weaken_post() (kdrag.contrib.hoare.Hoare method) wf (in module kdrag.notation) when() (kdrag.notation.Cond method) wires (kdrag.contrib.yosys.SmtModInfo attribute) with_traceback() (kdrag.kernel.LemmaError method) (kdrag.rewrite.RewriteRuleException method) witness (kdrag.contrib.yosys.SmtModInfo attribute) wp() (in module kdrag.contrib.hoare), [1] wp_str() (in module kdrag.contrib.hoare), [1] wps() (in module kdrag.contrib.hoare), [1] write_smt() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

write_tptp() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) wsize (kdrag.contrib.yosys.SmtModInfo attribute)

X

x (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

Y

y (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

Z

z (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

z3_array_val() (in module kdrag.hypothesis), [1] z3_mid_rad_of_arb() (in module kdrag.theories.real.arb), [1] z3_of_exact_arb() (in module kdrag.theories.real.arb), [1] z3_to_egglog() (in module kdrag.solvers.egglog), [1] ZipperpositionSolver (class in kdrag.solvers)