Index

_

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

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

A

a (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) AbelSemiGroup (class in kdrag.theories.algebra.group) abstract_arith() (in module kdrag.theories.real), [1] accessor_def() (in module kdrag.printers.lean), [1] accessor_lemmas() (in module kdrag.datatype), [1] accessor_num() (in module kdrag.datatype), [1] Add (class in kdrag.theories.real) add (in module kdrag.notation) (kdrag.theories.algebra.AddSemigroup attribute) (kdrag.theories.algebra.CommAddSemigroup attribute) add() (in module kdrag.solvers.kb.multiset), [1] (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.SATSolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) add_assert() (kdrag.contrib.pcode.asmspec.AsmSpec method) add_assign() (kdrag.contrib.pcode.asmspec.AsmSpec 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) add_entry() (kdrag.contrib.pcode.asmspec.AsmSpec method) add_exit() (kdrag.contrib.pcode.asmspec.AsmSpec method) add_inv (kdrag.theories.algebra.vector.VectorSpace attribute) add_lemma() (kdrag.Lemma method) (kdrag.tactics.Lemma method) add_note() (kdrag.kernel.LemmaError method) (kdrag.rewrite.RewriteRuleException method) add_term() (kdrag.solvers.egraph.EGraph method) add_zero (kdrag.theories.algebra.vector.VectorSpace attribute) AddAssoc (in module kdrag.theories.real) AddComm (in module kdrag.theories.real) AddId (in module kdrag.theories.real) addr (kdrag.contrib.pcode.asmspec.Assert attribute) (kdrag.contrib.pcode.asmspec.Assign attribute) (kdrag.contrib.pcode.asmspec.Assume attribute) (kdrag.contrib.pcode.asmspec.BoolStmt attribute) (kdrag.contrib.pcode.asmspec.Cut attribute) (kdrag.contrib.pcode.asmspec.Entry attribute) (kdrag.contrib.pcode.asmspec.Exit attribute) addrmap (kdrag.contrib.pcode.asmspec.AsmSpec attribute) AddSemigroup (class in kdrag.theories.algebra) admit (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) admit() (kdrag.Lemma method) (kdrag.tactics.Lemma method) all_narrow() (in module kdrag.rewrite), [1] all_pairs() (in module kdrag.solvers.kb), [1] all_values() (in module kdrag.utils), [1] allconsts (kdrag.contrib.yosys.SmtModInfo attribute) allseqs (kdrag.contrib.yosys.SmtModInfo attribute) alpha_eq() (in module kdrag.utils), [1] alpha_norm() (in module kdrag.utils), [1] Always (class in kdrag.contrib.pcode.asmspec) and_ (in module kdrag.notation)

