The Inez language is a superset of OCaml. We have augmented OCaml with constructs for easily expressing formulas in a fragment of first-order logic that encompasses uninterpreted functions and Linear Integer Arithmetic.

Inez extends OCaml without modifying its grammar in any way, i.e., Inez programs are representable by the Camlp4 OCaml Abstract Syntax Tree. Inez relies on constructs that are syntactically valid, but cannot possibly be part of semantically valid OCaml programs. For example, ~logic 1 is a valid Inez expression: labels like ~logic are expressions, therefore ~logic 1 is a syntactically valid application. The expression cannot possibly be semantically valid OCaml, because labels are only allowed as arguments. Previously-valid OCaml programs retain their original meaning.

Under the hood, we perform AST transformations by means of Camlp4 maps.

In most cases, terms and formulas should appear as applications of the ~logic keyword, e.g., ~logic (0 + 1). Inez preprocesses ~logic expressions to assign them the intended meaning over terms and formulas. Specifically,

• Integer literals become Inez integer terms.
• true and false become formulas.
• Operators like && and + obtain meaning over terms and formulas. (We locally open a module that defines them.)

All operators are implemented as OCaml functions. They are exported via the Logic.Ops module. Operators retain their OCaml precedence and associativity.

In what follows, we use term for the type of Inez integer terms and the type formula for the type of Inez formulas. The actual types in the implementation are more complicated: we rely on GADTs for type safety.

~- is the unary minus; you do not need ~ when applying the operator in the standard fashion.

For *, the left-hand side has to be constant.

An uninterpreted function is a function, whose body is the special keyword ~free. Any number of arguments is allowed. Lowercase identifiers and the wildcard pattern (_) can be used as arguments. The definitions below are equivalent ways of defining a function f that accepts two integer terms and produces an integer term:

• let f _ _ = ~free
• let f x y = ~free
• let f = fun _ _ -> ~free
• let f = fun _ -> fun _ -> ~free

Uninterpreted functions are OCaml functions, whose arguments and return values are terms. For example, ~logic (f 1 2) is valid and properly typed, 1 and 2 being Inez terms. f 1 2 (outside ~logic) fails with a type error, 1 and 2 being regular OCaml integers.

The ~free keyword and any of the arguments can be optionally annotated with one of the pseudo-types Int and Bool. (A Bool term is a formula.) No annotation means Int. For example,

let f1 (x : Int) (y : Bool) = (~free : Int) 

defines a function f1 of type term -> formula -> term, while

let f2 (x : Bool) = (~free : Bool) 

defines a function f2 of type formula -> formula.

The Script module provides an easy way of interacting with the solver. It is a good idea to start Inez scripts with open Script.

Terminology.result is defined as follows:

type result = R_Opt | R_Unbounded | R_Sat | R_Unsat | R_Unknown