Module Ast.Predicate

module Predicate: sig  end

A predicate is a boolean combination of atomic expressions. The signature allows All and Exist quantifiers, but we never use them.

type predicate =

`\|`	`True`
`\|`	`False`
`\|`	`And of predicate list`
`\|`	`Or of predicate list`
`\|`	`Not of predicate`
`\|`	`Implies of predicate * predicate`
`\|`	`Iff of predicate * predicate`
`\|`	`All of Ast.Symbol.symbol * predicate`
`\|`	`Exist of Ast.Symbol.symbol * predicate`
`\|`	`Atom of Ast.Expression.expression`

val normalize : predicate -> predicate

Various useful normalizations : e.g., And [...; False; ...] -> False etc

val conjoinL : predicate list -> predicate

val disjoinL : predicate list -> predicate

val implies : predicate -> predicate -> predicate

val iff : predicate -> predicate -> predicate

val negate : predicate -> predicate

val negateAtom : predicate -> predicate

val convertDNF : predicate -> predicate

Convert a boolean expression to DNF form.

val to_dnf : predicate -> predicate list

val toString : predicate -> string

val print : Format.formatter -> predicate -> unit

val allVarExps : predicate -> Ast.Expression.expression list

val allVarExps_deep : predicate -> Ast.Expression.lval list

val getAtoms : predicate -> predicate list

val map : (Ast.Symbol.symbol -> Ast.Symbol.symbol) ->
       ((Ast.Expression.lval -> bool) ->
        Ast.Expression.expression -> Ast.Expression.expression) ->
       predicate -> predicate

map sym_f expr_f p ==> p' Return a predicate with the same structure, and sym_f applied to each bound* symbol at the place where it is bound, and expr_f applied to each expression. The first argument passed to expr_f is a function that tests whether its argument is *bound*.

val alpha_convert : (Ast.Expression.lval -> Ast.Expression.lval) ->
       predicate -> predicate

val deep_alpha_convert : (Ast.Expression.lval -> Ast.Expression.expression) ->
       predicate -> predicate

substitute

val substitute : (Ast.Expression.expression * Ast.Expression.expression) list ->
       predicate -> predicate

val canonicize : predicate -> predicate