andI() (in module kdrag.kernel), [1] ann() (in module kdrag.tele), [1] annot (kdrag.tactics.LemmaCallback attribute) antipattern() (in module kdrag.utils), [1] Antisymm (class in kdrag.property) antisymm (kdrag.property.Antisymm attribute) anyconsts (kdrag.contrib.yosys.SmtModInfo attribute) anyseqs (kdrag.contrib.yosys.SmtModInfo attribute) apply() (in module kdrag.rewrite), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) arb_bnd() (in module kdrag.theories.real.arb), [1] arb_ge() (in module kdrag.theories.real.arb), [1] arb_gt() (in module kdrag.theories.real.arb), [1] arb_le_ax() (in module kdrag.theories.real.arb), [1] arb_lt_ax() (in module kdrag.theories.real.arb), [1] arb_over_of_mid_rad() (in module kdrag.theories.real.arb), [1] arg() (in module kdrag.smt), [1] (kdrag.contrib.expr.ExprRef method) args (kdrag.kernel.Defn attribute) (kdrag.kernel.LemmaError attribute) (kdrag.rewrite.RewriteRuleException attribute) arity() (kdrag.contrib.expr.FuncDeclRef method) asize (kdrag.contrib.yosys.SmtModInfo attribute) AsmSpec (class in kdrag.contrib.pcode.asmspec) assemble_and_check() (in module kdrag.contrib.pcode.asmspec), [1] assemble_and_check_str() (in module kdrag.contrib.pcode.asmspec), [1] assemble_and_gen_vcs() (in module kdrag.contrib.pcode.asmspec), [1] Assert (class in kdrag.contrib.pcode.asmspec) assert_and_track() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) assert_eq() (kdrag.property.TypeClass method) (kdrag.theories.algebra.group.AbelSemiGroup method) (kdrag.theories.algebra.group.Group method) (kdrag.theories.algebra.group.Monoid method) (kdrag.theories.algebra.group.Semigroup method) (kdrag.theories.algebra.lattice.SemiLattice method) (kdrag.theories.algebra.ordering.PreOrder method) (kdrag.theories.algebra.topology.Topology method) (kdrag.theories.algebra.vector.Normed method) (kdrag.theories.algebra.vector.VectorSpace method) assertion (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) asserts (kdrag.contrib.yosys.SmtModInfo attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) Assign (class in kdrag.contrib.pcode.asmspec) assign() (kdrag.contrib.hoare.Hoare class method) Assoc (class in kdrag.property) assoc (kdrag.property.Assoc attribute) (kdrag.theories.algebra.group.Semigroup attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) assoc_comm() (in module kdrag.property), [1] assoc_norm() (in module kdrag.property), [1] Assume (class in kdrag.contrib.pcode.asmspec) assumes (kdrag.contrib.yosys.SmtModInfo attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) assumption() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ast_size_sexpr() (in module kdrag.utils), [1] AstRef (class in kdrag.contrib.expr) Asymm (class in kdrag.property) asymm (kdrag.property.Asymm attribute) auto() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ax (kdrag.kernel.Defn attribute) axiom() (in module kdrag) (in module kdrag.kernel), [1] axiom_sig() (in module kdrag.tele), [1]

B

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

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

C

c (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) c_of_expr() (in module kdrag.printers.c), [1] Calc (class in kdrag) (class in kdrag.tactics) call_dict (in module kdrag.datatype) call_yosys_functional() (in module kdrag.contrib.yosys), [1] cases() (kdrag.Lemma method) (kdrag.tactics.Lemma method) cb (kdrag.tactics.LemmaCallback attribute) cells (kdrag.contrib.yosys.SmtModInfo attribute) check() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.SATSolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) (kdrag.theories.algebra.group.AbelSemiGroup method) (kdrag.theories.algebra.group.Group method) (kdrag.theories.algebra.group.Monoid method) (kdrag.theories.algebra.group.Semigroup method) (kdrag.theories.algebra.lattice.SemiLattice method) (kdrag.theories.algebra.ordering.PreOrder method) (kdrag.theories.algebra.topology.Topology method) (kdrag.theories.algebra.vector.Normed method) (kdrag.theories.algebra.vector.VectorSpace method) check_semigroup() (in module kdrag.theories.algebra), [1] check_tptp_status() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

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

D

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

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

E

e (kdrag.property.Identity attribute) (kdrag.property.LeftIdentity attribute) (kdrag.property.RightIdentity attribute) (kdrag.theories.algebra.group.Monoid attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) eclasses() (kdrag.solvers.egraph.EGraph method) EgglogSolver (class in kdrag.solvers.egglog) EGraph (class in kdrag.solvers.egraph) einstan() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) ematch() (kdrag.solvers.egraph.EGraph method) empty() (kdrag.tactics.Goal class method) Entry (class in kdrag.contrib.pcode.asmspec) Enum() (in module kdrag.datatype), [1] EProverTHFSolver (class in kdrag.solvers) eq (in module kdrag.notation) EQ (kdrag.rewrite.Order attribute) Eq() (in module kdrag.smt), [1] eq() (in module kdrag.smt), [1] (kdrag.Calc method) (kdrag.contrib.expr.AstRef method) (kdrag.contrib.expr.ExprRef method) (kdrag.contrib.expr.FuncDeclRef method) (kdrag.contrib.expr.SortRef method) (kdrag.contrib.expr.TypeVarRef method) (kdrag.Lemma method) (kdrag.tactics.Calc method) (kdrag.tactics.Lemma method) eval_() (in module kdrag.reflect), [1] execute1() (kdrag.contrib.pcode.BinaryContext method) execute1_schema() (kdrag.contrib.pcode.BinaryContext method) execute_insn() (in module kdrag.contrib.pcode.asmspec), [1] execute_spec_stmts() (in module kdrag.contrib.pcode.asmspec), [1]

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

