libzipperposition
Library for Zipperposition
1024">
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.AC
Libzipperposition.AC_intf
Libzipperposition.BBox
Libzipperposition.Bool_clause
Libzipperposition.Bool_lit
Libzipperposition.Bool_lit_intf
Libzipperposition.Classify_cst
Libzipperposition.Clause
Libzipperposition.ClauseContext
Libzipperposition.ClauseQueue
Libzipperposition.ClauseQueue_intf
Libzipperposition.Clause_intf
Libzipperposition.Const
Libzipperposition.Cover_set
Libzipperposition.Ctx
Libzipperposition.Ctx_intf
Libzipperposition.Cut_form
Libzipperposition.Env
Libzipperposition.Env_intf
Libzipperposition.Eprover_interface
Libzipperposition.Extensions
Libzipperposition.Ind_cst
Libzipperposition.Params
Libzipperposition.ProofState
Libzipperposition.ProofState_intf
Libzipperposition.SClause
Libzipperposition.Sat_solver
Libzipperposition.Sat_solver_intf
Libzipperposition.Saturate
Libzipperposition.Selection
Libzipperposition.Signals
Libzipperposition.SimplM
Libzipperposition.Stream
Libzipperposition.StreamQueue
Libzipperposition.StreamQueue_intf
Libzipperposition.Stream_intf
Libzipperposition.Trail
Dependencies: containers, zarith, msat, logtk, logtk.proofs, logtk.parsers, str
libzipperposition.calculi
Documentation:
Libzipperposition_calculi.App_encode
Libzipperposition_calculi.Arith_int
Libzipperposition_calculi.Arith_rat
Libzipperposition_calculi.Avatar
Libzipperposition_calculi.Avatar_intf
Libzipperposition_calculi.Booleans
Libzipperposition_calculi.EnumTypes
Libzipperposition_calculi.Fool
Libzipperposition_calculi.Heuristics
Libzipperposition_calculi.Higher_order
Libzipperposition_calculi.Ind_types
Libzipperposition_calculi.Induction
Libzipperposition_calculi.Induction_intf
Libzipperposition_calculi.Rewriting
Libzipperposition_calculi.Simplex
Modular and incremental implementation of the simplex.Libzipperposition_calculi.Superposition
Libzipperposition_calculi.Superposition_intf
Dependencies: libzipperposition
libzipperposition.phases
Documentation: Libzipperposition_phases
Dependencies: libzipperposition, libzipperposition.calculi