Index

_

__call__() (kdrag.kernel.Proof method) (kdrag.notation.SortDispatch method) (kdrag.Proof method) __contains__() (kdrag.rewrite.Order class method) __enter__() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) __exit__() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method)

__getitem__() (kdrag.rewrite.Order class method) __hash__() (kdrag.utils.Zipper method) __iter__() (kdrag.rewrite.Order class method) __len__() (kdrag.rewrite.Order class method) __matmul__() (kdrag.contrib.hoare.Hoare method) __next__() (kdrag.utils.Zipper 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) AbelSemiGroup (class in kdrag.theories.algebra.group) 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 (class in kdrag.theories.real) add (in module kdrag.notation) (kdrag.theories.algebra.AddSemigroup attribute) (kdrag.theories.algebra.CommAddSemigroup attribute) 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_assert() (kdrag.contrib.pcode.asmspec.AsmSpec method) (kdrag.contrib.pcode.asmspec.Debug method) add_assign() (kdrag.contrib.pcode.asmspec.AsmSpec method) (kdrag.contrib.pcode.asmspec.Debug method) add_assoc (kdrag.theories.algebra.AddSemigroup attribute) (kdrag.theories.algebra.CommAddSemigroup attribute) (kdrag.theories.algebra.vector.VectorSpace attribute) add_assume() (kdrag.contrib.pcode.asmspec.AsmSpec method) add_comm (kdrag.theories.algebra.CommAddSemigroup attribute) (kdrag.theories.algebra.vector.VectorSpace attribute) add_cut() (kdrag.contrib.pcode.asmspec.AsmSpec method) (kdrag.contrib.pcode.asmspec.Debug method) add_entry() (kdrag.contrib.pcode.asmspec.AsmSpec method) (kdrag.contrib.pcode.asmspec.Debug method) add_exit() (kdrag.contrib.pcode.asmspec.AsmSpec method) (kdrag.contrib.pcode.asmspec.Debug method) add_inv (kdrag.theories.algebra.vector.VectorSpace attribute) add_lemma() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) add_note() (kdrag.kernel.LemmaError method) (kdrag.rewrite.RewriteRuleException method) add_term() (kdrag.solvers.egraph.EGraph method) add_zero (kdrag.theories.algebra.vector.VectorSpace attribute) AddAssoc (in module kdrag.theories.real) AddComm (in module kdrag.theories.real) AddId (in module kdrag.theories.real) 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) addr() (kdrag.contrib.pcode.asmspec.Debug method) addrmap (kdrag.contrib.pcode.asmspec.AsmSpec attribute) AddSemigroup (class in kdrag.theories.algebra) admit (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) admit() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState 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) Alloc() (kdrag.theories.logic.sep.Sep method) 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) Always() (in module kdrag.theories.logic.temporal), [1]

And() (in module kdrag.theories.logic.intuitionistic), [1] (in module kdrag.theories.logic.temporal), [1] (kdrag.theories.logic.sep.Sep method) and_ (in module kdrag.notation) andI() (in module kdrag.kernel), [1] ann() (in module kdrag.tele), [1] annot (kdrag.tactics.LemmaCallback attribute) antipattern() (in module kdrag.utils), [1] Antisymm (class in kdrag.property) antisymm (kdrag.property.Antisymm attribute) anyconsts (kdrag.contrib.yosys.SmtModInfo attribute) anyseqs (kdrag.contrib.yosys.SmtModInfo attribute) append() (kdrag.utils.ExprCtx method) apply() (in module kdrag.rewrite), [1] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState 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) (kdrag.utils.ExprCtx method) (kdrag.utils.Zipper 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.theories.algebra.group.AbelSemiGroup method) (kdrag.theories.algebra.group.Group method) (kdrag.theories.algebra.group.Monoid method) (kdrag.theories.algebra.group.Semigroup method) (kdrag.theories.algebra.lattice.SemiLattice method) (kdrag.theories.algebra.ordering.PreOrder method) (kdrag.theories.algebra.topology.Topology method) (kdrag.theories.algebra.vector.Normed method) (kdrag.theories.algebra.vector.VectorSpace method) assertion (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) asserts (kdrag.contrib.yosys.SmtModInfo attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) Assign (class in kdrag.contrib.pcode.asmspec) assign() (kdrag.contrib.hoare.Hoare class method) Assoc (class in kdrag.property) assoc (kdrag.property.Assoc attribute) (kdrag.theories.algebra.group.Semigroup attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) Assume (class in kdrag.contrib.pcode.asmspec) assumes (kdrag.contrib.yosys.SmtModInfo attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) assumes() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) assumption() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) ast_size_sexpr() (in module kdrag.utils), [1] AstRef (class in kdrag.contrib.expr) Asymm (class in kdrag.property) asymm (kdrag.property.Asymm attribute) auto() (in module kdrag.tactics), [1] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) ax (kdrag.kernel.Defn attribute) axiom() (in module kdrag) (in module kdrag.kernel), [1] axiom_sig() (in module kdrag.tele), [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] Ball() (in module kdrag.theories.real.analysis), [1] BaseSolver (class in kdrag.solvers) basic() (in module kdrag.solvers.kb), [1] beta() (in module kdrag.rewrite), [1] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) beta_conv() (in module kdrag.theories.logic.axioms), [1] BigUnion() (in module kdrag.theories.set), [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) Bool() (in module kdrag.theories.logic.temporal), [1] Bools() (in module kdrag.theories.logic.temporal), [1] 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] Box() (in module kdrag.modal), [1] breakpoint() (kdrag.contrib.pcode.asmspec.Debug method) BVNot() (in module kdrag.theories.bitvec), [1] bysect() (in module kdrag.utils), [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 (in module kdrag.notation) call_dict (in module kdrag.datatype) call_yosys_functional() (in module kdrag.contrib.yosys), [1] case() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) cases() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) cauchy_mod (in module kdrag.theories.real.seq) 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) (kdrag.theories.algebra.group.AbelSemiGroup method) (kdrag.theories.algebra.group.Group method) (kdrag.theories.algebra.group.Monoid method) (kdrag.theories.algebra.group.Semigroup method) (kdrag.theories.algebra.lattice.SemiLattice method) (kdrag.theories.algebra.ordering.PreOrder method) (kdrag.theories.algebra.topology.Topology method) (kdrag.theories.algebra.vector.Normed method) (kdrag.theories.algebra.vector.VectorSpace method) check_semigroup() (in module kdrag.theories.algebra), [1] 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) (kdrag.utils.ExprCtx method) choose (in module kdrag.notation) Choose() (in module kdrag.theories.set), [1] clear() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) (kdrag.utils.ExprCtx method)