F

f (kdrag.property.Assoc attribute) (kdrag.property.Comm attribute) (kdrag.property.Idem attribute) (kdrag.property.Identity attribute) (kdrag.property.LeftIdentity attribute) (kdrag.property.RightIdentity attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) factor() (in module kdrag.theories.real.sympy), [1] failures (kdrag.contrib.pcode.asmspec.Results attribute) fallthruOp() (kdrag.contrib.pcode.BinaryContext method) FamilyUnion() (in module kdrag.theories.set), [1] Fin() (in module kdrag.tele), [1] find() (kdrag.solvers.egraph.EGraph method) find_calls() (in module kdrag.utils), [1] Finite() (in module kdrag.theories.set), [1] finsize() (in module kdrag.printers), [1] FinSort() (in module kdrag.theories.real.vec), [1] fix() (kdrag.Lemma method) (kdrag.tactics.Lemma method) FixedSort() (in module kdrag.theories.fixed), [1] fixes() (kdrag.Lemma method) (kdrag.tactics.Lemma method) flint_bnd() (in module kdrag.theories.real.arb), [1] flint_eq_ax_unsafe() (in module kdrag.theories.real.arb), [1] forall() (kdrag.kernel.Proof method) (kdrag.Proof method)

ForAllI() (in module kdrag.tactics), [1] forallI() (in module kdrag.tactics), [1] forget() (in module kdrag.kernel), [1] forget2() (in module kdrag.kernel), [1] forward_rule() (in module kdrag.rewrite), [1] free_in() (in module kdrag.kernel), [1] free_vars() (in module kdrag.utils), [1] fresh_const() (in module kdrag.kernel), [1] fresh_symbol() (in module kdrag.theories.real.sympy), [1] FreshConst() (in module kdrag.contrib.expr), [1] freshen() (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) FreshVar() (in module kdrag) (in module kdrag.kernel), [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) fromBV() (in module kdrag.theories.bitvec), [1] full_simp() (in module kdrag.rewrite), [1] func_kind() (in module kdrag.smt), [1] funcdecl_smtlib() (in module kdrag.solvers), [1] FuncDeclRef (class in kdrag.contrib.expr) Function() (in module kdrag.contrib.expr), [1] (in module kdrag.smt), [1]

G

gappa_of_bool() (in module kdrag.solvers.gappa), [1] gappa_of_real() (in module kdrag.solvers.gappa), [1] GappaSolver (class in kdrag.solvers.gappa) ge (in module kdrag.notation) ge() (kdrag.Calc method) (kdrag.tactics.Calc method) generalize() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) generate() (in module kdrag.utils), [1] GenericProof (class in kdrag.property) get() (in module kdrag.theories.option), [1] (kdrag.property.GenericProof method) get_id() (in module kdrag.smt), [1] (kdrag.contrib.expr.AstRef method) (kdrag.contrib.expr.ExprRef method) (kdrag.contrib.expr.FuncDeclRef method) (kdrag.contrib.expr.SortRef method) (kdrag.contrib.expr.TypeVarRef method) get_lemma() (kdrag.Lemma method) (kdrag.tactics.Lemma method) get_proof() (kdrag.solvers.egraph.EGraph method) get_reg() (kdrag.contrib.pcode.BinaryContext method) get_registry() (kdrag.property.TypeClass class method) (kdrag.theories.algebra.group.AbelSemiGroup class method) (kdrag.theories.algebra.group.Group class method) (kdrag.theories.algebra.group.Monoid class method) (kdrag.theories.algebra.group.Semigroup class method) (kdrag.theories.algebra.lattice.SemiLattice class method) (kdrag.theories.algebra.ordering.PreOrder class method) (kdrag.theories.algebra.topology.Topology class method) (kdrag.theories.algebra.vector.Normed class method) (kdrag.theories.algebra.vector.VectorSpace class method)

get_regs() (kdrag.contrib.pcode.BinaryContext method) get_vars() (in module kdrag.solvers.prolog), [1] getitem (in module kdrag.notation) getvalue() (kdrag.contrib.pcode.MemState method) getvalue_ram() (kdrag.contrib.pcode.MemState method) ghost_env (kdrag.contrib.pcode.asmspec.TraceState attribute) (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) globals (kdrag.reflect.KnuckleClosure attribute) Goal (class in kdrag.tactics) goal (kdrag.tactics.Goal attribute) GR (kdrag.rewrite.Order attribute) Group (class in kdrag.theories.algebra) (class in kdrag.theories.algebra.group) gt (in module kdrag.notation) gt() (kdrag.Calc method) (kdrag.tactics.Calc method)

