From 49009aa346176716108014db70ed57b381d2bab7 Mon Sep 17 00:00:00 2001 From: c-cube Date: Tue, 7 Dec 2021 19:11:45 +0000 Subject: [PATCH] deploy: 72d121fa648b4231e02333d517006f78149ff121 --- dev/sidekick/Sidekick_sat/Proof_dummy/Make/Step_vec/index.html | 2 ++ .../Sidekick_sat/Proof_dummy/Make/argument-1-Lit/index.html | 2 ++ dev/sidekick/Sidekick_sat/Proof_dummy/Make/index.html | 2 ++ dev/sidekick/Sidekick_sat/Proof_dummy/index.html | 2 ++ dev/sidekick/Sidekick_sat/index.html | 2 +- dev/sidekick/Sidekick_sat__Proof_dummy/.dune-keep | 0 dev/sidekick/Sidekick_sat__Proof_dummy/index.html | 2 ++ dev/sidekick/Sidekick_util/Backtrackable_ref/index.html | 2 ++ dev/sidekick/Sidekick_util/index.html | 2 +- dev/sidekick/Sidekick_util__Backtrackable_ref/.dune-keep | 0 dev/sidekick/Sidekick_util__Backtrackable_ref/index.html | 2 ++ 11 files changed, 16 insertions(+), 2 deletions(-) create mode 100644 dev/sidekick/Sidekick_sat/Proof_dummy/Make/Step_vec/index.html create mode 100644 dev/sidekick/Sidekick_sat/Proof_dummy/Make/argument-1-Lit/index.html create mode 100644 dev/sidekick/Sidekick_sat/Proof_dummy/Make/index.html create mode 100644 dev/sidekick/Sidekick_sat/Proof_dummy/index.html create mode 100644 dev/sidekick/Sidekick_sat__Proof_dummy/.dune-keep create mode 100644 dev/sidekick/Sidekick_sat__Proof_dummy/index.html create mode 100644 dev/sidekick/Sidekick_util/Backtrackable_ref/index.html create mode 100644 dev/sidekick/Sidekick_util__Backtrackable_ref/.dune-keep create mode 100644 dev/sidekick/Sidekick_util__Backtrackable_ref/index.html diff --git a/dev/sidekick/Sidekick_sat/Proof_dummy/Make/Step_vec/index.html b/dev/sidekick/Sidekick_sat/Proof_dummy/Make/Step_vec/index.html new file mode 100644 index 00000000..ba92c1e1 --- /dev/null +++ b/dev/sidekick/Sidekick_sat/Proof_dummy/Make/Step_vec/index.html @@ -0,0 +1,2 @@ + +Step_vec (sidekick.Sidekick_sat.Proof_dummy.Make.Step_vec)

Module Make.Step_vec

A vector of steps

include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_step
type t
val size : t -> int
val get : t -> int -> elt
val iter : f:(elt -> unit) -> t -> unit
val iteri : f:(int -> elt -> unit) -> t -> unit
val create : ?cap:int -> unit -> t
val clear : t -> unit
val copy : t -> t
val is_empty : t -> bool
val push : t -> elt -> unit
val fast_remove : t -> int -> unit

Remove element at index i without preserving order (swap with last element)

val filter_in_place : (elt -> bool) -> t -> unit
val ensure_size : t -> int -> unit
val pop : t -> elt
val set : t -> int -> elt -> unit
val shrink : t -> int -> unit
include Sidekick_util.Vec_sig.EXTENSIONS with type t := t and type elt := elt
val to_iter : t -> elt Iter.t
val to_array : t -> elt array
val fold_left : ('a -> elt -> 'a) -> 'a -> t -> 'a
val pp : elt CCFormat.printer -> t CCFormat.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Proof_dummy/Make/argument-1-Lit/index.html b/dev/sidekick/Sidekick_sat/Proof_dummy/Make/argument-1-Lit/index.html new file mode 100644 index 00000000..821210b6 --- /dev/null +++ b/dev/sidekick/Sidekick_sat/Proof_dummy/Make/argument-1-Lit/index.html @@ -0,0 +1,2 @@ + +Lit (sidekick.Sidekick_sat.Proof_dummy.Make.1-Lit)

Parameter Make.1-Lit

type t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Proof_dummy/Make/index.html b/dev/sidekick/Sidekick_sat/Proof_dummy/Make/index.html new file mode 100644 index 00000000..6399deb5 --- /dev/null +++ b/dev/sidekick/Sidekick_sat/Proof_dummy/Make/index.html @@ -0,0 +1,2 @@ + +Make (sidekick.Sidekick_sat.Proof_dummy.Make)

