Module Z3.Quantifier.Pattern

module Pattern: sig .. end

Quantifier patterns

Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern.

type pattern

val get_num_terms : pattern -> int

The number of terms in the pattern.

val get_terms : pattern -> Expr.expr list

The terms in the pattern.

val to_string : pattern -> string

A string representation of the pattern.