Index

_

__call__() (kdrag.kernel.Proof method) (kdrag.notation.SortDispatch method) (kdrag.Proof method) __contains__() (kdrag.contrib.expr.Kind class method) (kdrag.parsers.tptp.FormulaRole class method) (kdrag.rewrite.Order class method) __default__() (kdrag.parsers.tptp.TPTPTransformer method) __default_token__() (kdrag.parsers.tptp.TPTPTransformer method) __enter__() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) __exit__() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method)

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

A

a (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.CVC5Solver 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.property), [1] 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.CVC5Solver method) (kdrag.solvers.egglog.EgglogSolver 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.tactics.ProofStateProxy 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) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) all_narrow() (in module kdrag.rewrite), [1] all_pairs() (in module kdrag.solvers.kb), [1] all_smt2() (in module kdrag.utils), [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) andE() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) andI() (in module kdrag.kernel), [1] ann() (in module kdrag.tele), [1] annot (kdrag.tactics.LemmaCallback attribute)

antipattern() (in module kdrag.utils), [1] Antisymm() (in module kdrag.property), [1] 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.tactics.ProofStateProxy 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.contracts.Contract attribute) (kdrag.contrib.term.Term attribute) (kdrag.kernel.LemmaError attribute) (kdrag.kernel.Unfolding attribute) (kdrag.rewrite.RewriteRuleException attribute) arguments() (kdrag.parsers.tptp.TPTPTransformer method) 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.CVC5Solver 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 (kdrag.theories.algebra.group.Semigroup attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) Assoc() (in module kdrag.property), [1] Assume (class in kdrag.contrib.pcode.asmspec) assume() (kdrag.solvers.symunion.SymUnion method) assumes (kdrag.contrib.yosys.SmtModInfo attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) assumes() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) assumption() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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) atomic_formula() (kdrag.parsers.tptp.TPTPTransformer method) auto() (in module kdrag.tactics), [1] (kdrag.contrib.pcode.asmspec.AsmProofState method) (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) autocases() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) ax (kdrag.kernel.Unfolding attribute) AXIOM (kdrag.parsers.tptp.FormulaRole 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.CVC5Solver 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] BDD (class in kdrag.solvers.bdd) beta() (in module kdrag.rewrite), [1] (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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] Block (class in kdrag.contrib.ir) blocks (kdrag.contrib.ir.Function attribute) body (kdrag.kernel.Unfolding attribute) Bool (in module kdrag.theories.univ) Bool() (in module kdrag.theories.logic.temporal), [1] Bools() (in module kdrag.theories.logic.temporal), [1] boolsimp() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) 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.CVC5Solver 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] calls_of() (kdrag.contrib.ir.Function method) case() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) cases() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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) cegis_simple() (in module kdrag.solvers.synth), [1] cells (kdrag.contrib.yosys.SmtModInfo attribute) check() (kdrag.solvers.BaseSolver method) (kdrag.solvers.CVC5Solver 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.CVC5Solver 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.kernel), [1] Choose() (in module kdrag.theories.set), [1] Clause (in module kdrag.solvers.sat) clauses (kdrag.solvers.sat.DPLLSolver attribute) clear() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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) cnf() (kdrag.parsers.tptp.TPTPTransformer method) cnf_formula() (kdrag.parsers.tptp.TPTPTransformer method) codomain() (in module kdrag.smt), [1] coerce() (in module kdrag.modal), [1] collect() (kdrag.solvers.symunion.SymUnion method) collect_decls() (in module kdrag.solvers), [1] collect_sorts() (in module kdrag.solvers), [1]

