Index

_

__call__() (kdrag.kernel.Proof method) (kdrag.notation.SortDispatch method) (kdrag.Proof method) __contains__() (kdrag.contrib.expr.Kind class method) (kdrag.rewrite.Order class method) __enter__() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) __exit__() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method)

__getitem__() (kdrag.contrib.expr.Kind class method) (kdrag.rewrite.Order class method) __hash__() (kdrag.utils.Zipper method) __iter__() (kdrag.contrib.expr.Kind class method) (kdrag.rewrite.Order class method) __len__() (kdrag.contrib.expr.Kind class method) (kdrag.rewrite.Order class method) __matmul__() (kdrag.contrib.hoare.Hoare method) __next__() (kdrag.utils.Zipper method)

A

a (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverSolver 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) AbelSemiGroup() (in module kdrag) 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.EProverSolver 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.contrib.pcode.asmspec.VCProofState method) (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.contrib.pcode.asmspec.VCProofState method) (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) Antisymm() (in module kdrag) anyconsts (kdrag.contrib.yosys.SmtModInfo attribute) anyseqs (kdrag.contrib.yosys.SmtModInfo attribute) APP (kdrag.contrib.expr.Kind attribute) append() (kdrag.utils.ExprCtx method) apply() (in module kdrag.rewrite), [1] (kdrag.contrib.pcode.asmspec.VCProofState method) (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) asize (kdrag.contrib.yosys.SmtModInfo attribute) AsmProof (class in kdrag.contrib.pcode.asmspec) AsmProofState (class in kdrag.contrib.pcode.asmspec) 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.EProverSolver 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) Assoc() (in module kdrag) Assume (class in kdrag.contrib.pcode.asmspec) assumes (kdrag.contrib.yosys.SmtModInfo attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) assumes() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) assumption() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) ast (kdrag.contrib.expr.AstRef attribute) (kdrag.contrib.expr.ExprRef attribute) (kdrag.contrib.expr.FuncDeclRef attribute) (kdrag.contrib.expr.SortRef attribute) ast_size_sexpr() (in module kdrag.utils), [1] AstNode (class in kdrag.contrib.expr) astptr() (in module kdrag.contrib.fast), [1] AstRef (class in kdrag.contrib.expr) Asymm (class in kdrag.property) asymm (kdrag.property.Asymm attribute) auto() (in module kdrag.tactics), [1] (kdrag.contrib.pcode.asmspec.AsmProofState method) (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) ax (kdrag.kernel.Defn attribute) axiom() (in module kdrag) (in module kdrag.kernel), [1] (in module kdrag.parsers.microlean), [1] axiom_sig() (in module kdrag.tele), [1]

B

b (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverSolver 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) backtrack() (kdrag.solvers.sat.DPLLSolver method) 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.contrib.pcode.asmspec.VCProofState method) (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)

binder() (in module kdrag.parsers.microlean), [1] binders() (in module kdrag.parsers.microlean), [1] binop() (in module kdrag.hypothesis), [1] binops() (in module kdrag.hypothesis), [1] binpath() (in module kdrag.solvers), [1] bits (kdrag.contrib.pcode.CachedArray attribute) (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] (kdrag.contrib.expr.Context method) BoolStmt (class in kdrag.contrib.pcode.asmspec) BoolVal() (kdrag.contrib.expr.Context method) 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] box() (in module kdrag.theories.univ), [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.EProverSolver 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] cache (kdrag.contrib.pcode.CachedArray attribute) CachedArray (class in kdrag.contrib.pcode) 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] calling_globals_locals() (in module kdrag.utils), [1] case() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) cases() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) cast() (in module kdrag.cast), [1] (in module kdrag.theories.univ), [1] cast_dt() (in module kdrag.cast), [1] 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.EProverSolver 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.sat.DPLLSolver 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.EProverSolver 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.AstNode attribute) children() (kdrag.contrib.expr.ExprRef method) (kdrag.utils.ExprCtx method) choose (in module kdrag.notation) Choose() (in module kdrag.theories.set), [1] clauses (kdrag.solvers.sat.DPLLSolver attribute) clear() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) (kdrag.utils.ExprCtx method) clocks (kdrag.contrib.yosys.SmtModInfo attribute)

