package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Env.MakeSource

Build a new Environment

Parameters

module X : sig ... end

Signature

include S with module Ctx = X.Ctx
Sourcemodule Ctx = X.Ctx
Sourcemodule C : Clause.S with module Ctx = Ctx
Sourcemodule ProofState : ProofState.S with module C = C and module Ctx = Ctx
Sourcetype inf_rule = C.t -> C.t list

An inference returns a list of conclusions

Sourcetype generate_rule = full:bool -> unit -> C.t list

Generation of clauses regardless of current clause.

  • parameter full

    if true, perform more thorough checks

Sourcetype binary_inf_rule = inf_rule
Sourcetype unary_inf_rule = inf_rule
Sourcetype simplify_rule = C.t -> C.t SimplM.t

Simplify the clause structurally (basic simplifications), in the simplification monad. (c, `Same) means the clause has not been simplified; (c, `New) means the clause has been simplified at least once

Sourcetype active_simplify_rule = simplify_rule
Sourcetype rw_simplify_rule = simplify_rule
Sourcetype backward_simplify_rule = C.t -> C.ClauseSet.t

backward simplification by a unit clause. It returns a set of active clauses that can potentially be simplified by the given clause. backward_simplify c therefore returns a subset of ProofState.ActiveSet.clauses ()

Sourcetype redundant_rule = C.t -> bool

check whether the clause is redundant w.r.t the set

Sourcetype backward_redundant_rule = C.ClauseSet.t -> C.t -> C.ClauseSet.t

find redundant clauses in ProofState.ActiveSet w.r.t the clause. first param is the set of already known redundant clause, the rule should add clauses to it

Sourcetype is_trivial_trail_rule = Trail.t -> bool

Rule that checks whether the trail is trivial (a tautology)

Sourcetype is_trivial_rule = C.t -> bool

Rule that checks whether the clause is trivial (a tautology)

Sourcetype term_rewrite_rule = Logtk.Term.t -> (Logtk.Term.t * Logtk.Proof.parent list) option

Rewrite rule on terms

Sourcetype term_norm_rule = Logtk.Term.t -> Logtk.Term.t option

Normalization rule on terms

Sourcetype lit_rewrite_rule = Logtk.Literal.t -> (Logtk.Literal.t * Logtk.Proof.parent list * Logtk.Proof.tag list) option

Rewrite rule on literals

Sourcetype multi_simpl_rule = C.t -> C.t list option

(maybe) rewrite a clause to a set of clauses. Must return None if the clause is unmodified

Sourcetype 'a conversion_result =
  1. | CR_skip
    (*

    rule didn't fire

    *)
  2. | CR_drop
    (*

    drop the clause from the proof state

    *)
  3. | CR_add of 'a
    (*

    add this to the result

    *)
  4. | CR_return of 'a
    (*

    shortcut the remaining rules, return this

    *)
Sourcetype clause_conversion_rule = Logtk.Statement.clause_t -> C.t list conversion_result

A hook to convert a particular statement into a list of clauses

Modify the Env

Sourceval add_passive : C.t Iter.t -> unit

Add passive clauses

Sourceval add_active : C.t Iter.t -> unit

Add active clauses

Sourceval add_simpl : C.t Iter.t -> unit

Add simplification clauses

Sourceval remove_passive : C.t Iter.t -> unit

Remove passive clauses

Sourceval remove_active : C.t Iter.t -> unit

Remove active clauses

Sourceval remove_simpl : C.t Iter.t -> unit

Remove simplification clauses

Sourceval get_passive : unit -> C.t Iter.t

Passive clauses

Sourceval get_active : unit -> C.t Iter.t

Active clauses

Sourceval add_binary_inf : string -> binary_inf_rule -> unit

Add a binary inference rule

Sourceval add_unary_inf : string -> unary_inf_rule -> unit

Add a unary inference rule

Sourceval add_rw_simplify : rw_simplify_rule -> unit

Add forward rewriting rule

Sourceval add_active_simplify : active_simplify_rule -> unit

Add simplification w.r.t active set

Sourceval add_backward_simplify : backward_simplify_rule -> unit

Add simplification of the active set

Sourceval add_redundant : redundant_rule -> unit

Add redundancy criterion w.r.t. the active set

Sourceval add_backward_redundant : backward_redundant_rule -> unit

Add rule that finds redundant clauses within active set

Sourceval add_basic_simplify : simplify_rule -> unit

Add basic simplification rule

Sourceval add_unary_simplify : simplify_rule -> unit

Add unary simplification rule (not dependent on proof state)

Sourceval add_multi_simpl_rule : multi_simpl_rule -> unit

Add a multi-clause simplification rule