H

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

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

I

Id() (in module kdrag.tele), [1] id_left (kdrag.theories.algebra.group.Monoid attribute) id_right (kdrag.theories.algebra.group.Monoid attribute) Idem (class in kdrag.property) idem (kdrag.property.Idem attribute) (kdrag.theories.algebra.lattice.SemiLattice attribute) idem_norm() (in module kdrag.property), [1] Identity (class in kdrag.property) in_range() (in module kdrag.theories.float), [1] in_terms() (kdrag.solvers.egraph.EGraph method) index() (kdrag.contrib.pcode.asmspec.VerificationCondition method) (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.tactics.Goal method) induct (in module kdrag.notation) induct() (in module kdrag.theories.int), [1] (in module kdrag.theories.seq), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) induct_inductive() (in module kdrag.kernel), [1] induct_list() (in module kdrag.theories.seq), [1] induct_nat() (in module kdrag.theories.int), [1] induct_nat_strong() (in module kdrag.theories.int), [1] Inductive() (in module kdrag) (in module kdrag.kernel), [1] InductiveRel() (in module kdrag.datatype), [1] infer_sort() (in module kdrag.reflect), [1] init (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_unconstr (kdrag.contrib.yosys.VerilogModuleRel attribute) inj_lemmas() (in module kdrag.datatype), [1] Injective() (in module kdrag.theories.set), [1] input_sort (kdrag.contrib.yosys.VerilogModule attribute) inputs (kdrag.contrib.yosys.SmtModInfo attribute) install_solvers() (in module kdrag.solvers), [1] install_solvers2() (in module kdrag.solvers), [1] instan() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) instan2() (in module kdrag.kernel), [1]

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

J

Judgement (class in kdrag.kernel)

K

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

kdrag.solvers.kb.string module kdrag.solvers.ljt module kdrag.solvers.prolog module kdrag.tactics module kdrag.tele module kdrag.theories module kdrag.theories.algebra module kdrag.theories.algebra.category 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.nat module kdrag.theories.option module kdrag.theories.real module kdrag.theories.real.analysis module kdrag.theories.real.arb module kdrag.theories.real.complex module kdrag.theories.real.extended module kdrag.theories.real.geometry module kdrag.theories.real.interval module kdrag.theories.real.ndarray module kdrag.theories.real.seq module kdrag.theories.real.sympy module kdrag.theories.real.vec module kdrag.theories.regex module kdrag.theories.seq module kdrag.theories.set module kdrag.utils module key (kdrag.theories.algebra.group.AbelSemiGroup attribute) (kdrag.theories.algebra.group.Semigroup attribute) (kdrag.theories.algebra.lattice.SemiLattice attribute) (kdrag.theories.algebra.ordering.PreOrder attribute) (kdrag.theories.algebra.topology.Topology attribute) (kdrag.theories.algebra.vector.Normed attribute) (kdrag.theories.algebra.vector.VectorSpace attribute) kind() (kdrag.contrib.expr.SortRef method) KnuckleClosure (class in kdrag.reflect)

L

label (kdrag.contrib.pcode.asmspec.Assert attribute) (kdrag.contrib.pcode.asmspec.Assign attribute) (kdrag.contrib.pcode.asmspec.Assume attribute) (kdrag.contrib.pcode.asmspec.BoolStmt attribute) (kdrag.contrib.pcode.asmspec.Cut attribute) (kdrag.contrib.pcode.asmspec.Entry attribute) (kdrag.contrib.pcode.asmspec.Exit attribute) lam (kdrag.reflect.KnuckleClosure attribute) le (in module kdrag.notation) le() (kdrag.Calc method) (kdrag.tactics.Calc method) LeanSolver (class in kdrag.solvers) left() (kdrag.Lemma method) (kdrag.tactics.Lemma method) left_id (kdrag.property.Identity attribute) (kdrag.property.LeftIdentity attribute) (kdrag.theories.real.Add attribute) (kdrag.theories.real.Mul attribute) LeftIdentity (class in kdrag.property) Lemma (class in kdrag) (class in kdrag.tactics) lemma() (kdrag.property.GenericProof method) lemma_db() (in module kdrag.utils), [1] LemmaCallback (class in kdrag.tactics)