comm (kdrag.theories.algebra.group.AbelSemiGroup attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) Comm() (in module kdrag.property), [1] CommAddSemigroup (class in kdrag.theories.algebra) CommMonoid() (in module kdrag.property), [1] CommSemigroup (class in kdrag.theories.algebra) CommSemiRing() (in module kdrag.property), [1] compares() (in module kdrag.hypothesis), [1] compile_and_link() (in module kdrag.printers.c), [1] compile_and_link_defn() (in module kdrag.printers.c), [1] compile_c() (in module kdrag.printers.c), [1] compile_rust() (in module kdrag.printers.rust), [1] complement() (in module kdrag.theories.set), [1] ComplexSort() (in module kdrag) compose() (in module kdrag.kernel), [1] (in module kdrag.notation), [1] conc (kdrag.rewrite.Rule attribute) Concat() (in module kdrag.contrib.absint.knownbit), [1] concretize() (kdrag.solvers.symunion.SymUnion method) Cond (class in kdrag.notation) cond (kdrag.solvers.symunion.PartialExpr attribute) cond() (in module kdrag) (in module kdrag.notation), [1] conde() (in module kdrag.notation), [1] cong() (in module kdrag.theories.logic.axioms), [1] CONJECTURE (kdrag.parsers.tptp.FormulaRole attribute) 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) const() (kdrag.parsers.tptp.TPTPTransformer method) const_sorts (kdrag.parsers.tptp.TPTPTransformer attribute) constructor_num() (in module kdrag.datatype), [1] consts (kdrag.parsers.tptp.TPTPTransformer attribute) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) Contract (class in kdrag.contracts) contract (kdrag.solvers.symunion.PartialFuncDecl attribute) contract() (in module kdrag.contracts), [1] (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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.tactics.ProofStateProxy 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.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.contrib.pcode.asmspec.VCProofState property) (kdrag.tactics.Goal attribute) (kdrag.tactics.ProofState property) (kdrag.tactics.ProofStateProxy property) (kdrag.tele.ProgramState property) (kdrag.utils.Zipper attribute) ctx_find() (kdrag.tactics.Goal method) 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) cut (kdrag.contrib.ir.Spec attribute) cvc5() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) CVC5Solver (class in kdrag.solvers)

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.Unfolding attribute) (kdrag.refine.RefinedDefn attribute) (kdrag.solvers.symunion.PartialFuncDecl attribute) decl() (in module kdrag.smt), [1] (kdrag.contrib.expr.ExprRef method) (kdrag.refine.OpenDefn method) decl_axiom() (in module kdrag.printers.lean), [1] decl_index() (in module kdrag.rewrite), [1] decl_occurs() (in module kdrag.kernel), [1] decl_sig() (in module kdrag.printers.lean), [1] declare() (in module kdrag.kernel), [1] (kdrag.notation.SortDispatch method) (kdrag.solvers.bdd.BDD method) 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.refine.OpenDefn 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] define_simple() (in module kdrag.kernel), [1] defined_decls() (in module kdrag.utils), [1] defns (in module kdrag.kernel) deserialize_proof() (in module kdrag.contrib.cert), [1] 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) diseq() (kdrag.parsers.tptp.TPTPTransformer method) disjunction() (kdrag.parsers.tptp.TPTPTransformer 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.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.solvers.symunion.SymUnion class method) (kdrag.tactics.Goal class method) emt() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) EndStmt (in module kdrag.contrib.pcode.asmspec) Entry (class in kdrag.contrib.pcode.asmspec) entry (kdrag.contrib.ir.Function attribute) 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.parsers.tptp.TPTPTransformer method) (kdrag.tactics.Calc method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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] esolve() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) execute1() (kdrag.contrib.pcode.BinaryContext method) execute1_schema() (kdrag.contrib.pcode.BinaryContext method) execute_block() (kdrag.contrib.pcode.BinaryContext method) execute_insn() (in module kdrag.contrib.pcode.asmspec), [1] execute_simstate() (kdrag.contrib.pcode.BinaryContext method)