clocks (kdrag.contrib.yosys.SmtModInfo attribute) cmds (kdrag.contrib.hoare.Hoare attribute) codomain() (in module kdrag.smt), [1] coerce() (in module kdrag.modal), [1] collect_decls() (in module kdrag.solvers), [1] collect_sorts() (in module kdrag.solvers), [1] Comm (class in kdrag.property) comm (kdrag.property.Comm attribute) (kdrag.theories.algebra.group.AbelSemiGroup attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) CommAddSemigroup (class in kdrag.theories.algebra) CommSemigroup (class in kdrag.theories.algebra) 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] cong() (in module kdrag.theories.logic.axioms), [1] Cons() (in module kdrag.theories.seq), [1] consider() (in module kdrag.theories.logic.axioms), [1] Const() (in module kdrag.contrib.expr), [1] (in module kdrag.smt), [1] (in module kdrag.theories.logic.intuitionistic), [1] (kdrag.contrib.pcode.MemState class method) constructor_num() (in module kdrag.datatype), [1] Consts() (in module kdrag.contrib.expr), [1] (in module kdrag.smt), [1] consts() (in module kdrag.utils), [1] Context (class in kdrag.contrib.expr) contra() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) copy() (kdrag.solvers.egraph.EGraph method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) (kdrag.utils.ExprCtx method) (kdrag.utils.Zipper 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) (kdrag.utils.ExprCtx method) counter (kdrag.contrib.expr.Context attribute) countermodel() (kdrag.contrib.pcode.asmspec.VerificationCondition method) CountInter() (in module kdrag.theories.set), [1] 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) (kdrag.utils.Zipper 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] Debug (class in kdrag.contrib.pcode.asmspec) decl (kdrag.kernel.Defn attribute) 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) DeclareFunction() (in module kdrag.tele), [1] DeclareSort() (in module kdrag.smt), [1] DeclHole (class in kdrag.utils) 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] (in module kdrag.tele), [1] (kdrag.notation.SortDispatch method) (kdrag.tele.ProgramState method) define_fix() (in module kdrag.kernel), [1] define_fun() (in module kdrag.datatype), [1] define_primrec() (in module kdrag.datatype), [1] defined_decls() (in module kdrag.utils), [1] Defn (class in kdrag.kernel) defns (in module kdrag.kernel) diff() (in module kdrag.solvers.sympy), [1] (in module kdrag.theories.set), [1] diff_shim() (in module kdrag.solvers.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) domains() (in module kdrag.smt), [1] dot() (kdrag.solvers.egraph.EGraph method)

E

e (kdrag.property.Identity attribute) (kdrag.property.LeftIdentity attribute) (kdrag.property.RightIdentity attribute) (kdrag.theories.algebra.group.Monoid attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) EClass() (in module kdrag.theories.set), [1] eclasses() (kdrag.solvers.egraph.EGraph method) EgglogSolver (class in kdrag.solvers.egglog) EGraph (class in kdrag.solvers.egraph) 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] Eq() (in module kdrag.theories.logic.temporal), [1] eq() (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.tactics.Calc method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) eqrefl() (in module kdrag.theories.logic.axioms), [1] eqsym() (in module kdrag.theories.logic.axioms), [1] eqtrans() (in module kdrag.theories.logic.axioms), [1] esimp() (in module kdrag.rewrite), [1] eval() (kdrag.contrib.pcode.asmspec.Debug method) eval_() (in module kdrag.reflect), [1] Eventually() (in module kdrag.theories.logic.temporal), [1] exact() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) execute1() (kdrag.contrib.pcode.BinaryContext method) execute1_schema() (kdrag.contrib.pcode.BinaryContext method) execute_insn() (in module kdrag.contrib.pcode.asmspec), [1] execute_spec_and_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] executeZeroExtend() (in module kdrag.contrib.pcode), [1] exists (in module kdrag.notation) Exists() (in module kdrag.smt), [1] exists() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) exists_cong() (in module kdrag.theories.logic.axioms), [1] ExistsHole (class in kdrag.utils) 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.solvers.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] ExprCtx (class in kdrag.utils) ExprRef (class in kdrag.contrib.expr) ext() (in module kdrag.kernel), [1] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) extend() (kdrag.utils.ExprCtx method) extract() (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.egraph.EGraph method)

