package yices2

  1. Overview
  2. Docs

Boolean terms

val true_ : unit -> term

Boolean for true

val false_ : unit -> term

Boolean for false

val ite : term -> term -> term -> term

If-then-else ite cond iftrue iffalse

val eq : term -> term -> term

Generic equality

val neq : term -> term -> term

Generic inequality

val distinct : term array -> term

Distinct, all-diff.

val not : term -> term

Negation

val and2 : term -> term -> term

Conjunction

val and3 : term -> term -> term -> term
val andn : term array -> term
val or2 : term -> term -> term

Disjunction

val or3 : term -> term -> term -> term
val orn : term array -> term
val xor2 : term -> term -> term

Exclusive disjunction

val xor3 : term -> term -> term -> term
val xorn : term array -> term
val iff : term -> term -> term

Logical equivalence

val implies : term -> term -> term

Logical implication

val forall : typ -> (term -> term) -> term

Universal quantifier

val foralln : typ array -> (term array -> term) -> term
val exists : typ -> (term -> term) -> term

Existential quantifier

val existsn : typ array -> (term array -> term) -> term
OCaml

Innovation. Community. Security.