execute_spec_and_insn() (in module kdrag.contrib.pcode.asmspec), [1] execute_spec_stmts() (in module kdrag.contrib.pcode.asmspec), [1] execute_trace_frags() (kdrag.contrib.pcode.BinaryContext method) 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] exfalso() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) exists (in module kdrag.notation) Exists() (in module kdrag.smt), [1] exists() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.parsers.tptp.TPTPTransformer method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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) (kdrag.solvers.symunion.PartialExpr attribute) expr() (in module kdrag.parsers.microlean), [1] (in module kdrag.reflect), [1] (kdrag.notation.Cond method) expr2py (in module kdrag.solvers.symunion) expr2py_default() (in module kdrag.solvers.symunion), [1] 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) extend() (kdrag.utils.ExprCtx method) extract() (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.egraph.EGraph method)

F

f (kdrag.contracts.Contract attribute) (kdrag.contrib.term.Term 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] Fin0Sort() (in module kdrag.theories.real.vec), [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] finite() (in module kdrag.theories.set), [1] finite_decl() (in module kdrag.theories.set), [1] finite_empty() (in module kdrag.theories.set), [1] FinP() (in module kdrag) FinSet() (in module kdrag.theories.zf.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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) FixedSort() (in module kdrag.theories.fixed), [1] fixes() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) flatmap() (kdrag.solvers.symunion.SymUnion method) flint_bnd() (in module kdrag.theories.real.arb), [1] flint_eq_ax_unsafe() (in module kdrag.theories.real.arb), [1] flip() (kdrag.solvers.symunion.SymUnion static method) fof() (kdrag.parsers.tptp.TPTPTransformer method) fof_and_formula() (kdrag.parsers.tptp.TPTPTransformer method) fof_or_formula() (kdrag.parsers.tptp.TPTPTransformer method) fof_variable_list() (kdrag.parsers.tptp.TPTPTransformer method) forall (in module kdrag.notation) ForAll() (in module kdrag.smt), [1]

