diff --git a/dev/sidekick-base/Sidekick_base/Lit/index.html b/dev/sidekick-base/Sidekick_base/Lit/index.html index 447c3e56..0f2f662e 100644 --- a/dev/sidekick-base/Sidekick_base/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base.Lit)

Module Sidekick_base.Lit

include Sidekick_core.LIT with module T = Solver_arg
module T = Solver_arg

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base.Lit)

Module Sidekick_base.Lit

include Sidekick_core.LIT with module T = Solver_arg
module T = Solver_arg

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Lit/index.html b/dev/sidekick-base/Sidekick_base__/Lit/index.html index 91f3c879..4a24577a 100644 --- a/dev/sidekick-base/Sidekick_base__/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base__/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base__.Lit)

Module Sidekick_base__.Lit

include Sidekick_core.LIT with module T = Sidekick_base.Solver_arg
module T = Sidekick_base.Solver_arg

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base__.Lit)

Module Sidekick_base__.Lit

include Sidekick_core.LIT with module T = Sidekick_base.Solver_arg
module T = Sidekick_base.Solver_arg

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Lit/index.html b/dev/sidekick-base/Sidekick_base__Lit/index.html index 862e8479..9ce8f714 100644 --- a/dev/sidekick-base/Sidekick_base__Lit/index.html +++ b/dev/sidekick-base/Sidekick_base__Lit/index.html @@ -1,2 +1,2 @@ -Sidekick_base__Lit (sidekick-base.Sidekick_base__Lit)

Module Sidekick_base__Lit

include Sidekick_core.LIT with module T = Sidekick_base.Solver_arg
module T = Sidekick_base.Solver_arg

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Sidekick_base__Lit (sidekick-base.Sidekick_base__Lit)

Module Sidekick_base__Lit

include Sidekick_core.LIT with module T = Sidekick_base.Solver_arg
module T = Sidekick_base.Solver_arg

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/Lit/index.html index 64e2d148..b85b0bcd 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Solver/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Solver/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Solver.Lit)

Module Solver.Lit

module T : sig ... end
type t = Solver_arg.Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Solver.Lit)

Module Solver.Lit

module T : sig ... end
type t = Solver_arg.Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Actions/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Actions/Lit/index.html index b3675585..bdd83bab 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Actions/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Actions/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.CC.Actions.Lit)

Module Actions.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.CC.Actions.Lit)

Module Actions.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Lit/index.html index f6f8ed40..54003b5b 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.CC.Lit)

Module CC.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.CC.Lit)

Module CC.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/Lit/index.html index a93a207d..ad0d272c 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.Lit)

Module Solver_internal.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.Lit)

Module Solver_internal.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Lit/index.html index ef9964a6..ba606391 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Lit)

Module S.Lit

module T : sig ... end
type t = Solver_arg.Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Lit)

Module S.Lit

module T : sig ... end
type t = Solver_arg.Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Actions/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Actions/Lit/index.html index 5c5d0192..ac07773d 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Actions/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Actions/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.CC.Actions.Lit)

Module Actions.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.CC.Actions.Lit)

Module Actions.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Lit/index.html index 853a5db6..755c2ad7 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.CC.Lit)

Module CC.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.CC.Lit)

Module CC.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/Lit/index.html index b2b2b8ad..fbbbf48b 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.Lit)

Module Solver_internal.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.Lit)

Module Solver_internal.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Lit/index.html index a4da4120..9959d9a1 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_data.A.S.Lit)

Module S.Lit

module T : sig ... end
type t = Solver_arg.Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_data.A.S.Lit)

Module S.Lit

module T : sig ... end
type t = Solver_arg.Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/CC/Actions/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/CC/Actions/Lit/index.html index 1049c46c..d321412c 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/CC/Actions/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/CC/Actions/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_data.A.S.Solver_internal.CC.Actions.Lit)

Module Actions.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_data.A.S.Solver_internal.CC.Actions.Lit)

Module Actions.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/CC/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/CC/Lit/index.html index dccdd95f..2f7444c3 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/CC/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/CC/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_data.A.S.Solver_internal.CC.Lit)

Module CC.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_data.A.S.Solver_internal.CC.Lit)

Module CC.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/Lit/index.html index b83b8be5..796cccf2 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_data.A.S.Solver_internal.Lit)

