Module ClauseQueue_intf.S.C

module C: Clause_intf.S 

module Ctx: Ctx.S 
type t 
type clause = t 

Flags


type flag = SClause.flag 
val set_flag : flag -> t -> bool -> unit
set boolean flag
val get_flag : flag -> t -> bool
get value of boolean flag
val mark_redundant : t -> unit
val is_redundant : t -> bool
val mark_backward_simplified : t -> unit
val is_backward_simplified : t -> bool

Basics


include Interfaces.EQ
include Interfaces.HASH
val compare : t -> t -> int
val id : t -> int
val lits : t -> Logtk.Literal.t array
val is_ground : t -> bool
val weight : t -> int
module Tbl: CCHashtbl.S  with type key = t
val is_goal : t -> bool
Looking at the clause's proof, return true iff the clause is an initial (negated) goal from the problem
val distance_to_goal : t -> int option
See Proof.distance_to_goal, applied to the clause's proof
val comes_from_goal : t -> bool
true iff the clause is (indirectly) deduced from a goal or lemma

Boolean Abstraction


val pp_trail : Trail.t CCFormat.printer
Printer for boolean trails, that uses Clause_intf.S.Ctx to display boxes
val has_trail : t -> bool
Has a non-empty trail?
val trail : t -> Trail.t
Get the clause's trail
val trail_l : t list -> Trail.t
Merge the trails of several clauses
val update_trail : (Trail.t -> Trail.t) -> t -> t
Change the trail. The resulting clause has same parents, proof and literals as the input one
val trail_subsumes : t -> t -> bool
trail_subsumes c1 c2 = Trail.subsumes (get_trail c1) (get_trail c2)
val is_active : t -> v:Trail.valuation -> bool
True if the clause's trail is active in this valuation

Constructors


val create : penalty:int ->
trail:Trail.t ->
Logtk.Literal.t list -> Clause_intf.proof_step -> t
Build a new clause from the given literals.
penalty : heuristic penalty due to history of the clause (the higher, the less likely the clause is to be picked soon) also takes a list of literals and a proof builder
trail : boolean trail
val create_a : penalty:int ->
trail:Trail.t ->
Logtk.Literal.t array -> Clause_intf.proof_step -> t
Build a new clause from the given literals.
val of_sclause : ?penalty:int -> SClause.t -> Clause_intf.proof_step -> t
val of_forms : ?penalty:int ->
trail:Trail.t ->
Logtk.Term.t Logtk.SLiteral.t list ->
Clause_intf.proof_step -> t
Directly from list of formulas
val of_forms_axiom : ?penalty:int ->
file:string ->
name:string -> Logtk.Term.t Logtk.SLiteral.t list -> t
Construction from formulas as axiom (initial clause)
val of_statement : Logtk.Statement.clause_t -> t list
Extract a clause from a statement, if any
val proof_step : t -> Clause_intf.proof_step
Extract its proof from the clause
val proof : t -> Clause_intf.proof
Obtain the pair conclusion, step
val proof_parent : t -> Logtk.Proof.Parent.t
val proof_parent_subst : Logtk.Subst.Renaming.t ->
t Logtk.Scoped.t -> Logtk.Subst.t -> Logtk.Proof.Parent.t
val update_proof : t ->
(Clause_intf.proof_step -> Clause_intf.proof_step) -> t
update_proof c f creates a new clause that is similar to c in all aspects, but with the proof f (proof_step c)
val is_empty : t -> bool
Is the clause an empty clause?
val length : t -> int
Number of literals
val maxlits : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
List of maximal literals
val is_maxlit : t Logtk.Scoped.t -> Logtk.Subst.t -> idx:int -> bool
Is the i-th literal maximal in subst(clause)? Equivalent to Bitvector.get (maxlits ~ord c subst) i
val eligible_res : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
Bitvector that indicates which of the literals of subst(clause) are eligible for resolution. THe literal has to be either maximal among selected literals of the same sign, if some literal is selected, or maximal if none is selected.
val eligible_res_no_subst : t -> CCBV.t
More efficient version of Clause_intf.S.eligible_res with Subst.empty
val eligible_param : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
Bitvector that indicates which of the literals of subst(clause) are eligible for paramodulation. That means the literal is positive, no literal is selecteed, and the literal is maximal among literals of subst(clause).
val is_eligible_param : t Logtk.Scoped.t -> Logtk.Subst.t -> idx:int -> bool
Check whether the idx-th literal is eligible for paramodulation
val has_selected_lits : t -> bool
does the clause have some selected literals?
val is_selected : t -> int -> bool
check whether a literal is selected
val selected_lits : t -> (Logtk.Literal.t * int) list
get the list of selected literals
val penalty : t -> int
val is_unit_clause : t -> bool
is the clause a unit clause?
val is_oriented_rule : t -> bool
Is the clause a positive oriented clause?
val symbols : ?init:Logtk.ID.Set.t -> t Sequence.t -> Logtk.ID.Set.t
symbols that occur in the clause
val to_sclause : t -> SClause.t
val to_forms : t -> Logtk.Term.t Logtk.SLiteral.t list
Easy iteration on an abstract view of literals
val to_s_form : t -> Logtk.TypedSTerm.Form.t

Iterators


module Seq: sig .. end

Filter literals


module Eligible: sig .. end

Set of clauses


module ClauseSet: CCSet.S  with type elt = t
Simple set

Position


module Pos: sig .. end

Clauses with more data


module WithPos: sig .. end
Clause within which a subterm (and its position) are hilighted

IO


val pp : t CCFormat.printer
val pp_tstp : t CCFormat.printer
val pp_tstp_full : t CCFormat.printer
Print in a cnf() statement
val to_string : t -> string
Debug printing to a string
val pp_set : ClauseSet.t CCFormat.printer
val pp_set_tstp : ClauseSet.t CCFormat.printer