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 =

`\|`	`Pattern of AST.ast`

val ast_of_pattern : pattern -> AST.ast

val pattern_of_ast : AST.ast -> 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.