Module Solver_internal.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_data.A.S.Solver_internal.Lit)

Module Solver_internal.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Lit/index.html index 8e6c3b57..474453fd 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Lit)

Module S.Lit

module T : sig ... end
type t = Solver_arg.Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Lit)

Module S.Lit

module T : sig ... end
type t = Solver_arg.Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/CC/Actions/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/CC/Actions/Lit/index.html index 0dc58d96..bc418a97 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/CC/Actions/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/CC/Actions/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Solver_internal.CC.Actions.Lit)

Module Actions.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Solver_internal.CC.Actions.Lit)

Module Actions.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/CC/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/CC/Lit/index.html index c6ff33db..2a73e3c4 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/CC/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/CC/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Solver_internal.CC.Lit)

Module CC.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Solver_internal.CC.Lit)

Module CC.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/Lit/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/Lit/index.html index 9483e0d8..4f7038c5 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/Lit/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Solver_internal.Lit)

Module Solver_internal.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Solver_internal.Lit)

Module Solver_internal.Lit

module T : sig ... end
type t = Lit.t
val term : t -> T.Term.t
val sign : t -> bool
val neg : t -> t
val abs : t -> t
val signed_term : t -> T.Term.t * bool
val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t
val norm_sign : t -> t * bool
val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/Lit/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/Lit/index.html index f05c3a73..317960b3 100644 --- a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/Lit/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-bin.Sidekick_smtlib.Process.Solver.Lit)

Module Solver.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-bin.Sidekick_smtlib.Process.Solver.Lit)

Module Solver.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/index.html index 584681d5..fc6891a4 100644 --- a/dev/sidekick-bin/Sidekick_smtlib/Process/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib/Process/index.html @@ -1,2 +1,2 @@ -Process (sidekick-bin.Sidekick_smtlib.Process)

Module Sidekick_smtlib.Process

Process Statements

module Solver : Sidekick_smt_solver.S with type T.Term.t = Sidekick_base.Term.t and type T.Term.store = Sidekick_base.Term.store and type T.Ty.t = Sidekick_base.Ty.t and type T.Ty.store = Sidekick_base.Ty.store and type proof = Sidekick_base.Proof_stub.t
val th_bool : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
type 'a or_error = ('a, string) CCResult.t
module Check_cc : sig ... end
val process_stmt : ?⁠gc:bool -> ?⁠restarts:bool -> ?⁠pp_cnf:bool -> ?⁠proof_file:string -> ?⁠pp_model:bool -> ?⁠check:bool -> ?⁠time:float -> ?⁠memory:float -> ?⁠progress:bool -> Solver.t -> Sidekick_base.Statement.t -> unit or_error
\ No newline at end of file +Process (sidekick-bin.Sidekick_smtlib.Process)

Module Sidekick_smtlib.Process

Process Statements

module Solver : Sidekick_smt_solver.S with type T.Term.t = Sidekick_base.Term.t and type T.Term.store = Sidekick_base.Term.store and type T.Ty.t = Sidekick_base.Ty.t and type T.Ty.store = Sidekick_base.Ty.store and type proof = Sidekick_base.Proof_stub.t
val th_bool : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
type 'a or_error = ('a, string) CCResult.t
module Check_cc : sig ... end
val process_stmt : ?⁠gc:bool -> ?⁠restarts:bool -> ?⁠pp_cnf:bool -> ?⁠pp_model:bool -> ?⁠check:bool -> ?⁠time:float -> ?⁠memory:float -> ?⁠progress:bool -> Solver.t -> Sidekick_base.Statement.t -> unit or_error
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/Lit/index.html b/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/Lit/index.html index 5231e0c2..0d31482e 100644 --- a/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/Lit/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-bin.Sidekick_smtlib__.Process.Solver.Lit)

Module Solver.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-bin.Sidekick_smtlib__.Process.Solver.Lit)

Module Solver.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib__/Process/index.html b/dev/sidekick-bin/Sidekick_smtlib__/Process/index.html index 3fc7f01c..00bada3e 100644 --- a/dev/sidekick-bin/Sidekick_smtlib__/Process/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib__/Process/index.html @@ -1,2 +1,2 @@ -Process (sidekick-bin.Sidekick_smtlib__.Process)