F

f (kdrag.property.Assoc attribute) (kdrag.property.Comm attribute) (kdrag.property.Idem attribute) (kdrag.property.Identity attribute) (kdrag.property.LeftIdentity attribute) (kdrag.property.RightIdentity attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) (kdrag.utils.DeclHole attribute) F() (in module kdrag.theories.logic.temporal), [1] factor() (in module kdrag.solvers.sympy), [1] failures (kdrag.contrib.pcode.asmspec.Results attribute) fallthruOp() (kdrag.contrib.pcode.BinaryContext method) FamilyUnion() (in module kdrag.theories.set), [1] Filter() (in module kdrag.theories.algebra.filter), [1] FilterMod (class in kdrag.theories.algebra.filter) Fin() (in module kdrag.tele), [1] find() (kdrag.solvers.egraph.EGraph method) find_calls() (in module kdrag.utils), [1] Finite() (in module kdrag.theories.set), [1] FinSet() (in module kdrag.theories.logic.zf), [1] finsize() (in module kdrag.printers), [1] FinSort() (in module kdrag.theories.real.vec), [1] fix() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) FixedSort() (in module kdrag.theories.fixed), [1] fixes() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) flint_bnd() (in module kdrag.theories.real.arb), [1] flint_eq_ax_unsafe() (in module kdrag.theories.real.arb), [1] forall (in module kdrag.notation)

ForAll() (in module kdrag.smt), [1] forall() (kdrag.kernel.Proof method) (kdrag.Proof method) forall_cong() (in module kdrag.theories.logic.axioms), [1] ForAllHole (class in kdrag.utils) ForAllI() (in module kdrag.tactics), [1] forallI() (in module kdrag.tactics), [1] forget() (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.solvers.sympy), [1] FreshConst() (in module kdrag.contrib.expr), [1] freshen() (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) FreshVar() (in module kdrag) (in module kdrag.kernel), [1] (in module kdrag.tactics), [1] FreshVars() (in module kdrag) (in module kdrag.tactics), [1] from_expr() (kdrag.rewrite.RewriteRule class method) from_file() (kdrag.contrib.yosys.VerilogModule class method) (kdrag.contrib.yosys.VerilogModuleRel class method) from_term() (kdrag.utils.Zipper 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

G() (in module kdrag.theories.logic.temporal), [1] 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.tactics.ProofState method) (kdrag.tele.ProgramState method) generate() (in module kdrag.utils), [1] GenericDispatch() (in module kdrag.notation), [1] get() (in module kdrag.theories.option), [1] 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.tactics.ProofState method) (kdrag.tele.ProgramState method) get_proof() (kdrag.solvers.egraph.EGraph method) get_reg() (kdrag.contrib.pcode.BinaryContext method) get_registry() (kdrag.theories.algebra.group.AbelSemiGroup class method) (kdrag.theories.algebra.group.Group class method) (kdrag.theories.algebra.group.Monoid class method) (kdrag.theories.algebra.group.Semigroup class method) (kdrag.theories.algebra.lattice.SemiLattice class method) (kdrag.theories.algebra.ordering.PreOrder class method) (kdrag.theories.algebra.topology.Topology class method) (kdrag.theories.algebra.vector.Normed class method) (kdrag.theories.algebra.vector.VectorSpace 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() (kdrag.contrib.pcode.asmspec.Debug 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) Group (class in kdrag.theories.algebra) (class in kdrag.theories.algebra.group) gt (in module kdrag.notation) gt() (kdrag.Calc method) (kdrag.tactics.Calc method)

H

has_left() (kdrag.utils.DeclHole method) has_right() (kdrag.utils.DeclHole method) (kdrag.utils.ExistsHole method) (kdrag.utils.ForAllHole method) (kdrag.utils.LambdaHole method) (kdrag.utils.QuantifierHole method) has_type() (in module kdrag.tele), [1] HasType() (in module kdrag.tele), [1]

have() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) Head() (in module kdrag.theories.seq), [1] herb() (in module kdrag.kernel), [1] Hoare (class in kdrag.contrib.hoare) horn_trig() (in module kdrag.rewrite), [1] huet() (in module kdrag.solvers.kb), [1] huet_smt2_file() (in module kdrag.solvers.kb), [1] hyp (kdrag.rewrite.Rule attribute)

I

