Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file env_intf.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333(* This file is free software, part of Zipperposition. See file "license" for more details. *)openLogtkmoduletypeS=sigmoduleCtx:Ctx.SmoduleC:Clause.SwithmoduleCtx=CtxmoduleProofState:ProofState.SwithmoduleC=CandmoduleCtx=Ctxtypeinf_rule=C.t->C.tlist(** An inference returns a list of conclusions *)typegenerate_rule=full:bool->unit->C.tlist(** Generation of clauses regardless of current clause.
@param full if true, perform more thorough checks *)typeclause_elim_rule=unit->unit(** Eliminates clauses from the proof state using algorithms
like blocked clause elimination and similar *)typebinary_inf_rule=inf_ruletypeunary_inf_rule=inf_ruletypesimplify_rule=C.t->C.tSimplM.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 *)typeactive_simplify_rule=simplify_ruletyperw_simplify_rule=simplify_ruletypebackward_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 ()] *)typeredundant_rule=C.t->bool(** check whether the clause is redundant w.r.t the set *)typebackward_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 *)typeimmediate_simplification_rule=C.t->C.tIter.t->C.tIter.toption(** Following Kotelnikov's iProver superposition implementation, try to simplify
given clause (first argument) using a set of clauses (second argument).
If simplification suceeded, then a set of clauses to be injected
into passive set is returned. *)typeis_trivial_trail_rule=Trail.t->bool(** Rule that checks whether the trail is trivial (a tautology) *)typeis_trivial_rule=C.t->bool(** Rule that checks whether the clause is trivial (a tautology) *)typeterm_rewrite_rule=Term.t->(Term.t*Proof.parentlist)option(** Rewrite rule on terms *)typeterm_norm_rule=Term.t->Term.toption(** Normalization rule on terms *)typelit_rewrite_rule=Literal.t->(Literal.t*Proof.parentlist*Proof.taglist)option(** Rewrite rule on literals *)typemulti_simpl_rule=C.t->C.tlistoption(** (maybe) rewrite a clause to a set of clauses.
Must return [None] if the clause is unmodified *)type'aconversion_result=|CR_skip(** rule didn't fire *)|CR_drop(** drop the clause from the proof state *)|CR_addof'a(** add this to the result *)|CR_returnof'a(** shortcut the remaining rules, return this *)typeclause_conversion_rule=Statement.clause_t->C.tlistconversion_result(** A hook to convert a particular statement into a list
of clauses *)(** {2 Modify the Env} *)valadd_passive:C.tIter.t->unit(** Add passive clauses *)valadd_active:C.tIter.t->unit(** Add active clauses *)valadd_simpl:C.tIter.t->unit(** Add simplification clauses *)valremove_passive:C.tIter.t->unit(** Remove passive clauses *)valremove_active:C.tIter.t->unit(** Remove active clauses *)valremove_simpl:C.tIter.t->unit(** Remove simplification clauses *)valget_passive:unit->C.tIter.t(** Passive clauses *)valget_active:unit->C.tIter.t(** Active clauses *)valadd_binary_inf:string->binary_inf_rule->unit(** Add a binary inference rule *)valadd_unary_inf:string->unary_inf_rule->unit(** Add a unary inference rule *)valadd_rw_simplify:rw_simplify_rule->unit(** Add forward rewriting rule *)valadd_active_simplify:active_simplify_rule->unit(** Add simplification w.r.t active set *)valadd_backward_simplify:backward_simplify_rule->unit(** Add simplification of the active set *)valadd_redundant:redundant_rule->unit(** Add redundancy criterion w.r.t. the active set *)valadd_backward_redundant:backward_redundant_rule->unit(** Add rule that finds redundant clauses within active set *)valadd_basic_simplify:simplify_rule->unit(** Add basic simplification rule *)valadd_unary_simplify:simplify_rule->unit(** Add unary simplification rule (not dependent on proof state) *)valadd_multi_simpl_rule:priority:int->multi_simpl_rule->unit(** Add a multi-clause simplification rule *)valadd_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 *)valadd_cheap_multi_simpl_rule:multi_simpl_rule->unit(** Add an efficient multi-clause simplification rule,
that will be used to simplify newly generated clauses
when they are moved from unprocessed to passive set. *)valadd_is_trivial_trail:is_trivial_trail_rule->unit(** Add tautology detection rule *)valadd_is_trivial:is_trivial_rule->unit(** Add tautology detection rule *)valadd_rewrite_rule:string->term_rewrite_rule->unit(** Add a term rewrite rule *)valset_ho_normalization_rule:string->term_norm_rule->unit(** Add a ho norm rule *)valget_ho_normalization_rule:unit->term_norm_rulevaladd_immediate_simpl_rule:immediate_simplification_rule->unitvaladd_lit_rule:string->lit_rewrite_rule->unit(** Add a literal rewrite rule *)valadd_generate:priority:int->string->generate_rule->unit(** Add a generation rule with assigned priority.
Rules with higher priority will be tried first. *)valadd_clause_elimination_rule:priority:int->string->clause_elim_rule->unitvalcr_skip:_conversion_resultvalcr_return:'a->'aconversion_resultvalcr_add:'a->'aconversion_resultvaladd_clause_conversion:clause_conversion_rule->unitvaladd_step_init:(unit->unit)->unit(** add a function to call before each saturation step *)valadd_fragment_check:(C.t->bool)->unitvalcheck_fragment:C.t->bool(** {2 Use the Env} *)valmulti_simplify:C.t->C.tlistoption(** Can we simplify the clause into a List of simplified clauses? *)valparams:Params.tvalget_empty_clauses:unit->C.ClauseSet.t(** Set of known empty clauses *)valget_some_empty_clause:unit->C.toption(** Some empty clause, if present, otherwise None *)valhas_empty_clause:unit->bool(** Is there an empty clause? *)valon_start:unitSignal.t(** Triggered before starting saturation *)valon_input_statement:Statement.clause_tSignal.t(** Triggered on every input statement *)valon_forward_simplified:(C.t*(C.toption))Signal.t(** Triggered when after the clause set is fully forward-simplified.
First argument is the original clause c and the second one is Some c'
if c simplifies into c' or None if c is deemed redundant *)valconvert_input_statements:Statement.clause_tCCVector.ro_vector->C.tClause.sets(** Convert raw input statements into clauses, triggering
{! on_input_statement} *)valon_empty_clause:C.tSignal.t(** Signal triggered when an empty clause is found *)valord:unit->Ordering.tvalprecedence:unit->Precedence.tvalsignature:unit->Signature.tvalpp:unitCCFormat.printervalpp_full:unitCCFormat.printer(** {2 High level operations} *)typestats=int*int*int(** statistics on clauses : num active, num passive, num simplification *)valstats:unit->stats(** Compute stats *)valnext_passive:unit->C.toption(** Extract next passive clause *)valdo_binary_inferences:C.t->C.tIter.t(** do binary inferences that involve the given clause *)valdo_unary_inferences:C.t->C.tIter.t(** do unary inferences for the given clause *)valdo_generate:full:bool->unit->C.tIter.t(** do generating inferences *)valdo_clause_eliminate:unit->unit(** changes the proof state by running registered clause elimination procedures
and removing all the eliminated clauses from the proof state *)valis_trivial_trail:Trail.t->bool(** Check whether the trail is trivial *)valis_trivial:C.t->bool(** Check whether the clause is trivial *)valis_active:C.t->bool(** Is the clause in the active set *)valis_passive:C.t->bool(** Is the clause a passive clause? *)valbasic_simplify:simplify_rule(** Basic (and fast) simplifications *)valunary_simplify:simplify_rule(** Simplify the clause. *)valbackward_simplify:C.t->C.ClauseSet.t*C.tIter.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. *)valsimplify_active_with:(C.t->C.tlistoption)->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. *)valforward_simplify:simplify_rule(** Simplify the clause w.r.t to the active set and experts *)valcheap_multi_simplify:C.t->C.tlistoption(** Cheap simplifications that can result in multiple clauses (e.g. AVATAR splitting) *)valimmediate_simplify:C.t->C.tIter.t->(C.tIter.t)(** Simplify given clause using its children. Given clause is
removed from active set and result of this rule is added to passive set,
if any of the registered rules suceeded *)valgenerate:C.t->C.tIter.t(** Perform all generating inferences *)valis_redundant:C.t->bool(** Is the given clause redundant w.r.t the active set? *)valsubsumed_by:C.t->C.ClauseSet.t(** List of active clauses subsumed by the given clause *)valall_simplify:C.t->C.tlistSimplM.t(** Use all simplification rules to convert a clause into a set
of maximally simplified clause (or [[]] if they are all trivial). *)valstep_init:unit->unit(** call all functions registered with {!add_step_init} *)(** {2 Misc} *)valflex_state:unit->Flex_state.t(** State inherited from configuration *)valupdate_flex_state:(Flex_state.t->Flex_state.t)->unit(** [update_flex_state f] changes [flex_state ()] using [f] *)valflex_add:'aFlex_state.key->'a->unit(** add [k -> v] to the flex state *)valflex_get:'aFlex_state.key->'a(** [flex_get k] is the same as [Flex_state.get_exn k (flex_state ())].
@raise Not_found if the key is not present *)(* The following signals are raised only existentially *)valon_pred_var_elimination:(C.t*Term.t)Signal.t(** this signal is raised if a formula that universally quantifies
a predicate removes that predicate and rules that want to instantiate it
early should listen to this *)valon_pred_skolem_introduction:(C.t*Term.t)Signal.t(** this signal is raised when a predicate Skolem is introduced *)end