package libzipperposition

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

Module Libzipperposition.Cut_formSource

Universally Quantified Conjunction of Clauses

Sourcetype term = Logtk.Term.t
Sourcetype form = clause list
Sourcetype t = private {
  1. vars : Logtk.Term.VarSet.t;
  2. cs : form;
}

A formula of the form forall vars. \bigand_i C_i. The C_i are clauses with free variables in vars

Sourcetype cut_form = t
Sourceval make : Logtk.Literals.t list -> t
Sourceval trivial : 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
include Logtk.Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
include Logtk.Interfaces.PRINT with type t := t
Sourceval to_string : t -> string
Sourceval cs : t -> Logtk.Literals.t list
Sourceval ind_vars : t -> var list

subset of vars that have an inductive type

Sourceval subst1 : var -> term -> t -> t

Substitution of one variable

Sourceval are_variant : t -> t -> bool

Are these two cut formulas alpha-equivalent?

Sourceval normalize : t -> t

Use rewriting to normalize the formula

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

Convert to input formula

Sourcemodule Pos : sig ... end
Sourcemodule Seq : sig ... end
Sourcemodule FV_tbl (X : Map.OrderedType) : sig ... end
OCaml

Innovation. Community. Security.