Id() (in module kdrag.tele), [1] id_left (kdrag.theories.algebra.group.Monoid attribute) id_right (kdrag.theories.algebra.group.Monoid attribute) Idem (class in kdrag.property) idem (kdrag.property.Idem attribute) (kdrag.theories.algebra.lattice.SemiLattice attribute) Identity (class in kdrag.property) If() (in module kdrag.theories.logic.temporal), [1] Implies() (in module kdrag.theories.logic.intuitionistic), [1] (in module kdrag.theories.logic.temporal), [1] (kdrag.theories.logic.sep.Sep method) 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) (kdrag.utils.ExprCtx method) induct (in module kdrag.notation) induct() (in module kdrag.theories.int), [1] (in module kdrag.theories.logic.peano), [1] (in module kdrag.theories.seq), [1] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState 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 (kdrag.contrib.yosys.VerilogModuleRel attribute) init_constrs (kdrag.contrib.yosys.VerilogModule attribute) init_mem() (kdrag.contrib.pcode.BinaryContext method) init_proj() (in module kdrag.printers.rust), [1] init_trace_states() (in module kdrag.contrib.pcode.asmspec), [1] init_unconstr (kdrag.contrib.yosys.VerilogModuleRel attribute) 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) insert() (kdrag.utils.ExprCtx method) insn() (kdrag.contrib.pcode.asmspec.Debug method) install_solvers() (in module kdrag.solvers), [1] install_solvers2() (in module kdrag.solvers), [1]

instan() (in module kdrag.kernel), [1] Int() (in module kdrag.theories.logic.temporal), [1] integ_shim() (in module kdrag.solvers.sympy), [1] integrate() (in module kdrag.solvers.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.tactics.ProofState method) (kdrag.tele.ProgramState method) Ints() (in module kdrag.theories.logic.temporal), [1] IntSort() (in module kdrag.smt), [1] inv (kdrag.theories.algebra.Group attribute) (kdrag.theories.algebra.group.Group attribute) inv_left (kdrag.theories.algebra.group.Group attribute) inv_right (kdrag.theories.algebra.group.Group attribute) invert (in module kdrag.notation) Irrefl (class in kdrag.property) irrefl (kdrag.property.Irrefl attribute) 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_fresh_var() (in module kdrag.kernel), [1] is_func() (in module kdrag.smt), [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_set() (in module kdrag.theories.set), [1] is_strict_subterm() (in module kdrag.utils), [1] is_subterm() (in module kdrag.utils), [1] is_T() (in module kdrag.theories.logic.temporal), [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.solvers.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.yosys module kdrag.datatype module kdrag.hypothesis module kdrag.kernel module kdrag.modal module kdrag.notation module kdrag.parsers module kdrag.parsers.microlean module kdrag.parsers.sexp 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.llvm 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.solvers.sympy module kdrag.tactics module kdrag.tele module

kdrag.theories module kdrag.theories.algebra module kdrag.theories.algebra.category module kdrag.theories.algebra.filter module kdrag.theories.algebra.group module kdrag.theories.algebra.kleene module kdrag.theories.algebra.lattice module kdrag.theories.algebra.ordering module kdrag.theories.algebra.sqmatrix module kdrag.theories.algebra.topology module kdrag.theories.algebra.vector 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.logic module kdrag.theories.logic.axioms module kdrag.theories.logic.computable module kdrag.theories.logic.GAT module kdrag.theories.logic.intuitionistic module kdrag.theories.logic.nominal module kdrag.theories.logic.ordinal module kdrag.theories.logic.peano module kdrag.theories.logic.robinson module kdrag.theories.logic.sear module kdrag.theories.logic.sep module kdrag.theories.logic.temporal module kdrag.theories.logic.zf module kdrag.theories.nat module kdrag.theories.option module kdrag.theories.real module kdrag.theories.real.analysis 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.seq module kdrag.theories.real.vec module kdrag.theories.regex module kdrag.theories.seq module kdrag.theories.set module kdrag.theories.sexp module kdrag.utils module key (kdrag.theories.algebra.group.AbelSemiGroup attribute) (kdrag.theories.algebra.group.Semigroup attribute) (kdrag.theories.algebra.lattice.SemiLattice attribute) (kdrag.theories.algebra.ordering.PreOrder attribute) (kdrag.theories.algebra.topology.Topology attribute) (kdrag.theories.algebra.vector.Normed attribute) (kdrag.theories.algebra.vector.VectorSpace attribute) 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) label() (kdrag.contrib.pcode.asmspec.Debug method) lam (kdrag.reflect.KnuckleClosure attribute) lambda_cong() (in module kdrag.theories.logic.axioms), [1] LambdaHole (class in kdrag.utils) le (in module kdrag.notation) le() (kdrag.Calc method) (kdrag.tactics.Calc method) LeanSolver (class in kdrag.solvers) left() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) (kdrag.utils.DeclHole method) (kdrag.utils.Zipper method) left_id (kdrag.property.Identity attribute) (kdrag.property.LeftIdentity attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) LeftIdentity (class in kdrag.property) Lemma() (in module kdrag) (in module kdrag.tactics), [1] lemma_db() (in module kdrag.utils), [1]