forall() (kdrag.kernel.Proof method) (kdrag.parsers.tptp.TPTPTransformer 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] formula (kdrag.parsers.tptp.TPTPFormulaEntry attribute) FormulaRole (class in kdrag.parsers.tptp) forward() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) forward_rule() (in module kdrag.rewrite), [1] free_in() (in module kdrag.utils), [1] free_vars() (in module kdrag.kernel), [1] (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] fs (kdrag.refine.OpenDefn attribute) full_simp() (in module kdrag.rewrite), [1] fun_app() (kdrag.parsers.tptp.TPTPTransformer method) func_kind() (in module kdrag.smt), [1] func_sigs (kdrag.parsers.tptp.TPTPTransformer attribute) funcdecl_smtlib() (in module kdrag.printers.smtlib), [1] FuncDeclRef (class in kdrag.contrib.expr) funcs (kdrag.parsers.tptp.TPTPTransformer attribute) Function (class in kdrag.contrib.ir) Function() (in module kdrag.smt), [1] (kdrag.contrib.expr.Context method) FunVec() (in module kdrag.theories.real.vec), [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.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) get_proof() (kdrag.solvers.egraph.EGraph method) get_reg() (kdrag.contrib.pcode.BinaryContext method) (kdrag.contrib.pcode.MemState 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) GFP() (in module kdrag) 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.contrib.pcode.asmspec.VCProofState property) (kdrag.tactics.Goal attribute) (kdrag.tactics.ProofState property) (kdrag.tactics.ProofStateProxy property) (kdrag.tele.ProgramState property) goals (kdrag.tactics.ProofState attribute) (kdrag.tactics.ProofStateProxy attribute) (kdrag.tele.ProgramState 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.tactics.ProofStateProxy 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 (kdrag.theories.algebra.lattice.SemiLattice attribute) Idem() (in module kdrag.property), [1] If() (in module kdrag.theories.logic.temporal), [1] iff() (kdrag.parsers.tptp.TPTPTransformer method) Implies() (in module kdrag.theories.logic.intuitionistic), [1] (in module kdrag.theories.logic.temporal), [1] implies() (kdrag.parsers.tptp.TPTPTransformer method) Implies() (kdrag.theories.logic.sep.Sep method) In() (in module kdrag.modal), [1] 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.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.tactics.ProofStateProxy 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] 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) initialize() (in module kdrag.contrib.rust), [1] inj_lemmas() (in module kdrag.datatype), [1] Injective() (in module kdrag.theories.set), [1] input_sort (kdrag.contrib.yosys.VerilogModule attribute) inputs (kdrag.contrib.yosys.SmtModInfo attribute) insert() (kdrag.utils.ExprCtx method) insn() (kdrag.contrib.pcode.asmspec.Debug method) insns (kdrag.contrib.ir.Block attribute) 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] intify() (in module kdrag.contrib.fast), [1] intros() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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) is_accessor() (in module kdrag.smt), [1] is_app() (in module kdrag.smt), [1] is_complex() (in module kdrag) is_conflict() (kdrag.solvers.sat.DPLLSolver method) is_constructor() (in module kdrag.smt), [1] is_declared() (in module kdrag.kernel), [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_tuple() (in module kdrag) 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

join() (kdrag.solvers.symunion.SymUnion method)

json() (kdrag.contrib.pcode.asmspec.AsmSpec method) Judgement (class in kdrag.kernel)

K

k (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.CVC5Solver 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.contrib.absint.knownbit), [1] (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.contracts module kdrag.contrib module kdrag.contrib.absint module kdrag.contrib.absint.knownbit module kdrag.contrib.cert module kdrag.contrib.cpp module kdrag.contrib.data_modulo module kdrag.contrib.expr module kdrag.contrib.fast module kdrag.contrib.hoare module kdrag.contrib.ir module kdrag.contrib.ir.mlir module kdrag.contrib.ir.qbe module kdrag.contrib.pcode module kdrag.contrib.pcode.asmspec module kdrag.contrib.rust module kdrag.contrib.term 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.refine module kdrag.reflect module kdrag.rewrite module kdrag.smt module kdrag.solvers module kdrag.solvers.aprove module kdrag.solvers.bdd 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.sat module kdrag.solvers.sympy module

kdrag.solvers.symunion module kdrag.solvers.synth 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.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.fun module kdrag.theories.real.geometry module kdrag.theories.real.interval module kdrag.theories.real.lim_algebra module kdrag.theories.real.ndarray module kdrag.theories.real.rset module kdrag.theories.real.seq module kdrag.theories.real.vec module kdrag.theories.real.vec2 module kdrag.theories.real.vec3 module kdrag.theories.regex module kdrag.theories.seq module kdrag.theories.set module kdrag.theories.sexp module kdrag.theories.univ module kdrag.theories.zf module kdrag.theories.zf.axioms module kdrag.theories.zf.prod_lemmas module kdrag.theories.zf.zf 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) KnownBits() (in module kdrag.contrib.absint.knownbit), [1] KnownBits_ (class in kdrag.contrib.absint.knownbit) KnownBitsSort() (in module kdrag.contrib.absint.knownbit), [1] Knowns() (in module kdrag.contrib.absint.knownbit), [1] KnuckleClosure (class in kdrag.reflect)

L

Label (in module kdrag.contrib.ir) 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) lb_le_ub (in module kdrag.theories.real.rset) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) (kdrag.utils.DeclHole method) (kdrag.utils.Zipper method) left_id (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) LeftIdentity() (in module kdrag.property), [1] 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 lemmas (kdrag.tactics.ProofState attribute) (kdrag.tactics.ProofStateProxy attribute) (kdrag.tele.ProgramState attribute)

