Module `E.C`

module Ctx = Ctx

type t

type clause = t

Flags

type flag = Libzipperposition.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

val is_orphaned : t -> bool

Basics

include Logtk.Interfaces.EQ with type t := t

include Logtk.Interfaces.HASH with type t := t

include Logtk.Interfaces.EQ with type t := t

val equal : t -> t -> bool

val hash : t -> int

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

val ho_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 : Libzipperposition.Trail.t CCFormat.printer

Printer for boolean trails, that uses Ctx to display boxes

val has_trail : t -> bool

Has a non-empty trail?

val trail : t -> Libzipperposition.Trail.t

Get the clause's trail

val trail_l : t list -> Libzipperposition.Trail.t

Merge the trails of several clauses

val update_trail : 
  (Libzipperposition.Trail.t -> Libzipperposition.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:Libzipperposition.Trail.valuation -> bool

True if the clause's trail is active in this valuation

val is_inj_axiom : t -> (Logtk.ID.t * int) option

Returns Some (sym,i) if clause is injectivity axiom for ith argument of symbol sym.

Constructors

val create : 
  penalty:int ->
  trail:Libzipperposition.Trail.t ->
  Logtk.Literal.t list ->
  Libzipperposition.Clause_intf.proof_step ->
  t

Build a new clause from the given literals.

parameter trail
boolean trail

parameter 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

val create_a : 
  penalty:int ->
  trail:Libzipperposition.Trail.t ->
  Logtk.Literal.t array ->
  Libzipperposition.Clause_intf.proof_step ->
  t

Build a new clause from the given literals.

val of_sclause : 
  ?penalty:int ->
  Libzipperposition.SClause.t ->
  Libzipperposition.Clause_intf.proof_step ->
  t

val of_forms : 
  ?penalty:int ->
  trail:Libzipperposition.Trail.t ->
  Logtk.Term.t Logtk.SLiteral.t list ->
  Libzipperposition.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 : ?convert_defs:bool -> Logtk.Statement.clause_t -> t list

Extract a clause from a statement, if any

val proof_step : t -> Libzipperposition.Clause_intf.proof_step

Extract its proof from the clause

val proof : t -> Libzipperposition.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 ->
  (Libzipperposition.Clause_intf.proof_step ->
    Libzipperposition.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 proof_depth : t -> int

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 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 eligible_subterms_of_bool : t -> Libzipperposition.SClause.TPSet.t

Set that contains positions of selected Booleans and their eligible green subterms.

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 selected_lits_bv : t -> CCBV.t

get the bv of selected literals

val bool_selected : t -> (Logtk.Term.t * Logtk.Position.t) list

get the list of selected Bool subterms

val penalty : t -> int

val inc_penalty : t -> int -> unit

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 ->
  ?include_types:bool ->
  t Iter.t ->
  Logtk.ID.Set.t

symbols that occur in the clause

val to_sclause : t -> Libzipperposition.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

val ground_clause : t -> t

val eta_reduce : t -> t option

Iterators

module Seq : sig ... end

val apply_subst : 
  ?renaming:Logtk.Subst.Renaming.t ->
  ?proof:Logtk.Proof.Step.t option ->
  ?penalty_inc:int option ->
  t Logtk.Scoped.t ->
  Logtk.Subst.FO.t ->
  t

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 highlighted

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 to_string_tstp : t -> string

Debug printing to a string

val pp_set : ClauseSet.t CCFormat.printer

val pp_set_tstp : ClauseSet.t CCFormat.printer

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libzipperposition.induction/Libzipperposition_induction/Make/argument-1-E/C/index.html

Module `E.C`

Flags

Basics

Boolean Abstraction

Constructors

Iterators

Filter literals

Set of clauses

Position

Clauses with more data

IO

package libzipperposition

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libzipperposition.induction/Libzipperposition_induction/Make/argument-1-E/C/index.html

Module E.C

Flags

Basics

Boolean Abstraction

Constructors

Iterators

Filter literals

Set of clauses

Position

Clauses with more data

IO

Module `E.C`