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
-
Priority Queue of ho-streams
Heuristic selection of ho-streams, using a priority queue. Only one queue is used, but the priority of a stream is determined by a combination of criteria that should include at least one fair criterion (e.g. the age of the clause, so that older clauses are more likely to be chosen).
module type S = StreamQueue_intf.S