Module Proof_dummy.Make

Parameters

module Lit : sig ... end

Signature

include Solver_intf.PROOF with type lit = Lit.t and type t = unit and type proof_step = unit
type t = unit

The stored proof (possibly nil, possibly on disk, possibly in memory)

type proof_step = unit

identifier for a proof

A vector of steps

type lit = Lit.t

A boolean literal for the proof trace

type proof_rule = t -> proof_step

A proof proof_rule constructor, used to obtain proofs from theories

val enabled : t -> bool

Returns true if proof production is enabled

val emit_input_clause : lit Iter.t -> proof_rule

Emit an input clause.

val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule

Emit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.

val emit_unsat_core : lit Iter.t -> proof_rule

Produce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?

val emit_unsat : proof_step -> t -> unit

Signal "unsat" result at the given proof

val del_clause : proof_step -> lit Iter.t -> t -> unit

Forget a clause. Only useful for performance considerations.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Proof_dummy/index.html b/dev/sidekick/Sidekick_sat/Proof_dummy/index.html new file mode 100644 index 00000000..1d547843 --- /dev/null +++ b/dev/sidekick/Sidekick_sat/Proof_dummy/index.html @@ -0,0 +1,2 @@ + +Proof_dummy (sidekick.Sidekick_sat.Proof_dummy)

Module Sidekick_sat.Proof_dummy

Module for dummy proofs based on unit

Dummy proof module that does nothing.

module Make (Lit : sig ... end) : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/index.html b/dev/sidekick/Sidekick_sat/index.html index 9e860f58..18653f94 100644 --- a/dev/sidekick/Sidekick_sat/index.html +++ b/dev/sidekick/Sidekick_sat/index.html @@ -1,2 +1,2 @@ -Sidekick_sat (sidekick.Sidekick_sat)

Module Sidekick_sat

Main API

module Solver_intf : sig ... end

Interface for Solvers

module type S = Solver_intf.S
module type LIT = Solver_intf.LIT
module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
module type PROOF = Solver_intf.PROOF
type lbool = Solver_intf.lbool =
| L_true
| L_false
| L_undefined
module type SAT_STATE = Solver_intf.SAT_STATE
type 'form sat_state = 'form Solver_intf.sat_state
type ('lit, 'proof) reason = ('lit, 'proof) Solver_intf.reason =
| Consequence of unit -> 'lit list * 'proof
module type ACTS = Solver_intf.ACTS
type ('lit, 'proof, 'proof_step) acts = ('lit, 'proof, 'proof_step) Solver_intf.acts
type negated = bool
val pp_lbool : Stdlib.Format.formatter -> lbool -> unit

Print lbool values

exception No_proof
module Solver : sig ... end
module Make_cdcl_t = Solver.Make_cdcl_t
module Make_pure_sat = Solver.Make_pure_sat
\ No newline at end of file +Sidekick_sat (sidekick.Sidekick_sat)

Module Sidekick_sat

Main API

module Solver_intf : sig ... end

Interface for Solvers

module type S = Solver_intf.S
module type LIT = Solver_intf.LIT
module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
module type PROOF = Solver_intf.PROOF
type lbool = Solver_intf.lbool =
| L_true
| L_false
| L_undefined
module type SAT_STATE = Solver_intf.SAT_STATE
type 'form sat_state = 'form Solver_intf.sat_state
type ('lit, 'proof) reason = ('lit, 'proof) Solver_intf.reason =
| Consequence of unit -> 'lit list * 'proof
module type ACTS = Solver_intf.ACTS
type ('lit, 'proof, 'proof_step) acts = ('lit, 'proof, 'proof_step) Solver_intf.acts
type negated = bool
val pp_lbool : Stdlib.Format.formatter -> lbool -> unit

Print lbool values

exception No_proof
module Solver : sig ... end
module Make_cdcl_t = Solver.Make_cdcl_t
module Make_pure_sat = Solver.Make_pure_sat
module Proof_dummy : sig ... end

Module for dummy proofs based on unit

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat__Proof_dummy/.dune-keep b/dev/sidekick/Sidekick_sat__Proof_dummy/.dune-keep new file mode 100644 index 00000000..e69de29b diff --git a/dev/sidekick/Sidekick_sat__Proof_dummy/index.html b/dev/sidekick/Sidekick_sat__Proof_dummy/index.html new file mode 100644 index 00000000..6a1c2414 --- /dev/null +++ b/dev/sidekick/Sidekick_sat__Proof_dummy/index.html @@ -0,0 +1,2 @@ + +Sidekick_sat__Proof_dummy (sidekick.Sidekick_sat__Proof_dummy)