LemmaError LeoIIISolver (class in kdrag.solvers) less_le_not_le (kdrag.theories.algebra.ordering.PreOrder attribute) let() (kdrag.solvers.egglog.EgglogSolver method) lhs (kdrag.rewrite.RewriteRule attribute) limit() (in module kdrag.theories.real.sympy), [1] link() (in module kdrag.printers.c), [1] List() (in module kdrag.theories.list), [1] list() (in module kdrag.theories.list), [1] load() (kdrag.contrib.pcode.BinaryContext method) locals (kdrag.reflect.KnuckleClosure attribute) lookup() (kdrag.property.TypeClass class method) (kdrag.theories.algebra.group.AbelSemiGroup class method) (kdrag.theories.algebra.group.Group class method) (kdrag.theories.algebra.group.Monoid class method) (kdrag.theories.algebra.group.Semigroup class method) (kdrag.theories.algebra.lattice.SemiLattice class method) (kdrag.theories.algebra.ordering.PreOrder class method) (kdrag.theories.algebra.topology.Topology class method) (kdrag.theories.algebra.vector.Normed class method) (kdrag.theories.algebra.vector.VectorSpace class method) lpo() (in module kdrag.rewrite), [1] lt (in module kdrag.notation) lt() (kdrag.Calc method) (kdrag.tactics.Calc method)

M

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

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

N

n (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) name (kdrag.contrib.pcode.asmspec.Assign attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) (kdrag.kernel.Defn attribute) name() (kdrag.contrib.expr.FuncDeclRef method) (kdrag.contrib.expr.SortRef method) namedtuple_of_constructor() (in module kdrag.reflect), [1] NanoCopISolver (class in kdrag.solvers) nbe() (in module kdrag.reflect), [1]

ne (in module kdrag.notation) neg (in module kdrag.notation) newgoal() (kdrag.Lemma method) (kdrag.tactics.Lemma method) NewType() (in module kdrag) (in module kdrag.datatype), [1] NGE (kdrag.rewrite.Order attribute) Nil() (in module kdrag.theories.list), [1] no_overflow() (in module kdrag.theories.float), [1] None_() (in module kdrag.theories.option), [1] NoOverflow() (in module kdrag.theories.float), [1] 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) num_args() (in module kdrag.smt), [1] (kdrag.contrib.expr.ExprRef method)

O

occurs() (in module kdrag.utils), [1] of_datatype() (in module kdrag.printers.lean), [1] of_defn() (in module kdrag.printers.c), [1] of_expr() (in module kdrag.printers.lean), [1] of_file() (kdrag.contrib.pcode.asmspec.AsmSpec class method) of_sort() (in module kdrag.printers.lean), [1] (in module kdrag.printers.rust), [1] one (kdrag.theories.algebra.Group attribute) (kdrag.theories.algebra.Monoid attribute) one_mul (kdrag.theories.algebra.Group attribute) (kdrag.theories.algebra.Monoid attribute) open_binder() (in module kdrag.tactics), [1] (in module kdrag.tele), [1] (in module kdrag.utils), [1]

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

P

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

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

Q

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

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

R

