package libzipperposition

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

Module CQueue.CSource

Sourcemodule Ctx = C.Ctx
Sourcetype t = C.t
Sourcetype clause = t

Flags

Sourcetype flag = SClause.flag
Sourceval set_flag : flag -> t -> bool -> unit

set boolean flag

Sourceval get_flag : flag -> t -> bool

get value of boolean flag

Sourceval mark_redundant : t -> unit
Sourceval is_redundant : t -> bool
Sourceval mark_backward_simplified : t -> unit
Sourceval is_backward_simplified : 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
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval compare : t -> t -> int
Sourceval id : t -> int
Sourceval lits : t -> Logtk.Literal.t array
Sourceval is_ground : t -> bool
Sourceval weight : t -> int
Sourcemodule Tbl = C.Tbl
Sourceval is_goal : t -> bool

Looking at the clause's proof, return true iff the clause is an initial (negated) goal from the problem

Sourceval distance_to_goal : t -> int option

See Proof.distance_to_goal, applied to the clause's proof

Sourceval comes_from_goal : t -> bool

true iff the clause is (indirectly) deduced from a goal or lemma

Boolean Abstraction

Printer for boolean trails, that uses Ctx to display boxes

Sourceval has_trail : t -> bool

Has a non-empty trail?

Sourceval trail : t -> Trail.t

Get the clause's trail

Sourceval trail_l : t list -> Trail.t

Merge the trails of several clauses

Sourceval update_trail : (Trail.t -> Trail.t) -> t -> t

Change the trail. The resulting clause has same parents, proof and literals as the input one

Sourceval trail_subsumes : t -> t -> bool

trail_subsumes c1 c2 = Trail.subsumes (get_trail c1) (get_trail c2)

Sourceval is_active : t -> v:Trail.valuation -> bool

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

Constructors

Sourceval create : penalty:int -> trail:Trail.t -> Logtk.Literal.t list -> 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

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

Build a new clause from the given literals.

Sourceval of_sclause : ?penalty:int -> SClause.t -> Clause_intf.proof_step -> t
Sourceval of_forms : ?penalty:int -> trail:Trail.t -> Logtk.Term.t Logtk.SLiteral.t list -> Clause_intf.proof_step -> t

Directly from list of formulas

Sourceval of_forms_axiom : ?penalty:int -> file:string -> name:string -> Logtk.Term.t Logtk.SLiteral.t list -> t

Construction from formulas as axiom (initial clause)

Sourceval of_statement : Logtk.Statement.clause_t -> t list

Extract a clause from a statement, if any

Sourceval proof_step : t -> Clause_intf.proof_step

Extract its proof from the clause

Sourceval proof : t -> Clause_intf.proof

Obtain the pair conclusion, step

Sourceval proof_parent : t -> Logtk.Proof.Parent.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)

Sourceval is_empty : t -> bool

Is the clause an empty clause?

Sourceval length : t -> int

Number of literals

Sourceval maxlits : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t

List of maximal literals

Sourceval 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

Sourceval 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.

Sourceval eligible_res_no_subst : t -> CCBV.t

More efficient version of eligible_res with Subst.empty

Sourceval 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).

Sourceval is_eligible_param : t Logtk.Scoped.t -> Logtk.Subst.t -> idx:int -> bool

Check whether the idx-th literal is eligible for paramodulation

Sourceval has_selected_lits : t -> bool

does the clause have some selected literals?

Sourceval is_selected : t -> int -> bool

check whether a literal is selected

Sourceval selected_lits : t -> (Logtk.Literal.t * int) list

get the list of selected literals

Sourceval penalty : t -> int
Sourceval is_unit_clause : t -> bool

is the clause a unit clause?

Sourceval is_oriented_rule : t -> bool

Is the clause a positive oriented clause?

Sourceval symbols : ?init:Logtk.ID.Set.t -> t Iter.t -> Logtk.ID.Set.t

symbols that occur in the clause

Sourceval to_sclause : t -> SClause.t
Sourceval to_forms : t -> Logtk.Term.t Logtk.SLiteral.t list

Easy iteration on an abstract view of literals

Sourceval to_s_form : t -> Logtk.TypedSTerm.Form.t

Iterators

Sourcemodule Seq = C.Seq

Filter literals

Sourcemodule Eligible = C.Eligible

Set of clauses

Sourcemodule ClauseSet = C.ClauseSet

Simple set

Position

Sourcemodule Pos = C.Pos

Clauses with more data

Sourcemodule WithPos = C.WithPos

Clause within which a subterm (and its position) are highlighted

IO

Sourceval pp_tstp_full : t CCFormat.printer

Print in a cnf() statement

Sourceval to_string : t -> string

Debug printing to a string

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct