Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file avatar_intf.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100(* This file is free software, part of Zipperposition. See file "license" for more details. *)openLogtkopenLibzipperpositionmoduletypeS=sigmoduleE:Env.SmoduleSolver:Sat_solver.SmoduleBLit=BBox.Litvalsplit:E.multi_simpl_rule(** Split a clause into components *)valcheck_empty:E.unary_inf_rule(** Forbid empty clauses with trails, i.e. adds the negation of their
trails to the SAT-solver *)valbefore_check_sat:unitSignal.tvalafter_check_sat:unitSignal.tvalfilter_absurd_trails:(Trail.t->bool)->unit(** [filter_trails f] calls [f] on every trail associated with the empty
clause. If [f] returns [false], the trail is ignored, otherwise
it's negated and sent to the SAT solver *)valcheck_satisfiability:E.generate_rule(** Checks that the SAT context is still valid *)typecut_res=private{cut_form:Cut_form.t;(** the lemma itself *)cut_pos:E.C.tlist;(** clauses true if lemma is true *)cut_lit:BLit.t;(** lit that is true if lemma is true *)cut_depth:int;(** if the lemma is used to prove another lemma *)cut_proof:Proof.Step.t;(** where does the lemma come from? *)cut_proof_parent:Proof.Parent.t;(** how to justify sth from the lemma *)cut_reason:unitCCFormat.printeroption;(** Informal reason why the lemma was added *)}(** This represents a cut on a formula, where we obtain a list
of clauses [cut_pos] representing the formula itself with the
trail [lemma], and a boolean literal [cut_lit] that is true iff
the trail is true.
Other modules, when a cut is introduced, will try to disprove
the lemma (e.g. by induction or theory reasoning).
*)valcut_form:cut_res->Cut_form.tvalcut_pos:cut_res->E.C.tlistvalcut_lit:cut_res->BLit.tvalcut_depth:cut_res->intvalcut_proof:cut_res->Proof.Step.tvalcut_proof_parent:cut_res->Proof.Parent.tvalpp_cut_res:cut_resCCFormat.printervalcut_res_clauses:cut_res->E.C.tIter.tvalprint_lemmas:unitCCFormat.printer(** print the current list of lemmas, and their status *)valintroduce_cut:?reason:unitCCFormat.printer->?penalty:int->?depth:int->Cut_form.t->Proof.Step.t->cut_res(** Introduce a cut on the given clause(s). Pure.
@param reason some comment on why the lemma was added *)valadd_prove_lemma:(cut_res->E.C.tlistE.conversion_result)->unit(** Add a mean of proving lemmas *)valadd_lemma:cut_res->unit(** Add the given cut to the list of lemmas. Modifies the global list
of lemmas.
It will call the functions added by {!add_prove_lemma} to try and
prove this one. *)valadd_imply:cut_reslist->cut_res->Proof.Step.t->unit(** [add_imply l res] means that the conjunction of lemmas in [l]
implies that the lemma [res] is proven *)valon_input_lemma:cut_resSignal.t(** Triggered every time a cut is introduced for an input lemma
(i.e. every time a statement of the form `lemma F` is translated) *)valon_lemma:cut_resSignal.t(** Triggered every time a cut is introduced, by any means. In
particular it is triggered at least as often as {!on_input_lemma} *)valconvert_lemma:E.clause_conversion_rule(** Intercepts input lemmas and converts them into clauses.
Triggers {!on_input_lemma} with the resulting cut *)valregister:split:bool->unit->unit(** Register inference rules to the environment
@param split if true, the clause splitting rule is added. Otherwise
Avatar is only used for other things such as induction. *)end