libzipperposition
Library for Zipperposition
IN THIS PACKAGE
-
library libzipperposition
-
module Libzipperposition
-
module AC
-
module Make
-
argument 1-Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
-
module AC_intf
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module Bool_clause
-
module Bool_lit_intf
-
module Classify_cst
-
module ClauseContext
-
module Set
-
-
module Const
-
module Env
-
module Make
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module Env_intf
-
module type S
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module Eprover_interface
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
-
module Extensions
-
module Params
-
module ProofState
-
module Make
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module ProofState_intf
-
module type S
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module SClause
-
module Sat_solver
-
module Sat_solver_intf
-
module type S
-
-
module Saturate
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
-
module Selection
-
module Signals
-
module Trail
-
-
-
library libzipperposition.calculi
-
module Libzipperposition_calculi
-
module App_encode
-
module Arith_int
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module PS
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module PS
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module Arith_rat
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module PS
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module PS
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module Avatar
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
argument 2-Sat
-
-
-
module Avatar_intf
-
module type S
-
module E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module Solver
-
-
-
module Booleans
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module EnumTypes
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module Fool
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module Heuristics
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module PS
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module PS
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module Higher_order
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
module Ind_types
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
-
module Induction
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
-
module Induction_intf
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
-
module Rewriting
-
module Make
-
argument 1-E
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
-
module Superposition
-
module Make
-
argument 1-Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module PS
-
module ActiveSet
-
module C
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
-
module Superposition_intf
-
module type S
-
module Env
-
module ProofState
-
module ActiveSet
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
module PS
-
module ActiveSet
-
module C
-
module type CLAUSE_SET
-
module CQueue
-
module C
-
module PriorityFun
-
module WeightFun
-
-
module PassiveSet
-
module SimplSet
-
module SubsumptionIndex
-
module C
-
-
-
-
-
-
library libzipperposition.phases
-
module Libzipperposition_phases
-
module Phases_impl
-
Libraries
This package provides the following libraries (via dune):
libzipperposition
Documentation:
Libzipperposition.ACLibzipperposition.AC_intfLibzipperposition.BBoxLibzipperposition.Bool_clauseLibzipperposition.Bool_litLibzipperposition.Bool_lit_intfLibzipperposition.Classify_cstLibzipperposition.ClauseLibzipperposition.ClauseContextLibzipperposition.ClauseQueueLibzipperposition.ClauseQueue_intfLibzipperposition.Clause_intfLibzipperposition.ConstLibzipperposition.Cover_setLibzipperposition.CtxLibzipperposition.Ctx_intfLibzipperposition.Cut_formLibzipperposition.EnvLibzipperposition.Env_intfLibzipperposition.Eprover_interfaceLibzipperposition.ExtensionsLibzipperposition.Ind_cstLibzipperposition.ParamsLibzipperposition.ProofStateLibzipperposition.ProofState_intfLibzipperposition.SClauseLibzipperposition.Sat_solverLibzipperposition.Sat_solver_intfLibzipperposition.SaturateLibzipperposition.SelectionLibzipperposition.SignalsLibzipperposition.SimplMLibzipperposition.StreamLibzipperposition.StreamQueueLibzipperposition.StreamQueue_intfLibzipperposition.Stream_intfLibzipperposition.Trail
Dependencies: containers, zarith, msat, logtk, logtk.proofs, logtk.parsers, str
libzipperposition.calculi
Documentation:
Libzipperposition_calculi.App_encodeLibzipperposition_calculi.Arith_intLibzipperposition_calculi.Arith_ratLibzipperposition_calculi.AvatarLibzipperposition_calculi.Avatar_intfLibzipperposition_calculi.BooleansLibzipperposition_calculi.EnumTypesLibzipperposition_calculi.FoolLibzipperposition_calculi.HeuristicsLibzipperposition_calculi.Higher_orderLibzipperposition_calculi.Ind_typesLibzipperposition_calculi.InductionLibzipperposition_calculi.Induction_intfLibzipperposition_calculi.RewritingLibzipperposition_calculi.SimplexModular and incremental implementation of the simplex.Libzipperposition_calculi.SuperpositionLibzipperposition_calculi.Superposition_intf
Dependencies: libzipperposition
libzipperposition.phases
Documentation: Libzipperposition_phases
Dependencies: libzipperposition, libzipperposition.calculi