Module Sidekick_sat__Proof_dummy

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/Backtrackable_ref/index.html b/dev/sidekick/Sidekick_util/Backtrackable_ref/index.html new file mode 100644 index 00000000..b2231e7b --- /dev/null +++ b/dev/sidekick/Sidekick_util/Backtrackable_ref/index.html @@ -0,0 +1,2 @@ + +Backtrackable_ref (sidekick.Sidekick_util.Backtrackable_ref)

Module Sidekick_util.Backtrackable_ref

Backtrackable ref

type 'a t
val create : ?copy:('a -> 'a) -> 'a -> 'a t

Create a backtrackable reference holding the given value initially.

  • parameter copy

    if provided, will be used to copy the value when push_level is called.

val set : 'a t -> 'a -> unit

Set the reference's current content

val get : 'a t -> 'a

Get the reference's current content

val update : 'a t -> ('a -> 'a) -> unit

Update the reference's current content

val push_level : _ t -> unit

Push a backtracking level, copying the current value on top of some stack. The copy function will be used if it was provided in create.

val n_levels : _ t -> int

Number of saved values

val pop_levels : _ t -> int -> unit

Pop n levels, restoring to the value the reference was storing n calls to push_level earlier.

  • raises Invalid_argument

    if n is bigger than n_levels.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/index.html b/dev/sidekick/Sidekick_util/index.html index 41d1a535..ab06c286 100644 --- a/dev/sidekick/Sidekick_util/index.html +++ b/dev/sidekick/Sidekick_util/index.html @@ -1,2 +1,2 @@ -Sidekick_util (sidekick.Sidekick_util)

Module Sidekick_util

module Fmt = CCFormat
module Util : sig ... end
module Vec : sig ... end

Vectors

module VecSmallInt : sig ... end

Vectors of int32 integers

module VecI32 : sig ... end

Vectors of int32 integers

module Vec_float : sig ... end

Vectors of floats

module Vec_unit : sig ... end
module Vec_sig : sig ... end
module Bitvec : sig ... end

Bitvector

module Int_id : sig ... end
module Int_tbl = Util.Int_tbl
module Int_set = Util.Int_set
module Int_map = Util.Int_map
module IArray : sig ... end
module Backtrack_stack : sig ... end
module Backtrackable_tbl : sig ... end
module Log : sig ... end

Logging function, for debugging

module Error : sig ... end
module Bag : sig ... end
module Stat : sig ... end
module Hash : sig ... end
module Profile : sig ... end
module Chunk_stack : sig ... end

Manage a list of chunks.

module Intf = Sidekick_sigs
\ No newline at end of file +Sidekick_util (sidekick.Sidekick_util)

Module Sidekick_util

module Fmt = CCFormat
module Util : sig ... end
module Vec : sig ... end

Vectors

module VecSmallInt : sig ... end

Vectors of int32 integers

module VecI32 : sig ... end

Vectors of int32 integers

module Vec_float : sig ... end

Vectors of floats

module Vec_unit : sig ... end
module Vec_sig : sig ... end
module Bitvec : sig ... end

Bitvector

module Int_id : sig ... end
module Int_tbl = Util.Int_tbl
module Int_set = Util.Int_set
module Int_map = Util.Int_map
module IArray : sig ... end
module Backtrack_stack : sig ... end
module Backtrackable_tbl : sig ... end
module Backtrackable_ref : sig ... end
module Log : sig ... end

Logging function, for debugging

module Error : sig ... end
module Bag : sig ... end
module Stat : sig ... end
module Hash : sig ... end
module Profile : sig ... end
module Chunk_stack : sig ... end

Manage a list of chunks.

module Intf = Sidekick_sigs
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util__Backtrackable_ref/.dune-keep b/dev/sidekick/Sidekick_util__Backtrackable_ref/.dune-keep new file mode 100644 index 00000000..e69de29b diff --git a/dev/sidekick/Sidekick_util__Backtrackable_ref/index.html b/dev/sidekick/Sidekick_util__Backtrackable_ref/index.html new file mode 100644 index 00000000..6c8e89b2 --- /dev/null +++ b/dev/sidekick/Sidekick_util__Backtrackable_ref/index.html @@ -0,0 +1,2 @@ + +Sidekick_util__Backtrackable_ref (sidekick.Sidekick_util__Backtrackable_ref)

Module Sidekick_util__Backtrackable_ref

\ No newline at end of file