lemmas() (in module kdrag.contracts), [1] LeoIIISolver (class in kdrag.solvers) less_le_not_le (kdrag.theories.algebra.ordering.PreOrder attribute) let() (kdrag.solvers.egglog.EgglogSolver method) LFP() (in module kdrag) lhs (kdrag.rewrite.RewriteRule attribute) Lift() (kdrag.theories.logic.sep.Sep method) lift_binop() (in module kdrag.theories.logic.temporal), [1] lift_ite() (in module kdrag.utils), [1] lift_unop() (in module kdrag.theories.logic.temporal), [1] limit() (in module kdrag.solvers.sympy), [1] Linear() (in module kdrag.theories.real.fun), [1] link() (in module kdrag.printers.c), [1] list() (in module kdrag) List() (in module kdrag.theories.list), [1] List_ (class in kdrag.theories.list) ListSort() (in module kdrag) Lit (in module kdrag.solvers.sat) 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.CVC5Solver 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] make_unfolding() (in module kdrag.kernel), [1] makevar() (kdrag.solvers.sat.DPLLSolver method) mangle_decl() (in module kdrag.printers.tptp), [1] mangle_decl_smtlib() (in module kdrag.printers.smtlib), [1] mangle_name() (in module kdrag.solvers.egglog), [1] map() (kdrag.solvers.symunion.PartialExpr method) (kdrag.solvers.symunion.SymUnion method) map2() (kdrag.solvers.symunion.PartialExpr method) (kdrag.solvers.symunion.SymUnion method) 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.contracts kdrag.contrib kdrag.contrib.absint kdrag.contrib.absint.knownbit kdrag.contrib.cert kdrag.contrib.cpp kdrag.contrib.data_modulo kdrag.contrib.expr kdrag.contrib.fast kdrag.contrib.hoare kdrag.contrib.ir kdrag.contrib.ir.mlir kdrag.contrib.ir.qbe kdrag.contrib.pcode kdrag.contrib.pcode.asmspec kdrag.contrib.rust kdrag.contrib.term 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.refine kdrag.reflect kdrag.rewrite kdrag.smt kdrag.solvers kdrag.solvers.aprove kdrag.solvers.bdd 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.sat kdrag.solvers.sympy kdrag.solvers.symunion kdrag.solvers.synth 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.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.fun kdrag.theories.real.geometry kdrag.theories.real.interval kdrag.theories.real.lim_algebra kdrag.theories.real.ndarray kdrag.theories.real.rset kdrag.theories.real.seq kdrag.theories.real.vec kdrag.theories.real.vec2 kdrag.theories.real.vec3 kdrag.theories.regex kdrag.theories.seq kdrag.theories.set kdrag.theories.sexp kdrag.theories.univ kdrag.theories.zf kdrag.theories.zf.axioms kdrag.theories.zf.prod_lemmas kdrag.theories.zf.zf kdrag.utils

modus() (in module kdrag.kernel), [1] Monoid (class in kdrag.theories.algebra) (class in kdrag.theories.algebra.group) Monoid() (in module kdrag.property), [1] 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) 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.CVC5Solver 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.term.Var attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) (kdrag.kernel.Unfolding attribute) (kdrag.parsers.tptp.TPTPFormulaEntry attribute) (kdrag.refine.OpenDefn 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) (kdrag.solvers.sat.GroundClause attribute)

neg_ext() (in module kdrag.theories.logic.axioms), [1] neglit() (kdrag.parsers.tptp.TPTPTransformer method) NEq() (in module kdrag.theories.logic.temporal), [1] newgoal() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) NewType() (in module kdrag) (in module kdrag.datatype), [1] Next() (in module kdrag.modal), [1] (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] not_formula() (kdrag.parsers.tptp.TPTPTransformer method) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) occurs() (in module kdrag.utils), [1] of_datatype() (in module kdrag.printers.lean), [1] of_defined_fun() (kdrag.contrib.ir.Block class method) of_defined_funs() (kdrag.contrib.ir.Function class method) of_defn() (in module kdrag.printers.c), [1] of_expr() (in module kdrag.printers.lean), [1] (kdrag.contrib.ir.Block class method) (kdrag.solvers.sat.GroundClause class method) of_file() (kdrag.contrib.pcode.asmspec.AsmSpec class method) of_list() (kdrag.solvers.symunion.SymUnion class method) (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.kernel), [1] (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) OpenDefn (class in kdrag.refine) options (kdrag.solvers.CVC5Solver 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) 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