radd (in module kdrag.notation) Range() (in module kdrag.theories.set), [1] range() (kdrag.contrib.expr.FuncDeclRef method) range_() (in module kdrag.utils), [1] read (kdrag.contrib.pcode.MemState attribute) read_yosys_relational() (in module kdrag.contrib.yosys), [1] RealSort() (in module kdrag.smt), [1] reason (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) reasons (kdrag.contrib.hoare.Hoare attribute) (kdrag.solvers.egraph.EGraph attribute) rebuild() (kdrag.solvers.egraph.EGraph method) recognizer_lemmas() (in module kdrag.datatype), [1] Refl (class in kdrag.property) refl (kdrag.property.Refl attribute) (kdrag.theories.algebra.ordering.PreOrder attribute) reflect() (in module kdrag.reflect), [1] register() (kdrag.notation.SortDispatch method) (kdrag.property.GenericProof method) (kdrag.property.TypeClass class method) (kdrag.theories.algebra.group.AbelSemiGroup class method) (kdrag.theories.algebra.group.Group class method) (kdrag.theories.algebra.group.Monoid class method) (kdrag.theories.algebra.group.Semigroup class method) (kdrag.theories.algebra.lattice.SemiLattice class method) (kdrag.theories.algebra.ordering.PreOrder class method) (kdrag.theories.algebra.topology.Topology class method) (kdrag.theories.algebra.vector.Normed class method) (kdrag.theories.algebra.vector.VectorSpace class method) registers (kdrag.contrib.yosys.SmtModInfo attribute) reify() (in module kdrag.reflect), [1] rel (in module kdrag.datatype) (kdrag.property.Antisymm attribute) (kdrag.property.Asymm attribute) (kdrag.property.Irrefl attribute) (kdrag.property.Refl attribute) (kdrag.property.Total attribute) rename_vars() (in module kdrag.kernel), [1] replace() (in module kdrag.solvers.kb.multiset), [1] (in module kdrag.solvers.kb.string), [1] res (kdrag.solvers.egglog.EgglogSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeanSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

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

S

sanity_check_consistency() (in module kdrag.utils), [1] SATSolver (class in kdrag.solvers) scalar (kdrag.theories.algebra.vector.VectorSpace attribute) search() (in module kdrag) (in module kdrag.utils), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) search_decl() (in module kdrag.utils), [1] search_expr() (in module kdrag.utils), [1] select_concat() (in module kdrag.theories.bitvec), [1] SelectConcat() (in module kdrag.theories.bitvec), [1] SemiGroup (class in kdrag.theories.algebra) Semigroup (class in kdrag.theories.algebra.group) SemiLattice (class in kdrag.theories.algebra.lattice) Seq() (in module kdrag.theories.seq), [1] seq() (in module kdrag.theories.seq), [1] series() (in module kdrag.theories.real.sympy), [1] Set() (in module kdrag.theories.set), [1] set() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) set_reg() (kdrag.contrib.pcode.BinaryContext method) setvalue() (kdrag.contrib.pcode.MemState method) setvalue_ram() (kdrag.contrib.pcode.MemState method) shim_ho() (in module kdrag.theories.real.sympy), [1] shortlex() (in module kdrag.solvers.kb.multiset), [1] shortlex_swap() (in module kdrag.solvers.kb.string), [1] show() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sig (kdrag.tactics.Goal attribute) simp() (in module kdrag) (in module kdrag.rewrite), [1] (in module kdrag.tactics), [1] (in module kdrag.theories.real.sympy), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) simp1() (in module kdrag.rewrite), [1] simp2() (in module kdrag.rewrite), [1] simp_tac() (in module kdrag.tactics), [1] simplify() (in module kdrag.solvers.kb), [1] (in module kdrag.solvers.kb.string), [1] (in module kdrag.theories.real.sympy), [1] simplify_terms() (kdrag.solvers.egraph.EGraph method) SimState (class in kdrag.contrib.pcode) sin_bnd() (in module kdrag.theories.real.arb), [1] sin_lower() (in module kdrag.theories.real), [1] Singleton() (in module kdrag.theories.set), [1] skip() (kdrag.contrib.hoare.Hoare class method) skolem() (in module kdrag.kernel), [1]