LemmaCallback (class in kdrag.tactics) LemmaError LeoIIISolver (class in kdrag.solvers) less_le_not_le (kdrag.theories.algebra.ordering.PreOrder attribute) let() (kdrag.solvers.egglog.EgglogSolver method) lhs (kdrag.rewrite.RewriteRule attribute) Lift() (kdrag.theories.logic.sep.Sep method) lift_binop() (in module kdrag.theories.logic.temporal), [1] lift_unop() (in module kdrag.theories.logic.temporal), [1] limit() (in module kdrag.solvers.sympy), [1] link() (in module kdrag.printers.c), [1] List (class in kdrag.theories.list) ListSort() (in module kdrag.theories.list), [1] load() (kdrag.contrib.pcode.BinaryContext method) locals (kdrag.reflect.KnuckleClosure attribute) lookup() (kdrag.theories.algebra.group.AbelSemiGroup class method) (kdrag.theories.algebra.group.Group class method) (kdrag.theories.algebra.group.Monoid class method) (kdrag.theories.algebra.group.Semigroup class method) (kdrag.theories.algebra.lattice.SemiLattice class method) (kdrag.theories.algebra.ordering.PreOrder class method) (kdrag.theories.algebra.topology.Topology class method) (kdrag.theories.algebra.vector.Normed class method) (kdrag.theories.algebra.vector.VectorSpace 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] make_sep() (in module kdrag.theories.logic.sep), [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) Max() (in module kdrag.theories.real.interval), [1] maximize (kdrag.contrib.yosys.SmtModInfo attribute) measure (in module kdrag.notation) 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) MImplies() (in module kdrag.modal), [1] Min() (in module kdrag.theories.real.interval), [1] min_float64 (in module kdrag.theories.float) minimize (kdrag.contrib.yosys.SmtModInfo attribute) model() (kdrag.contrib.pcode.asmspec.Debug method) 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.yosys kdrag.datatype kdrag.hypothesis kdrag.kernel kdrag.modal kdrag.notation kdrag.parsers kdrag.parsers.microlean kdrag.parsers.sexp kdrag.parsers.smtlib kdrag.parsers.tptp kdrag.parsers.trs kdrag.printers kdrag.printers.c kdrag.printers.lean kdrag.printers.llvm 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.solvers.sympy kdrag.tactics kdrag.tele kdrag.theories kdrag.theories.algebra kdrag.theories.algebra.category kdrag.theories.algebra.filter kdrag.theories.algebra.group kdrag.theories.algebra.kleene kdrag.theories.algebra.lattice kdrag.theories.algebra.ordering kdrag.theories.algebra.sqmatrix kdrag.theories.algebra.topology kdrag.theories.algebra.vector kdrag.theories.bitvec kdrag.theories.bool kdrag.theories.fixed kdrag.theories.float kdrag.theories.fun kdrag.theories.int kdrag.theories.list kdrag.theories.logic kdrag.theories.logic.axioms kdrag.theories.logic.computable kdrag.theories.logic.GAT kdrag.theories.logic.intuitionistic kdrag.theories.logic.nominal kdrag.theories.logic.ordinal kdrag.theories.logic.peano kdrag.theories.logic.robinson kdrag.theories.logic.sear kdrag.theories.logic.sep kdrag.theories.logic.temporal kdrag.theories.logic.zf kdrag.theories.nat kdrag.theories.option kdrag.theories.real kdrag.theories.real.analysis 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.seq kdrag.theories.real.vec kdrag.theories.regex kdrag.theories.seq kdrag.theories.set kdrag.theories.sexp kdrag.utils

modus() (in module kdrag.kernel), [1] Monoid (class in kdrag.theories.algebra) (class in kdrag.theories.algebra.group) ms_order() (in module kdrag.solvers.kb.multiset), [1] mu (in module kdrag.theories.logic.computable) Mul (class in kdrag.theories.real) mul (in module kdrag.notation) (kdrag.theories.algebra.CommSemigroup attribute) (kdrag.theories.algebra.Group attribute) (kdrag.theories.algebra.Monoid attribute) (kdrag.theories.algebra.SemiGroup attribute) mul_assoc (kdrag.theories.algebra.CommSemigroup attribute) (kdrag.theories.algebra.Group attribute) (kdrag.theories.algebra.Monoid attribute) (kdrag.theories.algebra.SemiGroup attribute) mul_comm (kdrag.theories.algebra.CommSemigroup attribute) mul_left_inv (kdrag.theories.algebra.Group attribute) mul_one (kdrag.theories.algebra.Group attribute) (kdrag.theories.algebra.Monoid attribute) mul_right_inv (kdrag.theories.algebra.Group attribute) MulAssoc (in module kdrag.theories.real) multipattern_match() (in module kdrag.datatype), [1] MultiSolver (class in kdrag.solvers) MultiStore() (in module kdrag.theories.fun), [1]

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.contrib.yosys.VerilogModuleRel 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)

neg_ext() (in module kdrag.theories.logic.axioms), [1] NEq() (in module kdrag.theories.logic.temporal), [1] newgoal() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) NewType() (in module kdrag) (in module kdrag.datatype), [1] Next() (in module kdrag.theories.logic.temporal), [1] NGE (kdrag.rewrite.Order attribute) Nil() (in module kdrag.theories.seq), [1] no_overflow() (in module kdrag.theories.float), [1] None_() (in module kdrag.theories.option), [1] NoOverflow() (in module kdrag.theories.float), [1] norm (kdrag.theories.algebra.vector.Normed attribute) norm_homog (kdrag.theories.algebra.vector.Normed attribute) norm_nonneg (kdrag.theories.algebra.vector.Normed attribute) norm_triangle (kdrag.theories.algebra.vector.Normed attribute) norm_zero (kdrag.theories.algebra.vector.Normed attribute) normalize() (in module kdrag.tele), [1] Normed (class in kdrag.theories.algebra.vector) Not() (in module kdrag.theories.logic.intuitionistic), [1] (in module kdrag.theories.logic.temporal), [1] num_args() (in module kdrag.smt), [1] (kdrag.contrib.expr.ExprRef method)