PAnd() (in module kdrag.modal), [1] parse() (in module kdrag.parsers.microlean), [1] (in module kdrag.parsers.sexp), [1] (in module kdrag.theories.sexp), [1] PartialExpr (class in kdrag.solvers.symunion) PartialFuncDecl (class in kdrag.solvers.symunion) PartialOrder() (in module kdrag.property), [1] path_cond (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) (kdrag.contrib.pcode.SimState attribute) pathmap() (in module kdrag.utils), [1] pattern() (in module kdrag.parsers.microlean), [1] pattern_match() (in module kdrag.datatype), [1] PBoolRef (in module kdrag.modal) PC (in module kdrag.contrib.pcode) pc (kdrag.contrib.pcode.SimState attribute) pc_of_addr() (in module kdrag.contrib.pcode), [1] PDistinct() (in module kdrag.modal), [1] PEq() (in module kdrag.modal), [1] perf_event() (in module kdrag.config), [1] PExprRef (in module kdrag.modal) pf (kdrag.rewrite.RewriteRule attribute) (kdrag.rewrite.Rule attribute) pfs (kdrag.contrib.pcode.asmspec.AsmProof attribute) phis() (kdrag.contrib.ir.Function method) Pi() (in module kdrag.tele), [1] pick() (kdrag.solvers.bdd.BDD method) pick_iter() (kdrag.solvers.bdd.BDD method) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) (kdrag.utils.ExprCtx method) pop_goal() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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.tactics.ProofStateProxy 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] POr() (in module kdrag.modal), [1] pos (kdrag.solvers.sat.GroundClause attribute) poslit() (kdrag.parsers.tptp.TPTPTransformer method) post (kdrag.contracts.Contract attribute) (kdrag.contrib.hoare.Hoare attribute) (kdrag.contrib.ir.Spec attribute) PostFix() (in module kdrag) powers (kdrag.theories.real.seq.Series attribute) PowerSet() (in module kdrag.theories.set), [1] pp_sort() (in module kdrag.contrib.ir), [1] pprint_sexp() (in module kdrag.parsers.sexp), [1] pprint_sexps() (in module kdrag.parsers.sexp), [1] pre (kdrag.contracts.Contract attribute) (kdrag.contrib.hoare.Hoare attribute) (kdrag.contrib.ir.Spec attribute) predefined (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.CVC5Solver 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_names (kdrag.solvers.egglog.EgglogSolver attribute) predefined_sorts (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.CVC5Solver 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) predicate() (kdrag.parsers.tptp.TPTPTransformer method) preds (kdrag.parsers.tptp.TPTPTransformer attribute) PreFix() (in module kdrag) PreOrder (class in kdrag.theories.algebra.ordering) PreOrder() (in module kdrag.property), [1] 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] print_decl() (kdrag.solvers.egglog.EgglogSolver method) 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.contracts.Contract attribute) proof() (kdrag.solvers.BaseSolver method) (kdrag.solvers.CVC5Solver 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) ProofStateProxy (class in kdrag.tactics) proofstep_to_smt2() (in module kdrag.utils), [1] 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] property (kdrag.refine.RefinedDefn property) PropRef (in module kdrag.theories.logic.sep) 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] (kdrag.contrib.pcode.BinaryContext method) prove_sig() (in module kdrag.tele), [1] prune() (in module kdrag.utils), [1] (kdrag.solvers.symunion.SymUnion method) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) push_lemmas() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) py2expr() (in module kdrag.solvers.symunion), [1]

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.tactics.ProofStateProxy 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) qfixes() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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] refine() (kdrag.refine.RefinedDefn method) RefinedDefn (class in kdrag.refine) refl (kdrag.theories.algebra.ordering.PreOrder attribute) Refl() (in module kdrag.property), [1] 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_definition() (in module kdrag.kernel), [1] 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) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) replace() (in module kdrag.solvers.kb.multiset), [1] (in module kdrag.solvers.kb.string), [1] res (kdrag.solvers.CVC5Solver 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)