Module Sidekick_smtlib__.Process

Process Statements

val th_bool : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
type 'a or_error = ('a, string) CCResult.t
module Check_cc : sig ... end
val process_stmt : ?⁠gc:bool -> ?⁠restarts:bool -> ?⁠pp_cnf:bool -> ?⁠proof_file:string -> ?⁠pp_model:bool -> ?⁠check:bool -> ?⁠time:float -> ?⁠memory:float -> ?⁠progress:bool -> Solver.t -> Sidekick_base.Statement.t -> unit or_error
\ No newline at end of file +Process (sidekick-bin.Sidekick_smtlib__.Process)

Module Sidekick_smtlib__.Process

Process Statements

val th_bool : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
type 'a or_error = ('a, string) CCResult.t
module Check_cc : sig ... end
val process_stmt : ?⁠gc:bool -> ?⁠restarts:bool -> ?⁠pp_cnf:bool -> ?⁠pp_model:bool -> ?⁠check:bool -> ?⁠time:float -> ?⁠memory:float -> ?⁠progress:bool -> Solver.t -> Sidekick_base.Statement.t -> unit or_error
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/Lit/index.html b/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/Lit/index.html index b970ecf5..382701bf 100644 --- a/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/Lit/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick-bin.Sidekick_smtlib__Process.Solver.Lit)

Module Solver.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick-bin.Sidekick_smtlib__Process.Solver.Lit)

Module Solver.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib__Process/index.html b/dev/sidekick-bin/Sidekick_smtlib__Process/index.html index 33a578fc..9816fdc1 100644 --- a/dev/sidekick-bin/Sidekick_smtlib__Process/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib__Process/index.html @@ -1,2 +1,2 @@ -Sidekick_smtlib__Process (sidekick-bin.Sidekick_smtlib__Process)

Module Sidekick_smtlib__Process

Process Statements

module Solver : Sidekick_smt_solver.S with type T.Term.t = Sidekick_base.Term.t and type T.Term.store = Sidekick_base.Term.store and type T.Ty.t = Sidekick_base.Ty.t and type T.Ty.store = Sidekick_base.Ty.store and type proof = Sidekick_base.Proof_stub.t
val th_bool : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
type 'a or_error = ('a, string) CCResult.t
module Check_cc : sig ... end
val process_stmt : ?⁠gc:bool -> ?⁠restarts:bool -> ?⁠pp_cnf:bool -> ?⁠proof_file:string -> ?⁠pp_model:bool -> ?⁠check:bool -> ?⁠time:float -> ?⁠memory:float -> ?⁠progress:bool -> Solver.t -> Sidekick_base.Statement.t -> unit or_error
\ No newline at end of file +Sidekick_smtlib__Process (sidekick-bin.Sidekick_smtlib__Process)

Module Sidekick_smtlib__Process

Process Statements

module Solver : Sidekick_smt_solver.S with type T.Term.t = Sidekick_base.Term.t and type T.Term.store = Sidekick_base.Term.store and type T.Ty.t = Sidekick_base.Ty.t and type T.Ty.store = Sidekick_base.Ty.store and type proof = Sidekick_base.Proof_stub.t
val th_bool : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
type 'a or_error = ('a, string) CCResult.t
module Check_cc : sig ... end
val process_stmt : ?⁠gc:bool -> ?⁠restarts:bool -> ?⁠pp_cnf:bool -> ?⁠pp_model:bool -> ?⁠check:bool -> ?⁠time:float -> ?⁠memory:float -> ?⁠progress:bool -> Solver.t -> Sidekick_base.Statement.t -> unit or_error
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/Lit/index.html b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/Lit/index.html index d3d1d75a..d6ebdefe 100644 --- a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/Lit/index.html +++ b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_arith_lra.Make.1-A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_arith_lra.Make.1-A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/Lit/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/Lit/index.html index b9b09a26..216b64b1 100644 --- a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/Lit/index.html +++ b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_arith_lra.ARG.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_arith_lra.ARG.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/Lit/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/Lit/index.html index f11fcf19..a677a515 100644 --- a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/Lit/index.html +++ b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_arith_lra.S.A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_arith_lra.S.A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_cc/Make/argument-1-A/Lit/index.html b/dev/sidekick/Sidekick_cc/Make/argument-1-A/Lit/index.html index a9d99abf..c09dddb5 100644 --- a/dev/sidekick/Sidekick_cc/Make/argument-1-A/Lit/index.html +++ b/dev/sidekick/Sidekick_cc/Make/argument-1-A/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_cc.Make.1-A.Lit)