Closed() (in module kdrag.theories.set), [1] 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) Comm() (in module kdrag) CommAddSemigroup (class in kdrag.theories.algebra) CommMonoid() (in module kdrag) CommSemigroup (class in kdrag.theories.algebra) CommSemiRing() (in module kdrag) 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] (in module kdrag.notation), [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.smt), [1] (in module kdrag.theories.logic.intuitionistic), [1] (kdrag.contrib.expr.Context method) (kdrag.contrib.pcode.MemState class method) constructor_num() (in module kdrag.datatype), [1] Consts() (in module kdrag.smt), [1] consts() (in module kdrag.utils), [1] Consts() (kdrag.contrib.expr.Context method) Context (class in kdrag.contrib.expr) contra() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) copy() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.parsers.microlean.Env method) (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.expr.AstNode method) (kdrag.contrib.pcode.asmspec.VerificationCondition method) (kdrag.contrib.pcode.CachedArray method) (kdrag.contrib.pcode.MemState method) (kdrag.parsers.microlean.Env method) (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.solvers.sat.GroundClause 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) create() (kdrag.contrib.expr.AstNode static method) 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.pcode.asmspec.AsmSpec attribute) (kdrag.tactics.Goal attribute) (kdrag.utils.Zipper attribute) ctxptr() (in module kdrag.contrib.fast), [1] ctype_of_sort() (in module kdrag.printers.c), [1] curry_arrays() (in module kdrag.utils), [1] Cut (class in kdrag.contrib.pcode.asmspec)

D

data (kdrag.contrib.pcode.CachedArray attribute) 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) decide() (kdrag.solvers.sat.DPLLSolver method) DECL (kdrag.contrib.expr.Kind attribute) 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] (kdrag.contrib.expr.Context method) 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.parsers.microlean), [1] (in module kdrag.tele), [1] (kdrag.notation.SortDispatch method) (kdrag.tele.ProgramState method) define_const() (in module kdrag) 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) download() (in module kdrag.solvers), [1] DPLLSolver (class in kdrag.solvers.sat)

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) EGraph (class in kdrag.solvers.egraph) ematch() (kdrag.solvers.egraph.EGraph method) empty() (kdrag.tactics.Goal class method) emt() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) Entry (class in kdrag.contrib.pcode.asmspec) Enum() (in module kdrag.datatype), [1] Env (class in kdrag.parsers.microlean) EProverSolver (class in kdrag.solvers) 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.pcode.asmspec.VCProofState 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] eunify() (in module kdrag.utils), [1] eval() (kdrag.contrib.pcode.asmspec.Debug method) eval_() (in module kdrag.reflect), [1] eval_lit() (kdrag.solvers.sat.DPLLSolver method) Eventually() (in module kdrag.theories.logic.temporal), [1] exact() (kdrag.contrib.pcode.asmspec.AsmProofState method) (kdrag.contrib.pcode.asmspec.VCProofState method) (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.contrib.pcode.asmspec.VCProofState method) (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.parsers.microlean), [1] (in module kdrag.reflect), [1] (kdrag.notation.Cond method) expr_kind() (in module kdrag.smt), [1] expr_to_cnf() (in module kdrag.printers.tptp), [1] expr_to_smtlib() (in module kdrag.printers.smtlib), [1] expr_to_tptp() (in module kdrag.printers.tptp), [1] ExprCtx (class in kdrag.utils) ExprRef (class in kdrag.contrib.expr) ext() (in module kdrag.kernel), [1] (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) extend() (kdrag.utils.ExprCtx method) extract() (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] find_label() (kdrag.contrib.pcode.asmspec.AsmSpec method) 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.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) FixedSort() (in module kdrag.theories.fixed), [1] fixes() (kdrag.contrib.pcode.asmspec.VCProofState method) (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() (kdrag.contrib.expr.Context method) 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.printers.smtlib), [1] FuncDeclRef (class in kdrag.contrib.expr) Function() (in module kdrag.smt), [1] (kdrag.contrib.expr.Context method)

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.contrib.pcode.asmspec.VCProofState method) (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) get_lemma() (kdrag.contrib.pcode.asmspec.VCProofState method) (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.parsers.microlean.Env attribute) (kdrag.reflect.KnuckleClosure attribute) Goal (class in kdrag.tactics) goal (kdrag.tactics.Goal attribute) GR (kdrag.rewrite.Order attribute) GroundClause (class in kdrag.solvers.sat) 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] hash (kdrag.contrib.expr.AstNode attribute) hashcons() (kdrag.contrib.expr.Context method) HasType() (in module kdrag.tele), [1]

have() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) Head() (in module kdrag) 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) (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) Idem() (in module kdrag) 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.expr.AstNode method) (kdrag.contrib.pcode.asmspec.VerificationCondition method) (kdrag.contrib.pcode.CachedArray method) (kdrag.contrib.pcode.MemState method) (kdrag.parsers.microlean.Env method) (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.solvers.sat.GroundClause method) (kdrag.tactics.Goal method) (kdrag.utils.ExprCtx method) induct (in module kdrag.notation) induct() (in module kdrag.theories.logic.peano), [1] (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) induct_default() (in module kdrag.notation), [1] induct_inductive() (in module kdrag.kernel), [1] induct_int() (in module kdrag.notation), [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] induct_seq() (in module kdrag.notation), [1] Inductive() (in module kdrag) (in module kdrag.kernel), [1] inductive() (in module kdrag.parsers.microlean), [1] inductive_of_tree() (in module kdrag.parsers.microlean), [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] (in module kdrag.theories.univ), [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] intify() (in module kdrag.contrib.fast), [1] intros() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) Ints() (in module kdrag.theories.logic.temporal), [1] IntSort() (in module kdrag.smt), [1] (kdrag.contrib.expr.Context method) IntVal() (kdrag.contrib.expr.Context method) 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_conflict() (kdrag.solvers.sat.DPLLSolver method) 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_sat() (kdrag.solvers.sat.DPLLSolver method) 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] is_wf() (in module kdrag.smt), [1] IsFinite() (in module kdrag.theories.float), [1] ite() (kdrag.contrib.hoare.Hoare class method) iter() (kdrag.solvers.egraph.EGraph method)

J

json() (kdrag.contrib.pcode.asmspec.AsmSpec method)

Judgement (class in kdrag.kernel)

K

k (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverSolver 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.cast module kdrag.config module kdrag.contrib module kdrag.contrib.cpp module kdrag.contrib.data_modulo module kdrag.contrib.expr module kdrag.contrib.fast 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.smtlib module kdrag.printers.tptp 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.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.sat 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.theories.univ 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 (class in kdrag.contrib.expr) kind (kdrag.contrib.expr.AstNode attribute) 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] lambda_lift() (in module kdrag.utils), [1] LambdaHole (class in kdrag.utils) le (in module kdrag.notation) (kdrag.contrib.pcode.CachedArray attribute) le() (kdrag.Calc method) (kdrag.tactics.Calc method) lean() (in module kdrag.parsers.microlean), [1] LeanSolver (class in kdrag.solvers) left() (kdrag.contrib.pcode.asmspec.VCProofState method) (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) LeftIdentity() (in module kdrag) Lemma() (in module kdrag) (in module kdrag.tactics), [1]

lemma() (kdrag.contrib.pcode.asmspec.AsmProofState method) 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) 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) list() (in module kdrag) ListSort() (in module kdrag) load() (kdrag.contrib.pcode.BinaryContext method) locals (kdrag.parsers.microlean.Env attribute) (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.EProverSolver 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] makevar() (kdrag.solvers.sat.DPLLSolver method) mangle_decl() (in module kdrag.printers.tptp), [1] mangle_decl_smtlib() (in module kdrag.printers.smtlib), [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) 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) MemStateSort (in module kdrag.contrib.pcode) 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) (kdrag.solvers.sat.DPLLSolver method) model_registers() (kdrag.contrib.pcode.BinaryContext method) module kdrag kdrag.all kdrag.cast kdrag.config kdrag.contrib kdrag.contrib.cpp kdrag.contrib.data_modulo kdrag.contrib.expr kdrag.contrib.fast 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.smtlib kdrag.printers.tptp kdrag.printers.verilog kdrag.property kdrag.reflect kdrag.rewrite kdrag.smt kdrag.solvers kdrag.solvers.aprove kdrag.solvers.datalog 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.sat 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.theories.univ kdrag.utils