resolve_addr() (kdrag.contrib.pcode.BinaryContext method) ReSort() (in module kdrag.theories.regex), [1] Results (class in kdrag.contrib.pcode.asmspec) reverse() (kdrag.utils.ExprCtx method) reverse_implies() (kdrag.parsers.tptp.TPTPTransformer method) revert() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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_of_expr_exact() (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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) (kdrag.utils.DeclHole method) (kdrag.utils.Zipper method) right_id (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) RightIdentity() (in module kdrag.property), [1] rlemma() (in module kdrag.theories.real), [1] rmul (in module kdrag.notation) role (kdrag.parsers.tptp.TPTPFormulaEntry attribute) 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] rule_of_expr_exact() (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.contrib.pcode.asmspec.VCProofState method) (kdrag.solvers.egraph.EGraph method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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.tactics.ProofStateProxy 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.property), [1] SemiLattice (class in kdrag.theories.algebra.lattice) SemiLattice() (in module kdrag.property), [1] SemiRing() (in module kdrag.property), [1] 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] SeqVec() (in module kdrag.theories.real.vec), [1] SeqVecP() (in module kdrag) serialize_proof() (in module kdrag.contrib.cert), [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.CVC5Solver 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) SetMonotone() (in module kdrag) setvalue() (kdrag.contrib.pcode.MemState method) setvalue_ram() (kdrag.contrib.pcode.MemState method) Sexp (in module kdrag.parsers.sexp) sexpr() (kdrag.solvers.BaseSolver method) (kdrag.solvers.CVC5Solver 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) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) sig (kdrag.contrib.ir.Block attribute) (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.tactics.ProofStateProxy 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.zf.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] (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method)

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 (kdrag.parsers.tptp.TPTPTransformer attribute) (kdrag.refine.OpenDefn attribute) sorts() (in module kdrag.utils), [1] Spec (class in kdrag.contrib.ir) spec (kdrag.contrib.pcode.asmspec.AsmProof attribute) (kdrag.contrib.pcode.asmspec.Debug 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) SpecStmt (in module kdrag.contrib.pcode.asmspec) splintro() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) split() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy 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.property), [1] 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) (kdrag.parsers.tptp.TPTPTransformer method) StartStmt (in module kdrag.contrib.pcode.asmspec) state (kdrag.contrib.pcode.asmspec.TraceState attribute) state_sort (kdrag.contrib.yosys.VerilogModule attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) StateExpr (in module kdrag.contrib.pcode) StateProp (in module kdrag.contrib.pcode) step() (kdrag.contrib.pcode.asmspec.Debug method) store() (kdrag.contrib.pcode.CachedArray method) (kdrag.solvers.symunion.SymUnion 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) sublemma() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) subseq() (in module kdrag.solvers.kb.string), [1] subset() (in module kdrag.theories.set), [1] SubSort (in module kdrag.tele) 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) (kdrag.solvers.bdd.BDD 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] succ_calls() (kdrag.contrib.ir.Block method) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) symp() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) sympify() (in module kdrag.solvers.sympy), [1] sympy_const() (in module kdrag.solvers.sympy), [1] SymUnion (class in kdrag.solvers.symunion)

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] Telescope (in module kdrag.tele) Term (class in kdrag.contrib.term) terms (kdrag.solvers.egraph.EGraph attribute) test() (in module kdrag.contrib.absint.knownbit), [1] (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.real.interval), [1] (in module kdrag.theories.real.seq), [1] (in module kdrag.theories.zf.zf), [1] test_pcode() (in module kdrag.contrib.pcode), [1] TExists() (in module kdrag.tele), [1] tff() (kdrag.parsers.tptp.TPTPTransformer method) tff_type() (kdrag.parsers.tptp.TPTPTransformer method) tff_type_atom() (kdrag.parsers.tptp.TPTPTransformer method) tff_type_formula() (kdrag.parsers.tptp.TPTPTransformer method) tff_type_product() (kdrag.parsers.tptp.TPTPTransformer method) tff_typed_variable() (kdrag.parsers.tptp.TPTPTransformer method) 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] thf() (kdrag.parsers.tptp.TPTPTransformer method) thf_and_formula() (kdrag.parsers.tptp.TPTPTransformer method) thf_app() (kdrag.parsers.tptp.TPTPTransformer method) thf_lambda() (kdrag.parsers.tptp.TPTPTransformer method) thf_or_formula() (kdrag.parsers.tptp.TPTPTransformer method) 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] to_z3() (in module kdrag.parsers.tptp), [1] toBV() (in module kdrag.theories.bitvec), [1] top_goal() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) Topology (class in kdrag.theories.algebra.topology) tptp2smt() (in module kdrag.solvers), [1] TPTPFormulaEntry (class in kdrag.parsers.tptp) TPTPTransformer (class in kdrag.parsers.tptp) Trace (in module kdrag.contrib.pcode.asmspec) 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) tracestates (kdrag.contrib.pcode.asmspec.Debug attribute) trail (kdrag.solvers.sat.DPLLSolver attribute) trans (kdrag.contrib.yosys.VerilogModuleRel attribute) (kdrag.theories.algebra.ordering.PreOrder attribute) Trans() (in module kdrag.property), [1] trans_fun (kdrag.contrib.yosys.VerilogModule attribute) transform() (kdrag.parsers.tptp.TPTPTransformer method) translate() (kdrag.contrib.expr.Context method) (kdrag.contrib.pcode.BinaryContext method) (kdrag.solvers.bdd.BDD method) translate_tuple_args() (in module kdrag.solvers.sympy), [1] trigger() (in module kdrag.kernel), [1] Truth() (in module kdrag.theories.sexp), [1] TSort() (in module kdrag.theories.logic.temporal), [1] tuple_() (in module kdrag) TupleSort() (in module kdrag) TweeSolver (class in kdrag.solvers) Type (in module kdrag.tele) 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] Undef() (in module kdrag) 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.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) unfold_defns() (in module kdrag.kernel), [1] Unfolding (class in kdrag.kernel) 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.CVC5Solver 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) valueize() (kdrag.solvers.symunion.SymUnion method) values (kdrag.solvers.symunion.SymUnion attribute) vampire() (kdrag.contrib.pcode.asmspec.VCProofState method) (kdrag.tactics.ProofState method) (kdrag.tactics.ProofStateProxy method) (kdrag.tele.ProgramState method) VampireSolver (class in kdrag.solvers) VampireTHFSolver (class in kdrag.solvers) Var (class in kdrag.contrib.term) (in module kdrag.solvers.sat) VAR (kdrag.contrib.expr.Kind attribute) var() (kdrag.parsers.tptp.TPTPTransformer method) varnode_eq() (in module kdrag.contrib.pcode), [1] vars (kdrag.parsers.tptp.TPTPTransformer attribute) vc() (kdrag.contrib.pcode.asmspec.VerificationCondition method)

VCProofState (class in kdrag.contrib.pcode.asmspec) vcs (kdrag.contrib.pcode.asmspec.Debug attribute) 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] vname() (kdrag.contrib.ir.Block method) vprove() (in module kdrag.tactics), [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) while_() (in module kdrag.theories.algebra.kleene), [1] 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.solvers.symunion.SymUnion class method) (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.CVC5Solver 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_smt2_files() (in module kdrag.utils), [1] write_tptp() (kdrag.solvers.BaseSolver method) (kdrag.solvers.CVC5Solver 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.CVC5Solver 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.CVC5Solver 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.CVC5Solver 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] z3_to_egglog() (in module kdrag.solvers.egglog), [1] zero (kdrag.theories.algebra.vector.VectorSpace attribute) zero_add (in module kdrag.theories.algebra.vector) Zeros() (in module kdrag.contrib.absint.knownbit), [1] Zipper (class in kdrag.utils) ZipperpositionSolver (class in kdrag.solvers)