Module 1-A.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_cc.Make.1-A.Lit)

Module 1-A.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_cc/module-type-S/Lit/index.html b/dev/sidekick/Sidekick_cc/module-type-S/Lit/index.html index 20764609..ad4f68ef 100644 --- a/dev/sidekick/Sidekick_cc/module-type-S/Lit/index.html +++ b/dev/sidekick/Sidekick_cc/module-type-S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_cc.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_cc.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/Lit/index.html b/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/Lit/index.html index 07fe82d4..19ebfbc6 100644 --- a/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/Lit/index.html +++ b/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_core.Monoid_of_repr.1-M.SI.Lit)

Module SI.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_core.Monoid_of_repr.1-M.SI.Lit)

Module SI.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-CC_ACTIONS/Lit/index.html b/dev/sidekick/Sidekick_core/module-type-CC_ACTIONS/Lit/index.html index 2197d29f..8b13c2a9 100644 --- a/dev/sidekick/Sidekick_core/module-type-CC_ACTIONS/Lit/index.html +++ b/dev/sidekick/Sidekick_core/module-type-CC_ACTIONS/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_core.CC_ACTIONS.Lit)

Module CC_ACTIONS.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_core.CC_ACTIONS.Lit)

Module CC_ACTIONS.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-CC_ARG/Lit/index.html b/dev/sidekick/Sidekick_core/module-type-CC_ARG/Lit/index.html index d2587d99..0136f8bd 100644 --- a/dev/sidekick/Sidekick_core/module-type-CC_ARG/Lit/index.html +++ b/dev/sidekick/Sidekick_core/module-type-CC_ARG/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_core.CC_ARG.Lit)

Module CC_ARG.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_core.CC_ARG.Lit)

Module CC_ARG.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-CC_S/Lit/index.html b/dev/sidekick/Sidekick_core/module-type-CC_S/Lit/index.html index b3e027aa..d7459644 100644 --- a/dev/sidekick/Sidekick_core/module-type-CC_S/Lit/index.html +++ b/dev/sidekick/Sidekick_core/module-type-CC_S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_core.CC_S.Lit)

Module CC_S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_core.CC_S.Lit)

Module CC_S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-LIT/index.html b/dev/sidekick/Sidekick_core/module-type-LIT/index.html index e75ecfb6..ad113ac4 100644 --- a/dev/sidekick/Sidekick_core/module-type-LIT/index.html +++ b/dev/sidekick/Sidekick_core/module-type-LIT/index.html @@ -1,2 +1,2 @@ -LIT (sidekick.Sidekick_core.LIT)

Module type Sidekick_core.LIT

Literals

Literals are a pair of a boolean-sorted term, and a sign. Positive literals are the same as their term, and negative literals are the negation of their term.

The SAT solver deals only in literals and clauses (sets of literals). Everything else belongs in the SMT solver.

module T : TERM

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file +LIT (sidekick.Sidekick_core.LIT)

Module type Sidekick_core.LIT

Literals

Literals are a pair of a boolean-sorted term, and a sign. Positive literals are the same as their term, and negative literals are the negation of their term.

The SAT solver deals only in literals and clauses (sets of literals). Everything else belongs in the SMT solver.

module T : TERM

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/Lit/index.html b/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/Lit/index.html index 7cf91bff..a0e8a20a 100644 --- a/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/Lit/index.html +++ b/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_core.MONOID_ARG.SI.Lit)

Module SI.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_core.MONOID_ARG.SI.Lit)

Module SI.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-SOLVER/Lit/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER/Lit/index.html index 5da13af4..efb681ad 100644 --- a/dev/sidekick/Sidekick_core/module-type-SOLVER/Lit/index.html +++ b/dev/sidekick/Sidekick_core/module-type-SOLVER/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_core.SOLVER.Lit)

Module SOLVER.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_core.SOLVER.Lit)