O

obtain() (in module kdrag.kernel), [1] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) 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_list() (kdrag.theories.list.List method) of_sexp() (in module kdrag.theories.sexp), [1] of_sort() (in module kdrag.printers.lean), [1] (in module kdrag.printers.rust), [1] one (kdrag.theories.algebra.Group attribute) (kdrag.theories.algebra.Monoid attribute) one_mul (kdrag.theories.algebra.Group attribute) (kdrag.theories.algebra.Monoid attribute) open_binder() (in module kdrag.tactics), [1] (in module kdrag.tele), [1] (in module kdrag.utils), [1] (kdrag.utils.ExprCtx method) (kdrag.utils.Zipper method)

open_binder_unhygienic() (in module kdrag.utils), [1] open_Int (kdrag.theories.algebra.topology.Topology attribute) open_Union (kdrag.theories.algebra.topology.Topology attribute) open_UNIV (kdrag.theories.algebra.topology.Topology attribute) OptionSort() (in module kdrag.theories.option), [1] Or() (in module kdrag.theories.logic.intuitionistic), [1] (in module kdrag.theories.logic.temporal), [1] (kdrag.theories.logic.sep.Sep method) or_ (in module kdrag.notation) or_intro2 (in module kdrag.theories.logic.intuitionistic) Order (class in kdrag.rewrite) orient() (in module kdrag.solvers.kb), [1] orig_vs (kdrag.utils.ExistsHole attribute) (kdrag.utils.ForAllHole attribute) (kdrag.utils.LambdaHole attribute) (kdrag.utils.QuantifierHole attribute) otherwise() (kdrag.notation.Cond method) OutOfGas (class in kdrag.contrib.pcode.asmspec) 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

parse() (in module kdrag.parsers.microlean), [1] (in module kdrag.parsers.sexp), [1] (in module kdrag.theories.sexp), [1] path_cond (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) (kdrag.contrib.pcode.SimState attribute) pathmap() (in module kdrag.utils), [1] pattern_match() (in module kdrag.datatype), [1] pc (kdrag.contrib.pcode.SimState attribute) pc_of_addr() (in module kdrag.contrib.pcode), [1] PEq() (in module kdrag.modal), [1] perf_event() (in module kdrag.config), [1] pf (kdrag.rewrite.RewriteRule attribute) (kdrag.rewrite.Rule attribute) Pi() (in module kdrag.tele), [1] PIf() (in module kdrag.modal), [1] PImplies() (in module kdrag.modal), [1] pmatch() (in module kdrag.utils), [1] (kdrag.utils.Zipper method) pmatch_fo() (in module kdrag.utils), [1] pmatch_rec() (in module kdrag.utils), [1] pmatch_rec_ctx() (in module kdrag.utils), [1] PointEq() (in module kdrag.modal), [1] PointIf() (in module kdrag.modal), [1] pop() (kdrag.contrib.pcode.asmspec.Debug method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) (kdrag.utils.ExprCtx method) pop_goal() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) pop_lemma() (kdrag.contrib.pcode.asmspec.Debug method) pop_lemmas() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) pop_run() (kdrag.contrib.pcode.asmspec.Debug method) pop_verify() (kdrag.contrib.pcode.asmspec.Debug method) PopCount() (in module kdrag.theories.bitvec), [1] post (kdrag.contrib.hoare.Hoare attribute) powers (kdrag.theories.real.seq.Series attribute) PowerSet() (in module kdrag.theories.set), [1] pprint_sexp() (in module kdrag.parsers.sexp), [1] pprint_sexps() (in module kdrag.parsers.sexp), [1] 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) PreOrder (class in kdrag.theories.algebra.ordering) pretty_insn() (in module kdrag.contrib.pcode), [1] pretty_op() (in module kdrag.contrib.pcode), [1] pretty_trace() (in module kdrag.contrib.pcode.asmspec), [1] Program() (in module kdrag.tele), [1] ProgramState (class in kdrag.tele) proj() (in module kdrag.theories.logic.axioms), [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) (kdrag.tactics.Goal method) ProofState (class in kdrag.tactics) Prop (in module kdrag.theories.logic.intuitionistic) Prop() (kdrag.theories.logic.sep.Sep method) propagate() (in module kdrag.utils), [1] propagate_eqs() (in module kdrag.utils), [1] Props() (kdrag.theories.logic.sep.Sep method) prove() (in module kdrag) (in module kdrag.kernel), [1] (in module kdrag.solvers.ljt), [1] (in module kdrag.tactics), [1] prove_sig() (in module kdrag.tele), [1] prune() (in module kdrag.utils), [1] PTheorem() (in module kdrag) (in module kdrag.tactics), [1] Pto() (kdrag.theories.logic.sep.Sep method) push() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) push_lemmas() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method)

Q

qed() (kdrag.Calc method) (kdrag.tactics.Calc method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) QExists() (in module kdrag) (in module kdrag.notation), [1] qfix() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) qfixes() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) QForAll() (in module kdrag) (in module kdrag.notation), [1]