modus() (in module kdrag.kernel), [1] Monoid (class in kdrag.theories.algebra) (class in kdrag.theories.algebra.group) Monoid() (in module kdrag) 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.EProverSolver 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) namedtuple_of_constructor() (in module kdrag.reflect), [1] NanoCopISolver (class in kdrag.solvers) NatSort() (in module kdrag) nbe() (in module kdrag.reflect), [1] ne (in module kdrag.notation) neg (in module kdrag.notation) (in module kdrag.theories.univ) (kdrag.solvers.sat.GroundClause attribute)

neg_ext() (in module kdrag.theories.logic.axioms), [1] NEq() (in module kdrag.theories.logic.temporal), [1] newgoal() (kdrag.contrib.pcode.asmspec.VCProofState method) (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]

O

obtain() (in module kdrag.kernel), [1] (kdrag.contrib.pcode.asmspec.VCProofState method) (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] (kdrag.solvers.sat.GroundClause class method) 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) options (kdrag.solvers.EProverSolver 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)

OptionSort() (in module kdrag) 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] owner (kdrag.contrib.pcode.CachedArray attribute)

P

parse() (in module kdrag.parsers.microlean), [1] (in module kdrag.parsers.sexp), [1] (in module kdrag.theories.sexp), [1] PartialOrder() (in module kdrag) 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) pfs (kdrag.contrib.pcode.asmspec.AsmProof 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] poly_ax() (in module kdrag.theories.univ), [1] pop() (kdrag.contrib.pcode.asmspec.Debug method) (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) (kdrag.utils.ExprCtx method) pop_goal() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) pop_lemma() (kdrag.contrib.pcode.asmspec.Debug method) pop_lemmas() (kdrag.contrib.pcode.asmspec.VCProofState method) (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] popcount() (in module kdrag.theories.bitvec), [1] popcounts() (in module kdrag.theories.bitvec), [1] pos (kdrag.solvers.sat.GroundClause attribute) 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.EProverSolver 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_sorts (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverSolver 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) PreOrder() (in module kdrag) 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.EProverSolver 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] (kdrag.solvers.sat.DPLLSolver method) 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.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) push_lemmas() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method)

Q