smt2tptp() (in module kdrag.solvers), [1] smt_datatype_val() (in module kdrag.hypothesis), [1] smt_generic_val() (in module kdrag.hypothesis), [1] smt_metadata() (in module kdrag.contrib.yosys), [1] smt_seq_val() (in module kdrag.hypothesis), [1] smtlib_datatypes() (in module kdrag.solvers), [1] SmtModInfo (class in kdrag.contrib.yosys) 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.theories.real.sympy), [1] solver (kdrag.solvers.egraph.EGraph attribute) solver_classes (kdrag.solvers.MultiSolver attribute) Some() (in module kdrag.theories.option), [1] sort() (in module kdrag.smt), [1] sort_axiom() (in module kdrag.printers.lean), [1] sort_kind() (in module kdrag.smt), [1] sort_occurs() (in module kdrag.hypothesis), [1] sort_of_type() (in module kdrag.reflect), [1] sort_to_tptp() (in module kdrag.solvers), [1] SortDispatch (class in kdrag.notation) SortRef (class in kdrag.contrib.expr) sorts() (in module kdrag.utils), [1] split() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sqrt_bnd() (in module kdrag.theories.real), [1] sqrt_lower() (in module kdrag.theories.real), [1] sqrt_upper() (in module kdrag.theories.real), [1] start (kdrag.contrib.pcode.asmspec.TraceState attribute) (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) state (kdrag.contrib.pcode.asmspec.TraceState attribute) state_sort (kdrag.contrib.yosys.VerilogModule attribute) (kdrag.contrib.yosys.VerilogModuleRel attribute) 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] subseq() (in module kdrag.solvers.kb.string), [1] subset() (in module kdrag.theories.set), [1] subsort_domain() (in module kdrag.tele), [1] subst() (in module kdrag.kernel), [1] (in module kdrag.tactics), [1] subst_funs_body (kdrag.kernel.Defn attribute) substitute() (in module kdrag.contrib.pcode.asmspec), [1] (kdrag.contrib.pcode.BinaryContext method) substitute_fresh_vars() (in module kdrag.kernel), [1] substitute_ghost() (in module kdrag.contrib.pcode.asmspec), [1] subterms() (in module kdrag.utils), [1] successes (kdrag.contrib.pcode.asmspec.Results attribute) sum_shim() (in module kdrag.theories.real.sympy), [1] summation() (in module kdrag.theories.real.sympy), [1] Surjective() (in module kdrag.theories.set), [1] sym_execute() (kdrag.contrib.pcode.BinaryContext method) symm() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sympify() (in module kdrag.theories.real.sympy), [1]

T

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

top_goal() (kdrag.Lemma method) (kdrag.tactics.Lemma method) Topology (class in kdrag.theories.algebra.topology) Total (class in kdrag.property) total (kdrag.property.Total attribute) tptp2smt() (in module kdrag.solvers), [1] trace (kdrag.contrib.pcode.asmspec.TraceState attribute) (kdrag.contrib.pcode.asmspec.VerificationCondition attribute) TraceState (class in kdrag.contrib.pcode.asmspec) trans (kdrag.contrib.yosys.VerilogModuleRel attribute) (kdrag.theories.algebra.ordering.PreOrder attribute) trans_fun (kdrag.contrib.yosys.VerilogModule attribute) translate() (kdrag.contrib.pcode.BinaryContext method) translate_tuple_args() (in module kdrag.theories.real.sympy), [1] TweeSolver (class in kdrag.solvers) type_of_sort() (in module kdrag.reflect), [1] TypeClass (class in kdrag.property) TypeVarRef (class in kdrag.contrib.expr)

U

uf (kdrag.solvers.egraph.EGraph attribute) unfold() (in module kdrag.kernel), [1] (in module kdrag.rewrite), [1] (kdrag.contrib.pcode.BinaryContext method) (kdrag.Lemma method) (kdrag.tactics.Lemma method) unfold_old() (in module kdrag.rewrite), [1] unify() (in module kdrag.utils), [1] unify_db() (in module kdrag.utils), [1] union() (in module kdrag.theories.set), [1] (kdrag.solvers.egraph.EGraph method) Unit() (in module kdrag.theories.list), [1] (in module kdrag.theories.seq), [1]

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

V

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

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

W

weaken_post() (kdrag.contrib.hoare.Hoare method) wf (in module kdrag.notation) when() (kdrag.notation.Cond method) wires (kdrag.contrib.yosys.SmtModInfo attribute) (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] write (kdrag.contrib.pcode.MemState attribute) write_smt() (kdrag.solvers.BaseSolver method) (kdrag.solvers.egglog.EgglogSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeanSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

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

X

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

Y

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

Z

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

z3_array_val() (in module kdrag.hypothesis), [1] z3_mid_rad_of_arb() (in module kdrag.theories.real.arb), [1] z3_of_exact_arb() (in module kdrag.theories.real.arb), [1] z3_to_egglog() (in module kdrag.solvers.egglog), [1] zero (kdrag.theories.algebra.vector.VectorSpace attribute) zero_add (in module kdrag.theories.algebra.vector) ZipperpositionSolver (class in kdrag.solvers)