QImplies() (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] QuantifierHole (class in kdrag.utils) query() (kdrag.solvers.VampireSolver method) quickcheck() (in module kdrag.hypothesis), [1] Quot() (in module kdrag.theories.set), [1] Quote() (in module kdrag.theories.sexp), [1]

R

radd (in module kdrag.notation) ram() (kdrag.contrib.pcode.asmspec.Debug method) Range() (in module kdrag.theories.set), [1] range() (kdrag.contrib.expr.FuncDeclRef method) read (kdrag.contrib.pcode.MemState attribute) read_yosys_relational() (in module kdrag.contrib.yosys), [1] 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) (kdrag.utils.Zipper method) recognizer_lemmas() (in module kdrag.datatype), [1] Refl (class in kdrag.property) refl (kdrag.property.Refl attribute) (kdrag.theories.algebra.ordering.PreOrder attribute) reflect() (in module kdrag.reflect), [1] reg() (kdrag.contrib.pcode.asmspec.Debug method) register() (kdrag.notation.SortDispatch method) (kdrag.theories.algebra.group.AbelSemiGroup class method) (kdrag.theories.algebra.group.Group class method) (kdrag.theories.algebra.group.Monoid class method) (kdrag.theories.algebra.group.Semigroup class method) (kdrag.theories.algebra.lattice.SemiLattice class method) (kdrag.theories.algebra.ordering.PreOrder class method) (kdrag.theories.algebra.topology.Topology class method) (kdrag.theories.algebra.vector.Normed class method) (kdrag.theories.algebra.vector.VectorSpace class method) registers (kdrag.contrib.yosys.SmtModInfo attribute) reify() (in module kdrag.reflect), [1] rel (in module kdrag.datatype) (kdrag.property.Antisymm attribute) (kdrag.property.Asymm attribute) (kdrag.property.Irrefl attribute) (kdrag.property.Refl attribute) (kdrag.property.Total attribute) remove() (kdrag.utils.ExprCtx method) rename_vars() (in module kdrag.theories.logic.axioms), [1] rename_vars2() (in module kdrag.kernel), [1] repeat() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) 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) reverse() (kdrag.utils.ExprCtx method) revert() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) rewrite() (in module kdrag.rewrite), [1] (in module kdrag.solvers.kb.multiset), [1] (in module kdrag.solvers.kb.string), [1] 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.tactics.ProofState method) (kdrag.tele.ProgramState method) (kdrag.utils.DeclHole method) (kdrag.utils.Zipper method) right_id (kdrag.property.Identity attribute) (kdrag.property.RightIdentity attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) RightIdentity (class in kdrag.property) 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.contrib.pcode.asmspec.Debug method) (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] run_vc() (kdrag.contrib.pcode.asmspec.Debug method) rust_module_template() (in module kdrag.printers.rust), [1] rw() (kdrag.solvers.egraph.EGraph method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) rw_trig() (in module kdrag.rewrite), [1]

S

sanity_check_consistency() (in module kdrag.utils), [1] SATSolver (class in kdrag.solvers) scalar (kdrag.theories.algebra.vector.VectorSpace attribute) search() (in module kdrag) (in module kdrag.utils), [1] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) search_decl() (in module kdrag.utils), [1] search_expr() (in module kdrag.utils), [1] select_concat() (in module kdrag.theories.bitvec), [1] SelectConcat() (in module kdrag.theories.bitvec), [1] SemiGroup (class in kdrag.theories.algebra) Semigroup (class in kdrag.theories.algebra.group) SemiLattice (class in kdrag.theories.algebra.lattice) Sep (class in kdrag.theories.logic.sep) Sep() (kdrag.theories.logic.sep.Sep method) Seq() (in module kdrag.theories.seq), [1] seq() (in module kdrag.theories.seq), [1] Series (class in kdrag.theories.real.seq) series() (in module kdrag.solvers.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.solvers.sympy), [1] shortlex() (in module kdrag.solvers.kb.multiset), [1] shortlex_swap() (in module kdrag.solvers.kb.string), [1] show() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) sig (kdrag.tactics.Goal attribute) simp() (in module kdrag) (in module kdrag.rewrite), [1] (in module kdrag.solvers.sympy), [1] (in module kdrag.tactics), [1] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState 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.solvers.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] Singleton() (in module kdrag.theories.set), [1] skip() (kdrag.contrib.hoare.Hoare class method) skolem() (in module kdrag.tactics), [1] slemma() (in module kdrag.theories.logic.zf), [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) smul (kdrag.theories.algebra.vector.VectorSpace attribute) smul_assoc (kdrag.theories.algebra.vector.VectorSpace attribute) smul_distrib (kdrag.theories.algebra.vector.VectorSpace attribute) solve() (in module kdrag.solvers.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() (in module kdrag.theories.logic.intuitionistic), [1] sort() (kdrag.utils.ExprCtx method) 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] spec_file() (kdrag.contrib.pcode.asmspec.Debug method) specialize() (in module kdrag.kernel), [1] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) split() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState 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) start() (kdrag.contrib.pcode.asmspec.Debug method) state (kdrag.contrib.pcode.asmspec.TraceState attribute) state_sort (kdrag.contrib.yosys.VerilogModule attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) step() (kdrag.contrib.pcode.asmspec.Debug method) store_view() (in module kdrag.theories.fun), [1] 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] (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) sublemma() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) subseq() (in module kdrag.solvers.kb.string), [1] subset() (in module kdrag.theories.set), [1] subsort_domain() (in module kdrag.tele), [1] subst() (in module kdrag.kernel), [1] (in module kdrag.tactics), [1] substitute() (in module kdrag.contrib.pcode.asmspec), [1] (kdrag.contrib.pcode.BinaryContext method) substitute_fresh_vars() (in module kdrag.theories.logic.axioms), [1] substitute_ghost() (in module kdrag.contrib.pcode.asmspec), [1] subterms() (in module kdrag.utils), [1] successes (kdrag.contrib.pcode.asmspec.Results attribute) sum_shim() (in module kdrag.solvers.sympy), [1] summation() (in module kdrag.solvers.sympy), [1] Surjective() (in module kdrag.theories.set), [1] sym_execute() (kdrag.contrib.pcode.BinaryContext method) symm() (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) sympify() (in module kdrag.solvers.sympy), [1]