qed() (kdrag.Calc method) (kdrag.contrib.pcode.asmspec.AsmProofState method) (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.Calc method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) QExists() (in module kdrag) (in module kdrag.notation), [1] qfix() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) qfixes() (kdrag.contrib.pcode.asmspec.VCProofState method) (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() (in module kdrag.parsers.microlean), [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.MemState attribute) 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() (kdrag.contrib.pcode.CachedArray method) 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) Refl() (in module kdrag) reflect() (in module kdrag.reflect), [1] reg() (kdrag.contrib.pcode.asmspec.Debug method) register (kdrag.contrib.pcode.CachedArray attribute) (kdrag.contrib.pcode.MemState attribute) 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) register_well_formed() (in module kdrag.smt), [1] 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.contrib.pcode.asmspec.VCProofState method) (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.EProverSolver 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.contrib.pcode.asmspec.VCProofState method) (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.contrib.pcode.asmspec.VCProofState method) (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) RightIdentity() (in module kdrag) 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) run_all_paths() (in module kdrag.contrib.pcode.asmspec), [1] run_aprove() (in module kdrag.solvers.aprove), [1] 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.contrib.pcode.asmspec.VCProofState method) (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.contrib.pcode.asmspec.VCProofState method) (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] select_concats() (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) SemiGroup() (in module kdrag) SemiLattice (class in kdrag.theories.algebra.lattice) SemiLattice() (in module kdrag) SemiRing() (in module kdrag) Sep (class in kdrag.theories.logic.sep) Sep() (kdrag.theories.logic.sep.Sep method) seq() (in module kdrag) 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.EProverSolver 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.contrib.pcode.asmspec.VCProofState method) (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.contrib.pcode.asmspec.VCProofState method) (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] (kdrag.contrib.pcode.BinaryContext method) 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.printers.smtlib), [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) SORT (kdrag.contrib.expr.Kind attribute) sort() (in module kdrag.parsers.microlean), [1] (in module kdrag.smt), [1] Sort() (in module kdrag.theories.logic.intuitionistic), [1] sort() (kdrag.contrib.expr.ExprRef method) (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.printers.tptp), [1] SortDispatch (class in kdrag.notation) SortRef (class in kdrag.contrib.expr) sorts() (in module kdrag.utils), [1] spec (kdrag.contrib.pcode.asmspec.AsmProof attribute) spec_file() (kdrag.contrib.pcode.asmspec.Debug method) specialize() (in module kdrag.kernel), [1] (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) split() (kdrag.contrib.pcode.asmspec.VCProofState method) (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] StarSemiring() (in module kdrag) start (kdrag.contrib.pcode.asmspec.TraceState attribute) (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) start() (in module kdrag.parsers.microlean), [1] (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() (kdrag.contrib.pcode.CachedArray method) store_concat() (in module kdrag.theories.bitvec), [1] store_concats() (in module kdrag.theories.bitvec), [1] 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.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) sublemma() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) subseq() (in module kdrag.solvers.kb.string), [1] subset() (in module kdrag.theories.set), [1] subsort() (in module kdrag.cast), [1] subsort_domain() (in module kdrag.tele), [1] subst() (in module kdrag.kernel), [1] (in module kdrag.tactics), [1] substitute() (kdrag.contrib.pcode.BinaryContext method) substitute_fresh_vars() (in module kdrag.theories.logic.axioms), [1] substitute_ghost() (in module kdrag.contrib.pcode.asmspec), [1] substitute_state() (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.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tele.ProgramState method) sympify() (in module kdrag.solvers.sympy), [1]

T

t (kdrag.utils.Zipper attribute) table (kdrag.contrib.expr.Context attribute) Tail() (in module kdrag) tan_bnd() (in module kdrag.theories.real.arb), [1] terms (kdrag.solvers.egraph.EGraph attribute) test() (in module kdrag.contrib.fast), [1] (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) theorem() (in module kdrag.parsers.microlean), [1] Theorem() (in module kdrag.tactics), [1] thm (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) TLift() (in module kdrag.theories.logic.temporal), [1] to_expr() (kdrag.contrib.pcode.CachedArray method) (kdrag.contrib.pcode.MemState method) (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.solvers.sat.GroundClause 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.contrib.pcode.asmspec.VCProofState method) (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) trail (kdrag.solvers.sat.DPLLSolver attribute) trans (kdrag.contrib.yosys.VerilogModuleRel attribute) (kdrag.theories.algebra.ordering.PreOrder attribute) Trans() (in module kdrag) trans_fun (kdrag.contrib.yosys.VerilogModule attribute) translate() (kdrag.contrib.expr.Context method) (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() (in module kdrag.theories.univ), [1] type_of_sort() (in module kdrag.reflect), [1]

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.asmspec.VCProofState method) (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) unique (kdrag.contrib.pcode.MemState attribute) Unit() (in module kdrag.theories.seq), [1]

UnitSort() (in module kdrag) Unquote() (in module kdrag.theories.sexp), [1] unsat_core() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverSolver 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_and_num_insn() (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) VAR (kdrag.contrib.expr.Kind attribute) varnode_eq() (in module kdrag.contrib.pcode), [1] vc() (kdrag.contrib.pcode.asmspec.VerificationCondition method) VCProofState (class in kdrag.contrib.pcode.asmspec) 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.Debug method) (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.EProverSolver 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.EProverSolver 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.EProverSolver 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.EProverSolver 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.EProverSolver 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] 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)