package libzipperposition

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

Module Libzipperposition.ClauseSource

Clauses

The clauses are hashconsed within a context (an application of Make). Now clauses also have a trail, that is, a set of boolean literals that it depends upon as a conditional guard.

Sourceval stat_clause_create : Logtk.Util.stat
Sourcemodule type S = Clause_intf.S
Sourcetype 'c sets = {
  1. c_set : 'c CCVector.ro_vector;
    (*

    main set of clauses

    *)
  2. c_sos : 'c CCVector.ro_vector;
    (*

    set of support

    *)
}

Bundle of clause sets

Clauses that depend on a Context

Sourcemodule Make (Ctx : Ctx.S) : S with module Ctx = Ctx
OCaml

Innovation. Community. Security.