Module SOLVER.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/Lit/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/Lit/index.html index a5058b52..473a4756 100644 --- a/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/Lit/index.html +++ b/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_core.SOLVER_INTERNAL.Lit)

Module SOLVER_INTERNAL.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_core.SOLVER_INTERNAL.Lit)

Module SOLVER_INTERNAL.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_lit/Make/index.html b/dev/sidekick/Sidekick_lit/Make/index.html index 6398c8a9..f37d22ef 100644 --- a/dev/sidekick/Sidekick_lit/Make/index.html +++ b/dev/sidekick/Sidekick_lit/Make/index.html @@ -1,2 +1,2 @@ -Make (sidekick.Sidekick_lit.Make)

Module Sidekick_lit.Make

Parameters

Signature

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Make (sidekick.Sidekick_lit.Make)

Module Sidekick_lit.Make

Parameters

Signature

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Make/argument-1-A/Lit/index.html b/dev/sidekick/Sidekick_smt_solver/Make/argument-1-A/Lit/index.html index de44ad24..4b5b2805 100644 --- a/dev/sidekick/Sidekick_smt_solver/Make/argument-1-A/Lit/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Make/argument-1-A/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_smt_solver.Make.1-A.Lit)

Module 1-A.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_smt_solver.Make.1-A.Lit)

Module 1-A.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/module-type-ARG/Lit/index.html b/dev/sidekick/Sidekick_smt_solver/module-type-ARG/Lit/index.html index 29429a12..b57e11ab 100644 --- a/dev/sidekick/Sidekick_smt_solver/module-type-ARG/Lit/index.html +++ b/dev/sidekick/Sidekick_smt_solver/module-type-ARG/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_smt_solver.ARG.Lit)

Module ARG.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_smt_solver.ARG.Lit)

Module ARG.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/module-type-S/Lit/index.html b/dev/sidekick/Sidekick_smt_solver/module-type-S/Lit/index.html index 264ca6dd..311d6b2e 100644 --- a/dev/sidekick/Sidekick_smt_solver/module-type-S/Lit/index.html +++ b/dev/sidekick/Sidekick_smt_solver/module-type-S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_smt_solver.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_smt_solver.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/Lit/index.html b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/Lit/index.html index 7d2a2f20..ea19f65f 100644 --- a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/Lit/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_th_bool_static.Make.1-A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_th_bool_static.Make.1-A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/Lit/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/Lit/index.html index ac2df590..9751ec02 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/Lit/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_th_bool_static.ARG.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_th_bool_static.ARG.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/Lit/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/Lit/index.html index 05a03cc5..417a1209 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/Lit/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_th_bool_static.S.A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_th_bool_static.S.A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/Lit/index.html b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/Lit/index.html index c33f05a4..61398c39 100644 --- a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/Lit/index.html +++ b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_th_cstor.Make.1-A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_th_cstor.Make.1-A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/Lit/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/Lit/index.html index 908be13d..0a5a7f21 100644 --- a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/Lit/index.html +++ b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_th_cstor.ARG.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_th_cstor.ARG.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/Lit/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/Lit/index.html index 238e013d..0815ada5 100644 --- a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/Lit/index.html +++ b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_th_cstor.S.A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_th_cstor.S.A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/Lit/index.html b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/Lit/index.html index e8f07105..f96c3f38 100644 --- a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/Lit/index.html +++ b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_th_data.Make.1-A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_th_data.Make.1-A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/Lit/index.html b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/Lit/index.html index 164a0ab4..c0bd0efa 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/Lit/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_th_data.ARG.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_th_data.ARG.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/Lit/index.html b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/Lit/index.html index 73dba933..1d1459c4 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/Lit/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_th_data.S.A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : T.Term.store -> ?⁠sign:bool -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file +Lit (sidekick.Sidekick_th_data.S.A.S.Lit)

Module S.Lit

module T = T

Literals depend on terms

type t

A literal

val term : t -> T.Term.t

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> T.Term.t * bool

Return the atom and the sign

val atom : ?⁠sign:bool -> T.Term.store -> T.Term.t -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

parameter sign

if provided, and sign=false, negate the resulting lit.

val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

val equal : t -> t -> bool
val hash : t -> int
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file