Module Smtlib_attribute

module Smtlib_attribute: sig .. end

SMT-LIB benchmark, logic and theory attributes.

type status =

Expected status of a benchmark.

type attribute =

`\|`	`Name of string`
`\|`	`Sorts of string list`
`\|`	`Funs of Constant.t list`
`\|`	`Preds of Constant.t list`
`\|`	`Definition of string`
`\|`	`Axioms of Term.term list`
`\|`	`Theory of attribute list`
`\|`	`Language of string`
`\|`	`Extensions of string`
`\|`	`Logic of attribute list`
`\|`	`Assumption of Term.term`
`\|`	`Formula of Term.term`
`\|`	`Status of status`
`\|`	`Notes of string`
`\|`	`Annotation of (string * string option)`

Attributes that may appear in benchmark, logic and theory files.

val assumptions : attribute list -> Term.term list

A list of all the assumptions in a collection of attributes.

val formula : attribute list -> Term.term

Formula attribute value from a collection of attributes.

val status : attribute list -> status

The status attribute of a collection of attributes.

val name : attribute list -> string

The name attribute of a collection of attributes.

val logic : attribute list -> attribute list

The logic attribute of a collection of attributes.

Hosted by the

^* web site.
^*Other names and brands may be claimed as the property of others.