Sourceval set_single_step_multi_simpl_rule : multi_simpl_rule -> unit

Add a multi-clause simplification rule, that is going to be applied only once, not in a fixed-point manner

Sourceval add_is_trivial_trail : is_trivial_trail_rule -> unit

Add tautology detection rule

Sourceval add_is_trivial : is_trivial_rule -> unit

Add tautology detection rule

Sourceval add_rewrite_rule : string -> term_rewrite_rule -> unit

Add a term rewrite rule

Sourceval set_ho_normalization_rule : term_norm_rule -> unit

Add a ho norm rule

Sourceval get_ho_normalization_rule : unit -> term_norm_rule
Sourceval add_lit_rule : string -> lit_rewrite_rule -> unit

Add a literal rewrite rule

Sourceval add_generate : string -> generate_rule -> unit
Sourceval cr_skip : _ conversion_result
Sourceval cr_return : 'a -> 'a conversion_result
Sourceval cr_add : 'a -> 'a conversion_result
Sourceval add_clause_conversion : clause_conversion_rule -> unit
Sourceval add_step_init : (unit -> unit) -> unit

add a function to call before each saturation step

Use the Env

Sourceval multi_simplify : C.t -> C.t list option

Can we simplify the clause into a List of simplified clauses?

Sourceval params : Params.t
Sourceval get_empty_clauses : unit -> C.ClauseSet.t

Set of known empty clauses

Sourceval get_some_empty_clause : unit -> C.t option

Some empty clause, if present, otherwise None

Sourceval has_empty_clause : unit -> bool

Is there an empty clause?

Sourceval on_start : unit Logtk.Signal.t

Triggered before starting saturation

Triggered on every input statement

Convert raw input statements into clauses, triggering on_input_statement

Sourceval on_empty_clause : C.t Logtk.Signal.t

Signal triggered when an empty clause is found

Sourceval ord : unit -> Logtk.Ordering.t
Sourceval precedence : unit -> Logtk.Precedence.t
Sourceval signature : unit -> Logtk.Signature.t
Sourceval pp_full : unit CCFormat.printer

High level operations

Sourcetype stats = int * int * int

statistics on clauses : num active, num passive, num simplification

Sourceval stats : unit -> stats

Compute stats

Sourceval next_passive : unit -> C.t option

Extract next passive clause

Sourceval do_binary_inferences : C.t -> C.t Iter.t

do binary inferences that involve the given clause

Sourceval do_unary_inferences : C.t -> C.t Iter.t

do unary inferences for the given clause

Sourceval do_generate : full:bool -> unit -> C.t Iter.t

do generating inferences

Sourceval is_trivial_trail : Trail.t -> bool

Check whether the trail is trivial

Sourceval is_trivial : C.t -> bool

Check whether the clause is trivial

Sourceval is_active : C.t -> bool

Is the clause in the active set

Sourceval is_passive : C.t -> bool

Is the clause a passive clause?

Sourceval basic_simplify : simplify_rule

Basic (and fast) simplifications

Sourceval unary_simplify : simplify_rule

Simplify the clause.

Sourceval backward_simplify : C.t -> C.ClauseSet.t * C.t Iter.t

Perform backward simplification with the given clause. It returns the CSet of clauses that become redundant, and the sequence of those very same clauses after simplification.

Sourceval simplify_active_with : (C.t -> C.t list option) -> unit

Can be called when a simplification relation becomes stronger, with the strengthened relation. (e.g. new axioms should be declared because a theory was detected). This will go through the whole active set, trying to simplify clauses with the given function. Simplified clauses will be put back in the passive set.

Sourceval forward_simplify : simplify_rule

Simplify the clause w.r.t to the active set and experts

Sourceval generate : C.t -> C.t Iter.t

Perform all generating inferences

Sourceval is_redundant : C.t -> bool

Is the given clause redundant w.r.t the active set?

Sourceval subsumed_by : C.t -> C.ClauseSet.t

List of active clauses subsumed by the given clause

Sourceval all_simplify : C.t -> C.t list SimplM.t

Use all simplification rules to convert a clause into a set of maximally simplified clause (or [] if they are all trivial).

Sourceval step_init : unit -> unit

call all functions registered with add_step_init

Misc

Sourceval flex_state : unit -> Logtk.Flex_state.t

State inherited from configuration

Sourceval update_flex_state : (Logtk.Flex_state.t -> Logtk.Flex_state.t) -> unit

update_flex_state f changes flex_state () using f

Sourceval flex_add : 'a Logtk.Flex_state.key -> 'a -> unit

add k -> v to the flex state

Sourceval flex_get : 'a Logtk.Flex_state.key -> 'a

flex_get k is the same as Flex_state.get_exn k (flex_state ()).