module Env:Env.S
module Ctx:Ctx.S
module C:Clause.S
with module Ctx = Ctx
module ProofState:ProofState.S
with module C = C and module Ctx = Ctx
typeinf_rule =
C.t -> C.t list
typegenerate_rule =
unit -> C.t list
typebinary_inf_rule =
inf_rule
typeunary_inf_rule =
inf_rule
typesimplify_rule =
C.t -> C.t SimplM.t
(c, `Same)
means the clause has not been simplified;
(c, `New)
means the clause has been simplified at least oncetypeactive_simplify_rule =
simplify_rule
typerw_simplify_rule =
simplify_rule
typebackward_simplify_rule =
C.t -> C.ClauseSet.t
backward_simplify c
therefore returns a subset of
ProofState.ActiveSet.clauses ()
typeredundant_rule =
C.t -> bool
typebackward_redundant_rule =
C.ClauseSet.t -> C.t -> C.ClauseSet.t
ProofState.ActiveSet
w.r.t the clause.
first param is the set of already known redundant clause, the rule
should add clauses to ittypeis_trivial_rule =
C.t -> bool
typeterm_rewrite_rule =
Libzipperposition.FOTerm.t -> Libzipperposition.FOTerm.t option
typelit_rewrite_rule =
Literal.t -> Literal.t option
typemulti_simpl_rule =
C.t -> C.t list option
None
if the clause is unmodifiedtype 'a
conversion_result =
| |
CR_skip |
(* |
rule didn't fire
| *) |
| |
CR_add of |
(* |
add this to the result
| *) |
| |
CR_return of |
(* |
shortcut the remaining rules, return this
| *) |
typeclause_conversion_rule =
Libzipperposition.Statement.clause_t ->
C.t list conversion_result
val add_passive : C.t Sequence.t -> unit
val add_active : C.t Sequence.t -> unit
val add_simpl : C.t Sequence.t -> unit
val remove_passive : C.t Sequence.t -> unit
val remove_active : C.t Sequence.t -> unit
val remove_simpl : C.t Sequence.t -> unit
val get_passive : unit -> C.t Sequence.t
val get_active : unit -> C.t Sequence.t
val add_binary_inf : string -> binary_inf_rule -> unit
val add_unary_inf : string -> unary_inf_rule -> unit
val add_rw_simplify : rw_simplify_rule -> unit
val add_active_simplify : active_simplify_rule -> unit
val add_backward_simplify : backward_simplify_rule -> unit
val add_redundant : redundant_rule -> unit
val add_backward_redundant : backward_redundant_rule -> unit
val add_simplify : simplify_rule -> unit
val add_multi_simpl_rule : multi_simpl_rule -> unit
val add_is_trivial : is_trivial_rule -> unit
val add_rewrite_rule : string -> term_rewrite_rule -> unit
val add_lit_rule : string -> lit_rewrite_rule -> unit
val add_generate : string -> generate_rule -> unit
val cr_skip : 'a conversion_result
val cr_return : 'a -> 'a conversion_result
val cr_add : 'a -> 'a conversion_result
val add_clause_conversion : clause_conversion_rule -> unit
val add_step_init : (unit -> unit) -> unit
val multi_simplify : C.t -> C.t list option
val params : Params.t
val get_empty_clauses : unit -> C.ClauseSet.t
val get_some_empty_clause : unit -> C.t option
val has_empty_clause : unit -> bool
val on_start : unit Signal.t
val on_input_statement : Libzipperposition.Statement.clause_t Signal.t
val convert_input_statements : Libzipperposition.Statement.clause_t CCVector.ro_vector ->
C.t CCVector.ro_vector
Env_intf.S.on_input_statement
val on_empty_clause : C.t Signal.t
val ord : unit -> Libzipperposition.Ordering.t
val precedence : unit -> Libzipperposition.Precedence.t
val signature : unit -> Libzipperposition.Signature.t
val pp : unit CCFormat.printer
val pp_full : unit CCFormat.printer
typestats =
int * int * int
val stats : unit -> stats
val next_passive : unit -> C.t option
val do_binary_inferences : C.t -> C.t Sequence.t
val do_unary_inferences : C.t -> C.t Sequence.t
val do_generate : unit -> C.t Sequence.t
val is_trivial : C.t -> bool
val is_active : C.t -> bool
val is_passive : C.t -> bool
val simplify : simplify_rule
val backward_simplify : C.t -> C.ClauseSet.t * C.t Sequence.t
val simplify_active_with : (C.t -> C.t list option) -> unit
val forward_simplify : simplify_rule
val generate : C.t -> C.t Sequence.t
val is_redundant : C.t -> bool
val subsumed_by : C.t -> C.ClauseSet.t
val all_simplify : C.t -> C.t list SimplM.t
[]
if they are all trivial).val step_init : unit -> unit
Env_intf.S.add_step_init
val flex_state : unit -> Flex_state.t
val update_flex_state : (Flex_state.t -> Flex_state.t) -> unit
update_flex_state f
changes flex_state ()
using f
val flex_add : 'a Flex_state.key -> 'a -> unit
k -> v
to the flex stateval flex_get : 'a Flex_state.key -> 'a
flex_get k
is the same as Flex_state.get_exn k (flex_state ())
.Not_found
if the key is not present