List of all items
Structs
- DerivationTree
- InductionArg
- InductionCase
- MatchArm
- ProofGoal
- affine::Affine
- affine::AffineCanonical
- affine_gfp::AffineP
- affine_gfp::AffinePCanonical
- ait::AffineReduction
- ait::AffineSignature
- ait::AlgebraicAttack
- ait::AlgebraicImmunityReport
- ait::BooleanCensus
- ait::Budget
- ait::CombinerLeak
- ait::CompressibilityReport
- ait::CoverageCensus
- ait::DeepStructureReport
- ait::DescriptionBound
- ait::InvarianceReduction
- ait::KolmogorovBound
- ait::LensCoverage
- ait::LensReport
- ait::LinearDistinguisher
- ait::LinearRigidityCert
- ait::LinearStructureCert
- ait::LinearStructureReport
- ait::RecursiveReduction
- ait::SampledCensus
- ait::SboxProfile
- ait::SboxSpectra
- ait::SeparableDecomposition
- ait::StructuralBound
- ait::StructureCover
- ait::StructureReport
- ait::VariableSymmetry
- category_collapse::Reduction
- cdcl::LearnedClause
- cdcl::Lit
- cdcl::Solver
- census::AglCollapse
- census::AglWitness
- census::CoverageSummary
- census::MenuSplit
- census::OrbitRecord
- census::ResidueMap
- census::StructureAccounting
- certifier::CertificationContext
- cnf::Cnf
- coalgebra::TransitionSystem
- cofactor::CofactorIso
- cofactor::GroupInduced
- cofactor::QuotientDag
- cofactor::Raw
- cofactor::ReduceIso
- cofactor::Rename
- cofactor::StructuredDag
- cofactor::StructuredReduceIso
- cofactor::UnitPropIso
- complexity::RankedRefutation
- complexity::SizeBound
- counting_principle::CountingCert
- cubical::Cube
- cubical::CubicalComplex
- cyclotomic::Cyclo
- cyclotomic::LogUnitAudit
- development::Development
- dimacs::DimacsCnf
- discrimination::DiscTree
- elliptic::Curve
- elliptic::Isogeny
- elliptic::IsogenyStep
- engine::BackwardChainer
- factor::StructuralBudget
- factor::StructuralWitness
- formula::FormulaError
- fp2::Curve2
- fp2::Isogeny2
- fp2::IsogenyStep2
- fp2::SsVertex
- gf2::SolutionSpace
- groupoid::ActionGroupoid
- hints::SocraticHint
- hornsat::HornClause
- hypercube::AbstractRefutation
- hypercube::AdvanceStep
- hypercube::CarveStats
- hypercube::CollapseStep
- hypercube::Cover
- hypercube::CubeSym
- hypercube::Diagnosis
- hypercube::FamilySignature
- hypercube::LadderStats
- hypercube::RuleSymmetry
- hypercube::StructuralProfile
- hypercube::Subcube
- hyperelliptic::MatchedPairGlue
- hyperelliptic::Mumford
- hyperelliptic::Richelot
- hyperelliptic::SplitGenus2
- interval_sched::Interval
- isogeny::KaniDiamond
- isogeny::KaniGlue
- isogeny::SecretRecovery
- isogeny::TorsionImageWitness
- lemma_index::LemmaIndex
- lemma_index::Suggestion
- linarith_solve::LinExpr
- lll::LllSatCert
- lyapunov::CardinalitySeams
- lyapunov::CollapsingMeasure
- lyapunov::CoveringMeasure
- lyapunov::LyapunovCertificate
- lyapunov::PartialCoveringMeasure
- lyapunov::SymmetryTheory
- matching::CapHallWitness
- matching::HallWitness
- modm::SolutionSpaceM
- modp::ModpEquation
- modp::ModpRecovery
- modp::SolutionSpaceP
- optimize::MinResult
- orbit_stability::CollapsedDual
- orbit_stability::FittedCount
- orbit_stability::ForAllVerdict
- orbit_stability::StabilizedSystem
- orbit_stability::SymmetricInstance
- ordering::OrderingCert
- permgroup::Bsgs
- permgroup::CharacterTable
- pigeonhole::CountingCert
- polycalc::NsCertificate
- polycalc_gfp::NsCertificateGfp
- polycalc_zm::NsCertificateZm
- progress_complex::ProgressComplex
- progress_complex::ProgressComplex3
- proof::Perm
- proof_emit::SizeSink
- proof_rewrite::ProofPoset
- pseudo_boolean::CardinalityTheory
- pseudo_boolean::PbConstraint
- register_alloc::LiveRange
- rule_search::Rule
- rule_search::RuleSet
- rule_search::SearchStats
- simp::SimpSet
- solve::Solved
- solve::SymmetricCount
- solve::SymmetryProfile
- sym_certify::CertifiedRefutation
- symmetry_detect::AutomorphismIndex
- tactic::CtorSpec
- tactic::Goal
- tactic::Hyp
- tactic::ProofState
- tactic_script::ScriptError
- tactic_script::ScriptedTheorem
- tactic_script::TacticEnv
- trace_determinism::Op
- two_group::CrossedModule
- two_group::FiniteGroup
- twosat::Lit
- verify::ConflictReport
- verify::Definition
- verify::DependencyGraph
- verify::LibraryResult
- verify::LibraryTheorem
- verify::VerifiedProof
- xor_engine::IncXor
- xor_engine::XorEngine
- xorsat::XorEquation
Enums
- InferenceRule
- ProofExpr
- ProofTerm
- affine::AffineCanon
- affine::AffineOutcome
- affine_gfp::AffinePCanon
- affine_gfp::AffinePForced
- ait::CompressibilityClass
- ait::CryptoStrength
- ait::CubeStructure
- ait::Descriptor
- ait::LinearShortcut
- ait::Refusal
- ait::RsaAuditVerdict
- ait::RsaStrength
- ait::SboxVerdict
- ait::StructureTree
- bmc::BmcOutcome
- bmc::InductionOutcome
- bmc::VacuityOutcome
- cdcl::BudgetedResult
- cdcl::RestartMode
- cdcl::SolveResult
- cofactor::Node
- cofactor::QNode
- cofactor::SNode
- counterexample::Counterexample
- dimacs::DimacsError
- elliptic::CurveWeakness
- elliptic::Point
- error::ProofError
- families::ExpectedVerdict
- fp2::Point2
- hints::SuggestedTactic
- hornsat::HornOutcome
- hypercube::AdvanceStatus
- hypercube::CarveOutcome
- hypercube::CoverVerdict
- hypercube::ProofRung
- hypercube::SearchCost
- hypercube::Shadow
- hyperelliptic::GuidedWalk
- inprocess::EquivResult
- interval_sched::ScheduleOutcome
- isogeny::RecoveryLaw
- isogeny::SidhAudit
- lyapunov::AutoCollapse
- matching::CapMatchOutcome
- matching::MatchOutcome
- modm::AllowedOutcome
- modm::ForcedM
- modm::ModmOutcome
- modm::PrimePowerSpace
- modp::ModpOutcome
- polycalc_gfp::NsField
- proof::ProofStep
- proof::Witness
- proof_emit::EmitError
- register_alloc::Allocation
- res_width::WidthConvention
- rule_search::RuleKind
- rule_search::Safety
- rup::Verdict
- sat::EquivOutcome
- sat::ModelOutcome
- sat::UnsatOutcome
- sdcl::CertifiedOutcome
- solve::Answer
- solve::EquivVerdict
- solve::Route
- steenrod::AdamsFact
- sym_dynamic::SelOutcome
- tactic::TacticError
- twosat::TwoSatOutcome
- xor_engine::XorStep
- xorsat::XorOutcome
Traits
Functions
- affine::affine_canonicalize
- affine::affine_reduce
- affine::affine_refutation_drat
- affine::affine_subspace_agl_order
- affine::affine_symmetries
- affine::agl_order
- affine::all_affine_bijections
- affine::models_of
- affine::recover_linear_system
- affine_gfp::affine_m_canonicalize
- affine_gfp::affine_m_forced
- affine_gfp::affine_p_canonicalize
- affine_gfp::affine_p_forced
- affine_gfp::affine_p_refutation_drat
- affine_gfp::affine_p_symmetries
- affine_gfp::agl_m_order
- affine_gfp::agl_p_order
- affine_gfp::all_affine_p_bijections
- affine_gfp::models_p
- ait::affine_reduce
- ait::affine_signature
- ait::algebraic_attack_on_bytes
- ait::algebraic_filter_attack
- ait::algebraic_immunity_of
- ait::assess_key_material
- ait::attack_shrinking_generator
- ait::boolean_function_census
- ait::boomerang_uniformity
- ait::census
- ait::certified_incompressible_function_exists
- ait::certify_linear_rigidity
- ait::certify_linear_rigidity_within
- ait::certify_linear_structure
- ait::check_linear_rigidity
- ait::check_linear_structure
- ait::classify_bytes
- ait::classify_int_seq
- ait::classify_text
- ait::exhaustive_coverage
- ait::fast_correlation_attack
- ait::find_structure
- ait::find_structure_deep
- ait::gf256_word_complexity
- ait::incompressibility_gate
- ait::incompressibility_ratio
- ait::incompressible_string_exists
- ait::kolmogorov_bound
- ait::lens_report
- ait::linear_cryptanalysis
- ait::linear_shortcut_verdict
- ait::linear_structures
- ait::maximal_order_complexity_of_bytes
- ait::recursive_reduce
- ait::reduce_by_invariance
- ait::rsa_full_audit
- ait::rsa_structural_audit
- ait::sampled_boolean_census
- ait::sbox_full_audit
- ait::sbox_profile
- ait::sbox_spectra
- ait::scan_for_combiner_leaks
- ait::separable_decomposition
- ait::structural_bound
- ait::structure_cover
- ait::structure_tree
- ait::two_adic_complexity_of_bytes
- ait::variable_symmetry
- arith::prove_int_eq
- bmc::check_vacuity
- bmc::find_counterexample
- bmc::find_counterexample_incremental
- bmc::find_counterexample_symmetric
- bmc::prove_invariant
- bmc::temporal_symmetry_pairs
- cardinality::at_least
- cardinality::at_most
- cardinality::exactly
- category_collapse::iso
- category_collapse::refines
- category_collapse::transfer
- census::affine_composite_shear_generators
- census::affine_transvection_generators
- census::agl_collapse_exact
- census::agl_collapse_via_transvections
- census::census
- census::clause_agl_symmetries
- census::coverage_summary
- census::extended_rung
- census::family_census
- census::family_growth
- census::family_of_types
- census::family_tower
- census::find_agl_witness
- census::generic_subfamilies
- census::max_ns_degree_at
- census::menu_split
- census::named_giants
- census::realized_tower_families
- census::residue_map
- census::structure_accounting
- census::symplectic_transvection_generators
- census::witness_counting
- census::witness_parity
- census::witness_unit_propagation
- certifier::certify
- cnf::cdcl_entails
- coalgebra::canonical_countdown_morphism
- coalgebra::is_countdown_morphism
- coalgebra::is_well_founded
- cofactor::apply_twist
- cofactor::canon
- cofactor::canon_raw
- cofactor::check_distinct_dag
- cofactor::check_quotient_dag
- cofactor::check_structured_dag
- cofactor::cofactor
- cofactor::cofactor_set
- cofactor::distinct_cofactor_dag
- cofactor::distinct_width
- cofactor::group_canon
- cofactor::is_leaf
- cofactor::iso_canon
- cofactor::level_widths
- cofactor::normalize
- cofactor::quotient_class_count
- cofactor::quotient_dag
- cofactor::quotient_width
- cofactor::reduce
- cofactor::structured_leaf
- cofactor::structured_leaf_dag
- cofactor::unit_propagate
- complexity::certify_size_bound
- counterexample::find_counterexample
- counting_principle::counting_certificate
- counting_principle::refute_counting
- cyclotomic::approximation_scale
- cyclotomic::audit_log_unit
- cyclotomic::cyclotomic_units
- cyclotomic::galois_group
- cyclotomic::recover_short_generator
- cyclotomic::recovery_margin
- development::parse_development
- development::prove_development
- dimacs::parse
- dimacs::print
- eilenberg_maclane::homology_size
- eilenberg_maclane::homotopy_group_size
- eilenberg_maclane::is_omega_spectrum
- eilenberg_maclane::stable_homotopy
- elliptic::curve_security
- elliptic::derive_isogeny_path
- elliptic::ecdlp_bsgs
- elliptic::ecm
- elliptic::ecm_factor
- elliptic::ecm_two_stage
- elliptic::kernel_generator
- elliptic::ladder
- elliptic::point_of_order
- elliptic::torsion_basis
- elliptic::weil_pairing
- elliptic::xadd
- elliptic::xdbl
- factor::batch_gcd
- factor::boneh_durfee
- factor::common_modulus_attack
- factor::coppersmith_factor_high_bits
- factor::crt
- factor::dixon_factor
- factor::factor_via_private_exponent
- factor::fermat
- factor::franklin_reiter_attack
- factor::gcd
- factor::hastad_broadcast_attack
- factor::integer_nth_root
- factor::is_probable_prime
- factor::isqrt
- factor::low_exponent_message
- factor::mod_inverse
- factor::modpow
- factor::next_prime
- factor::pollard_p_minus_1
- factor::pollard_rho
- factor::quadratic_sieve
- factor::rsa_private_exponent
- factor::structural_factor
- factor::trial_division
- factor::verify_factorization
- factor::wiener
- families::clique_coloring
- families::functional_php
- families::grid_tseitin
- families::ksat_threshold_first_moment_upper
- families::mod_counting
- families::mod_counting_edges
- families::mod_counting_groups
- families::mod_m_tseitin_expander
- families::mod_p_consistent_onehot
- families::mod_p_tseitin_expander
- families::mutilated_chessboard
- families::onto_php
- families::ordering_principle
- families::parity_exactly_one
- families::parity_unsat
- families::pebbling_pyramid
- families::php
- families::ramsey
- families::ramsey_number
- families::random_3sat
- families::random_ksat
- families::random_kxor
- families::tseitin_expander
- families::weak_php
- formula::parse_formula
- fp2::aut_1728
- fp2::derive_isogeny_path2
- fp2::fp2_add
- fp2::fp2_const
- fp2::fp2_inv
- fp2::fp2_is_zero
- fp2::fp2_mul
- fp2::fp2_neg
- fp2::fp2_pow
- fp2::fp2_sqrt
- fp2::fp2_sub
- fp2::full_order_basis2
- fp2::isogeny_graph_distances
- fp2::kernel_generator2
- fp2::keyspace_codomain_classes
- fp2::point_of_order2
- fp2::point_order2
- fp2::product_weil_pairing
- fp2::push_through2
- fp2::recover_secret2
- fp2::recover_secret_pruned2
- fp2::recover_secret_recursive2
- fp2::supersingular_graph
- fp2::torsion_basis2
- fp2::weil_pairing2
- gf2::count_invertible_gf2_bruteforce
- gf2::gl_order
- gf2::invertibility_density
- gf2::is_invertible_gf2
- gf2::solve_gf2
- grid_solver::grid_prove
- grounding::at_most_one_lemmas
- grounding::column_closure_lemmas
- grounding::definite_property_implications
- grounding::discharge_unary_facts
- grounding::domain_constants
- grounding::functionality_lemmas
- grounding::ground
- grounding::ground_problem
- grounding::ground_problem_sorted
- grounding::ground_sorted
- grounding::simplify_trivial_identities
- grounding::sort_domains
- hints::suggest_hint
- hornsat::is_refutation
- hornsat::satisfies
- hornsat::solve
- hypercube::abstract_signature
- hypercube::applicable_levers
- hypercube::apply_perm_to_model
- hypercube::apply_renaming
- hypercube::auto_advance
- hypercube::autocarve
- hypercube::autocarve_measured
- hypercube::automorphism_group_size
- hypercube::backdoor_branch_orbit_count
- hypercube::blocker_orbit
- hypercube::bounded_variable_elimination
- hypercube::burnside_corner_orbits
- hypercube::burnside_orbit_count
- hypercube::canonical_blocker
- hypercube::canonical_cover
- hypercube::canonical_model
- hypercube::carve
- hypercube::clause_orbits
- hypercube::clauses_to_expr
- hypercube::collapse_curve
- hypercube::components
- hypercube::crush
- hypercube::cube_group_closure
- hypercube::decide_2sat
- hypercube::decide_laddered
- hypercube::decide_laddered_nocut
- hypercube::decide_laddered_sym
- hypercube::decide_sat_via_2sat_backdoor
- hypercube::decompose_and_crush
- hypercube::diagnose
- hypercube::eliminate_variable
- hypercube::face_vector
- hypercube::find_random_core
- hypercube::greedy_2sat_backdoor
- hypercube::hyperoctahedral_generators
- hypercube::is_antipodally_symmetric
- hypercube::is_strong_backdoor_to_2sat
- hypercube::is_total_via_orbits
- hypercube::min_resolution_width
- hypercube::minimal_cover_orbits
- hypercube::model_orbit
- hypercube::orbit_count
- hypercube::orbit_representatives
- hypercube::partition_into_orbits
- hypercube::perm_group_closure
- hypercube::php_cover
- hypercube::php_perm_symmetries
- hypercube::php_symmetries
- hypercube::pigeonhole_abstract_refutation
- hypercube::pigeonhole_rule_symmetry
- hypercube::pure_literal_reduce
- hypercube::renaming_to_horn
- hypercube::restrict
- hypercube::search_cost
- hypercube::search_cost_antipodal
- hypercube::stabilizer
- hypercube::structural_profile
- hypercube::symmetric_resolution_closure
- hypercube::symmetric_resolution_growth
- hypercube::symmetry_entropy_bits
- hypercube::walsh_hadamard_energy
- hypercube::weakest_crushing_rung
- hypercube::weakest_crushing_rung_with_char
- hypercube::witness_perspective
- hyperelliptic::cantor_add
- hyperelliptic::count_curve_fp
- hyperelliptic::find_split_neighbour
- hyperelliptic::genus2_jacobian_order
- hyperelliptic::genus2_jacobian_order_general
- hyperelliptic::glue_shared_2torsion
- hyperelliptic::guided_chain
- hyperelliptic::jac_element_order
- hyperelliptic::jac_identity
- hyperelliptic::jac_negate
- hyperelliptic::jac_scalar_mul
- hyperelliptic::poly_deriv
- hyperelliptic::poly_eval
- hyperelliptic::poly_mul
- hyperelliptic::richelot
- hyperelliptic::richelot_chain
- hyperelliptic::richelot_partitions
- hyperelliptic::select_splitting_branch
- hyperelliptic::split_jacobian_from_cubic
- hyperelliptic::surface_is_reducible
- inprocess::bucket_elimination_refute
- inprocess::bve
- inprocess::eliminate_variable
- inprocess::equivalent_literal_scc
- inprocess::vivify
- inprocess::vivify_clause
- interval_sched::is_overflow_witness
- interval_sched::is_valid_schedule
- interval_sched::peak_concurrency
- interval_sched::schedule_or_overflow
- isogeny::audit
- isogeny::build_kani_diamond
- isogeny::build_kani_glue
- isogeny::certify_isogeny
- isogeny::certify_recovery
- isogeny::is_smooth
- isogeny::kani_diamond_degrees
- kan_complex::inner_horns_fill_uniquely
- kan_complex::kan_fills
- kan_complex::nerve_cohomology_size
- lattice::lll_reduce
- lattice::lll_reduce_bigint
- lattice::lll_reduce_bigint_exact
- lattice::lll_reduce_bigint_fp
- linarith_solve::combine
- linarith_solve::find_farkas
- linarith_solve::parse_lin
- lll::lll_certifies_sat
- lll::lll_dependency_degree
- lll::moser_tardos_witness
- lyapunov::affine_parity_symmetries
- lyapunov::all_transposition_symmetries
- lyapunov::auto_collapse
- lyapunov::cardinality_collapse
- lyapunov::cardinality_parity_seams
- lyapunov::cardinality_symmetry_break
- lyapunov::cardinality_symmetry_generators
- lyapunov::compose_collapses
- lyapunov::covering_collapse
- lyapunov::cutting_planes_lyapunov
- lyapunov::extract_xor
- lyapunov::fused_parity_cardinality_decide
- lyapunov::fused_permutation_generators
- lyapunov::fused_symmetry_group
- lyapunov::gaussian_lyapunov
- lyapunov::lyapunov_of_symmetry
- lyapunov::proof_from_measure
- lyapunov::proof_induced_measure
- lyapunov::recover_at_most_k
- lyapunov::recover_at_most_one
- lyapunov::recover_cardinality_constraints
- lyapunov::recover_cardinality_substructure
- lyapunov::solve_by_measure_synthesis
- lyapunov::synthesize_measure
- lyapunov::verify_lyapunov
- matching::assign_or_hall
- matching::assign_or_hall_capacitated
- matching::is_cap_hall_witness
- matching::is_hall_witness
- matching::is_valid_assignment
- modm::allowed_residues
- modm::cycle_system
- modm::forced_values_prime_power
- modm::forced_values_squarefree
- modm::is_refutation
- modm::prime_power_factorize
- modm::satisfies
- modm::solve
- modm::solve_prime_power
- modm::solve_space_prime_power
- modm::solve_squarefree
- modm::squarefree_primes
- modp::cycle_system
- modp::gl_order_p
- modp::invertibility_density_p
- modp::is_invertible_modp
- modp::is_prime
- modp::is_refutation
- modp::recover_from_cnf
- modp::satisfies
- modp::solve
- modp::solve_space
- optimize::minimize_certified
- orbit_stability::canonical_structure
- orbit_stability::collapsed_dual_system
- orbit_stability::count_instance_linear
- orbit_stability::count_instance_linear_marked
- orbit_stability::decide_invariant_witness_for_all_scales
- orbit_stability::invariant_witness_exists_direct
- orbit_stability::labeled_dual_counts
- orbit_stability::monomial_orbits_bounded
- orbit_stability::php_instance_clause
- orbit_stability::php_instance_linear
- orbit_stability::php_instance_linear_marked_hole
- orbit_stability::php_instance_linear_marked_pigeon
- ordering::check_ordering_cert
- ordering::ordering_certificate
- ordering::refute_ordering
- ordering::refutes_ordering_principle
- parity_cardinality::refute
- period::factor_from_order
- period::factor_via_order
- period::multiplicative_order
- permgroup::abelianization
- permgroup::automorphism_group_order
- permgroup::burnside_ring_product
- permgroup::center_order
- permgroup::character_table
- permgroup::class_multiplication_coefficients
- permgroup::composition_factor_orders
- permgroup::conjugacy_classes
- permgroup::cycle_index
- permgroup::derived_length
- permgroup::derived_subgroup
- permgroup::element_orders
- permgroup::exponent
- permgroup::frobenius_schur_from_table
- permgroup::frobenius_schur_indicators
- permgroup::galois_class_orbits
- permgroup::generating_tuple_count
- permgroup::irreducible_degrees
- permgroup::is_abelian
- permgroup::is_nilpotent
- permgroup::is_primitive
- permgroup::is_primitive_via_orbitals
- permgroup::is_simple
- permgroup::is_solvable
- permgroup::isotypic_from_table
- permgroup::isotypic_multiplicities
- permgroup::minimal_block_system
- permgroup::mobius_number
- permgroup::nilpotency_class
- permgroup::orbitals
- permgroup::orbits
- permgroup::orbits_on_tuples
- permgroup::outer_automorphism_order
- permgroup::pattern_inventory
- permgroup::permutation_character
- permgroup::permutation_character_decomposition
- permgroup::polya_count
- permgroup::rank
- permgroup::rational_class_count
- permgroup::real_class_count
- permgroup::schreier_sims
- permgroup::subgroup_count
- permgroup::sylow_counts
- permgroup::table_of_marks
- permgroup::tensor_decomposition
- permgroup::tensor_from_table
- permgroup::transitivity_degree
- permgroup::upper_central_length
- permgroup::upper_central_series
- pigeonhole::certify_pigeonhole_unsat
- pigeonhole::check_counting_cert
- pigeonhole::counting_certificate
- pigeonhole::decide_pigeonhole_unsat
- pigeonhole::hall_refutation
- polycalc::build_ns_certificate
- polycalc::check_ns_lower_bound
- polycalc::check_ns_lower_bound_polys
- polycalc::clause_polynomial
- polycalc::exactly_one_linear_generators
- polycalc::monomial_orbits
- polycalc::monomials_up_to_degree
- polycalc::ns_lower_bound_witness
- polycalc::ns_lower_bound_witness_on_basis
- polycalc::ns_lower_bound_witness_polys
- polycalc::ns_lower_bound_witness_polys_on_basis
- polycalc::ns_refutes_polys
- polycalc::nullstellensatz_basis_size
- polycalc::nullstellensatz_refutes
- polycalc::nullstellensatz_refutes_symmetric
- polycalc::partition_of_unity
- polycalc::php_is_hole_injective
- polycalc::php_is_partial_matching
- polycalc::poly_degree
- polycalc::polynomial_calculus_refutes
- polycalc::pou_as_product
- polycalc::pou_atom
- polycalc::symmetric_group_generators
- polycalc_gfp::build_ns_certificate_gfp
- polycalc_gfp::check_ns_lower_bound_gfp
- polycalc_gfp::check_ns_lower_bound_polys_gfp
- polycalc_gfp::clause_polynomial_gfp
- polycalc_gfp::exactly_one_linear_generators_gfp
- polycalc_gfp::gfp_poly_degree
- polycalc_gfp::gfp_solve
- polycalc_gfp::ns_certificate_at_degree_gfp
- polycalc_gfp::ns_lower_bound_witness_gfp
- polycalc_gfp::ns_lower_bound_witness_on_basis_gfp
- polycalc_gfp::ns_lower_bound_witness_polys_gfp
- polycalc_gfp::ns_refutes_gfp
- polycalc_gfp::ns_refutes_polys_gfp
- polycalc_gfp::partition_of_unity_gfp
- polycalc_gfp::pou_atom_gfp
- polycalc_gfp::project_gf4_certificate_to_gf2
- polycalc_gfp::reynolds_gfp
- polycalc_gfp::symmetrize_gfp
- polycalc_zm::build_ns_certificate_zm
- polycalc_zm::check_ns_lower_bound_polys_zm
- polycalc_zm::check_ns_lower_bound_zm
- polycalc_zm::clause_polynomial_zm
- polycalc_zm::lift_prime_witness_to_zm
- polycalc_zm::ns_refutes_polys_zm
- polycalc_zm::ns_refutes_zm
- polycalc_zm::partition_of_unity_zm
- polycalc_zm::pou_atom_zm
- polycalc_zm::zm_poly_degree
- postnikov::bockstein
- postnikov::coboundary
- postnikov::cohomology_size
- postnikov::cup
- postnikov::cup_cube_z2
- postnikov::cup_power_z2
- postnikov::cup_square
- postnikov::is_coboundary
- postnikov::is_cocycle
- pr::check_pr_refutation
- pr::check_pr_refutation_fast
- pr::is_pr
- pr::is_pr_indexed
- proof_emit::check_lrat
- proof_emit::emit_dpr
- proof_emit::emit_drat
- proof_emit::emit_lrat
- proof_emit::emit_sr
- proof_emit::parse_dpr
- proof_emit::try_assignment_witness
- proof_emit::write_sr
- proof_rewrite::disjoint_double_contradiction
- proof_rewrite::permutations
- pseudo_boolean::coeff_symmetry_generators
- pseudo_boolean::is_pb_symmetry
- pseudo_boolean::php_refutation
- pseudo_boolean::refute_clausal
- register_alloc::allocate
- register_alloc::is_spill_certificate
- register_alloc::is_valid_allocation
- register_alloc::register_pressure
- res_width::check_res_width_lower_bound
- res_width::mask_clause
- res_width::mask_width
- res_width::min_res_width_clauses
- res_width::resolution_width_closure
- res_width::resolve_masks
- res_width::width_refutes
- rule_search::default_ruleset
- rup::check_refutation
- rup::entails_certified
- rup::entails_certified_prepared
- sat::decode_model
- sat::decode_model_from
- sat::find_model
- sat::prove_equivalence
- sat::prove_unsat
- sat::prove_unsat_certified
- satcli::run
- sdcl::find_pr_clause
- sdcl::find_pr_clause_unified
- sdcl::plain_cdcl_refutation
- sdcl::sdcl_refute
- sdcl::solve_certified
- solve::almost_symmetry_pairs
- solve::assignment_weight_inventory
- solve::association_scheme_eigenmatrix
- solve::association_scheme_multiplicities
- solve::automorphism_group_order
- solve::break_all_symmetry
- solve::break_all_symmetry_complete
- solve::burnside_ring_product
- solve::canonical_form
- solve::character_table
- solve::class_algebra_constants
- solve::coherent_configuration_constants
- solve::coherent_rank
- solve::color_refinement
- solve::color_refinement_cells
- solve::common_automorphism_generators
- solve::equivalence_check_counts
- solve::equivalent_modulo_symmetry
- solve::formulas_isomorphic
- solve::fractional_automorphism
- solve::frobenius_schur_indicators
- solve::galois_class_orbits
- solve::generating_tuple_count
- solve::is_fractional_automorphism
- solve::isotypic_multiplicities
- solve::mine_clauses
- solve::mobius_number
- solve::models_up_to_symmetry
- solve::optimization_symmetry_generators
- solve::optimize_enumeration_counts
- solve::optimize_modulo_symmetry
- solve::pb_symmetry_profile
- solve::permutation_character
- solve::permutation_character_decomposition
- solve::provably_asymmetric_variables
- solve::semantic_symmetry_pairs
- solve::solve_by_components
- solve::solve_by_symmetry_breaking
- solve::solve_comprehensive
- solve::solve_structured
- solve::solve_with_declared_symmetry
- solve::structured_prefix
- solve::symmetry_structure
- solve::table_of_marks
- solve::tensor_decomposition
- solve::three_wl_colors
- solve::three_wl_fingerprint
- solve::two_wl_fingerprint
- solve::two_wl_pair_cells
- solve::two_wl_pair_colors
- solve::weighted_model_count
- solve::weighted_model_count_solve_counts
- sos::check_sos_certificate
- sos::sos_certificate
- sos::sos_refutes
- steenrod::act_monomial
- steenrod::adams_one_line
- steenrod::adams_two_line
- steenrod::adem_reduce
- steenrod::admissibles_of_degree
- steenrod::apply_sq
- steenrod::ext
- steenrod::harvest_adams_facts
- steenrod::harvest_secondary_facts
- steenrod::is_admissible
- steenrod::is_decomposable_sq
- steenrod::monomial
- steenrod::sq
- steenrod::total_square
- steenrod::yoneda_product
- sym_break::affine_lex_leader_sbp
- sym_break::conditional_symmetry_generators
- sym_break::count_models_modulo_symmetry
- sym_break::hierarchical_break
- sym_break::is_lex_leader
- sym_break::is_lex_leader_lit
- sym_break::lex_leader_sbp
- sym_break::lex_leader_sbp_lit
- sym_break::literal_automorphism_generators
- sym_break::literal_automorphism_group
- sym_break::litsym_from_points
- sym_break::litsym_to_points
- sym_break::variable_automorphism_generators
- sym_break::variable_automorphism_group
- sym_certify::certified_unsat
- sym_certify::certified_unsat_auto
- sym_certify::certified_unsat_lex
- sym_certify::heule_clique_ranked
- sym_certify::heule_clique_refutation
- sym_certify::heule_php_ranked
- sym_certify::heule_php_refutation
- sym_certify::lex_leader_clauses
- sym_certify::symmetry_break_certified
- sym_dynamic::sel_refute
- symmetry::break_symmetries
- symmetry::lex_le
- symmetry_detect::aut_order
- symmetry_detect::automorphism_group
- symmetry_detect::find_generators
- symmetry_detect::perm_is_automorphism
- tactic::combinators::all_goals
- tactic::combinators::assumption
- tactic::combinators::auto
- tactic::combinators::cases
- tactic::combinators::crush
- tactic::combinators::decide
- tactic::combinators::exact
- tactic::combinators::exists
- tactic::combinators::first
- tactic::combinators::induction
- tactic::combinators::induction_over
- tactic::combinators::intro
- tactic::combinators::left
- tactic::combinators::omega
- tactic::combinators::repeat
- tactic::combinators::rewrite
- tactic::combinators::right
- tactic::combinators::seq
- tactic::combinators::simp
- tactic::combinators::split
- tactic::combinators::then_all
- tactic::combinators::try_
- tactic_script::parse_script
- tactic_script::parse_script_with_env
- tactic_script::prove_scripted_library
- trace_determinism::bernstein_independent
- trace_determinism::run
- trace_determinism::trace_poset
- twosat::is_refutation
- twosat::satisfies
- twosat::solve
- unify::apply_subst_to_expr
- unify::apply_subst_to_term
- unify::beta_reduce
- unify::compose_substitutions
- unify::match_expr_pattern
- unify::match_term_pattern
- unify::unify_exprs
- unify::unify_pattern
- unify::unify_terms
- verify::check_derivation
- verify::check_derivation_with_defs
- verify::dependency_graph
- verify::detect_conflict
- verify::prove_certify_check
- verify::prove_certify_check_bounded
- verify::prove_certify_check_bounded_with_defs
- verify::prove_certify_check_with_defs
- verify::prove_library
- verify::prove_library_with_axioms
- xor_drat::emit_drat_over_support
- xor_drat::emit_modp_drat
- xor_drat::emit_xor_drat
- xor_drat::gadget_clauses
- xorsat::is_refutation
- xorsat::refute_via_parity
- xorsat::satisfies
- xorsat::solve
Type Aliases
- cdcl::Var
- cofactor::CanonClauses
- cofactor::Twist
- error::ProofResult
- fp2::Fp2
- hypercube::Corner
- hyperelliptic::Quad
- orbit_stability::RowLabel
- orbit_stability::Structure
- permgroup::Perm
- polycalc::Mono
- polycalc::Poly
- polycalc_gfp::GfpPoly
- polycalc_zm::ZmPoly
- res_width::MaskClause
- tactic::Tactic
- unify::ExprSubstitution
- unify::Substitution