T

t (kdrag.utils.Zipper attribute) Tail() (in module kdrag.theories.seq), [1] 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] (in module kdrag.theories.logic.nominal), [1] (in module kdrag.theories.logic.zf), [1] (in module kdrag.theories.real.interval), [1] (in module kdrag.theories.real.seq), [1] test_pcode() (in module kdrag.contrib.pcode), [1] TExists() (in module kdrag.tele), [1] TForAll() (in module kdrag.tele), [1] then() (kdrag.notation.Cond method) Theorem() (in module kdrag) (in module kdrag.tactics), [1] thm (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) TLift() (in module kdrag.theories.logic.temporal), [1] to_expr() (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.tactics.Goal 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.tactics.ProofState method) (kdrag.tele.ProgramState method) Topology (class in kdrag.theories.algebra.topology) Total (class in kdrag.property) total (kdrag.property.Total attribute) tptp2smt() (in module kdrag.solvers), [1] trace (kdrag.contrib.pcode.asmspec.TraceState attribute) (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) trace_id (kdrag.contrib.pcode.asmspec.TraceState attribute) TraceState (class in kdrag.contrib.pcode.asmspec) trans (kdrag.contrib.yosys.VerilogModuleRel attribute) (kdrag.theories.algebra.ordering.PreOrder attribute) trans_fun (kdrag.contrib.yosys.VerilogModule attribute) translate() (kdrag.contrib.pcode.BinaryContext method) translate_tuple_args() (in module kdrag.solvers.sympy), [1] Truth() (in module kdrag.theories.sexp), [1] TSort() (in module kdrag.theories.logic.temporal), [1] TweeSolver (class in kdrag.solvers) type_of_sort() (in module kdrag.reflect), [1] TypeVarRef (class in kdrag.contrib.expr)

U

uf (kdrag.solvers.egraph.EGraph attribute) UNCHANGED() (in module kdrag.theories.logic.temporal), [1] UnConcat() (in module kdrag.theories.bitvec), [1] unfold() (in module kdrag.kernel), [1] (in module kdrag.rewrite), [1] (in module kdrag.theories.logic.axioms), [1] (kdrag.contrib.pcode.BinaryContext method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState 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.seq), [1]

Unquote() (in module kdrag.theories.sexp), [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) up() (kdrag.utils.Zipper method) update_write() (in module kdrag.contrib.pcode.asmspec), [1]

V

val_of_sort() (in module kdrag.hypothesis), [1] Valid() (in module kdrag.modal), [1] (in module kdrag.theories.logic.intuitionistic), [1] (in module kdrag.theories.logic.temporal), [1] (kdrag.theories.logic.sep.Sep method) VampireSolver (class in kdrag.solvers) VampireTHFSolver (class in kdrag.solvers) vc() (kdrag.contrib.pcode.asmspec.VerificationCondition method) Vec() (in module kdrag.theories.real.vec), [1] Vec0() (in module kdrag.theories.real.vec), [1] VectorSpace (class in kdrag.theories.algebra.vector) 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) VerilogModuleRel (class in kdrag.contrib.yosys) vmap() (in module kdrag.theories.bitvec), [1] vs (kdrag.rewrite.RewriteRule attribute) (kdrag.rewrite.Rule attribute) (kdrag.utils.ExistsHole attribute) (kdrag.utils.ForAllHole attribute) (kdrag.utils.LambdaHole attribute) (kdrag.utils.QuantifierHole attribute)

W

Wand() (kdrag.theories.logic.sep.Sep method) weaken_post() (kdrag.contrib.hoare.Hoare method) wf (in module kdrag.notation) when() (kdrag.notation.Cond method) wires (kdrag.contrib.yosys.SmtModInfo attribute) (kdrag.contrib.yosys.VerilogModuleRel 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] wrap() (kdrag.utils.DeclHole method) (kdrag.utils.ExistsHole method) (kdrag.utils.ExprCtx method) (kdrag.utils.ForAllHole method) (kdrag.utils.LambdaHole method) write (kdrag.contrib.pcode.MemState attribute) 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)

X() (in module kdrag.theories.logic.temporal), [1]

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] zero (kdrag.theories.algebra.vector.VectorSpace attribute) zero_add (in module kdrag.theories.algebra.vector) Zipper (class in kdrag.utils) ZipperpositionSolver (class in kdrag.solvers)