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.