module Yices:`sig`

..`end`

Yices binding for Ocaml

See the official C API documentation

`type `

context

`type `

typ

`type `

expr

`type `

var_decl

`type `

model

type`assertion_id =`

`int`

`type `

lbool =

`|` |
`False` |

`|` |
`Undef` |

`|` |
`True` |

`type `

var_decl_iterator

type`unsat_core =`

`assertion_id array`

`context`

A context sotres a collection of declarations and asserations.
`expr`

Expressions (abstract syntax tree)

`typ`

Types (abstract syntax tree)

`var_decl`

Variable declaration.
A declaration consists of a name a type (such as `x::bool`

). An
instance of the declaration represents the term `x`

. Instances are also
called name expressions. Instances can be created using
`Yices.mk_bool_var_from_decl`

or `Yices.mk_var_from_decl`

.

`model`

Model. A model assigns constant values to variables defined in a context.
The context must be known to be consistent for a model to be available.
The model is constructed by calling `Yices.check`

(or its relatives) then
`Yices.get_model`

.

`assertion_id`

Assertion index, to identify retractable assertions.

`unsat_core`

Arrays of assertion indexes.

`lbool`

Extended booleans: to represent the value of literals in the context

`val version : ``unit -> string`

Return the Yices version number.

`val set_verbosity : ``int -> unit`

Set the verbosity level.

`val enable_type_checker : ``bool -> unit`

Force Yices to type check expressions when they are asserted (default = false).

`val enable_log_file : ``string -> unit`

Enable a log file that will store the assertions, checks, decls, etc.

If the log file is already open, then nothing happens.

**Raises** `Failure`

if either:

- there's already a log file
- if the file cannot be opened for write (or some other file error)

`val set_arith_only : ``bool -> unit`

Inform yices that only arithmetic theory is going to be used.

This flag usually improves performance (default = false).

`val set_max_num_conflicts_in_maxsat_iteration : ``int -> unit`

Set the maximum number of conflicts that are allowed in a maxsat iteration.

If the maximum is reached, then "unknown" (i.e., `Undef`

) is returned by maxsat.

`val set_max_num_iterations_in_maxsat : ``int -> unit`

Set the maximum number of iterations in the MaxSAT algorithm.

If the maximum is reached, then "unknown" (i.e., `Undef`

) is returned by maxsat.

`val set_maxsat_initial_cost : ``int64 -> unit`

Set the initial cost for a maxsat problem.

`val mk_context : ``unit -> context`

`mk_context ()`

creates a logical context.`val del_context : ``context -> unit`

`del_context ctx`

deletes the given logical context.
See `Yices.mk_context`

.

`val reset : ``context -> unit`

`reset ctx`

resets the given logical context.`val dump_context : ``context -> unit`

Display the internal representation of the given logical context on

`stderr`

.
This function is mostly for debugging.

`val push : ``context -> unit`

Create a backtracking point in the given logical context.

The logical context can be viewed as a stack of contexts.
The scope level is the number of elements on this stack. The stack
of contexts is simulated using trail (undo) stacks.

`val pop : ``context -> unit`

Backtrack.

Restores the context from the top of the stack, and pops it off the
stack. Any changes to the logical context (by `Yices.assert_simple`

or
other functions) between the matching `Yices.push`

and `pop`

operators are flushed, and the context is completely restored to
what it was right before the `Yices.push`

.

See `Yices.push`

.

`val assert_simple : ``context -> expr -> unit`

Assert a constraint in the logical context.

After one assertion, the logical context may become inconsistent.
The method `Yices.inconsistent`

may be used to check that.

`val assert_weighted : ``context -> expr -> int64 -> assertion_id`

Assert a constraint in the logical context with weight

**Returns** An id that can be used to retract the constraint.

`w`

.
See `Yices.retract`

.

`val assert_retractable : ``context -> expr -> assertion_id`

Assert a constraint that can be later retracted.

**Returns** An id that can be used to retract the constraint.

This is similar to `Yices.assert_weighted`

, but the weight is considered to be infinite.

See `Yices.retract`

.

`val retract : ``context -> assertion_id -> unit`

Retract a retractable or weighted constraint.

`val inconsistent : ``context -> int`

Check whether the logical context is known to be inconsistent.

If the function returns true (i.e., a non-zero value) then the context
is inconsistent. If it returns false (i.e., 0) then the context's status
is unknown. To determine the status in this case, call `Yices.check`

.

`val check : ``context -> lbool`

Check if the logical context is satisfiable.

`True`

means the context is satisfiable`False`

means it is unsatisfiable`Undef`

means it was not possible to decide due to an incompleteness.

`Yices.get_model`

can be used to obtain a model.
**Warning!** This method ignore the weights associated with the constraints.

`val max_sat : ``context -> lbool`

Compute the maximal satisfying assignment for the asserted
weighted constraints.

`True`

means the maximal satisfying assignment was found`False`

means it is unsatisfiable (this may happen if the context has unweighted constraints)`Undef`

means it was not possible to decide due to an incompleteness.

`True`

, then `Yices.get_model`

can be used to obtain a model.
`val max_sat_cost_leq : ``context -> int64 -> lbool`

Similar to

**Returns**

`Yices.max_sat`

, but start looking for models with cost
less than of equal to `max_cost`

.`False`

if such a model doesn't exist.`val find_weighted_model : ``context -> bool -> lbool`

`find_weighted_model ctx random`

searches for a model of the constraints
asserted in `ctx`

and compute its cost.
If `random`

is true, then random search is used,
otherwise, the default decision heuristic is used.

If there are no weighted constaints in `ctx`

, then this function is the
same as `Yices.check`

.

Otherwise, it searches for a model that satisfies all the
non-weighted constraints but not necessarily the weighted
constraints. The function returns `True`

if such a model is
found, and the model can be obtained using `Yices.get_model`

. The
cost of this model is the sum of the weights of the unsatisfied
weighted constraints.

The function returns `False`

if it cannot find such a model.

The function may also return `Undef`

, if the context contains
formulas for which yices is incomplete (e.g., quantifiers). Do not
use the model in this case.

`val get_unsat_core : ``context -> unsat_core`

Get the unsat core as an array.

Each element is the id of a retractable assertion.

`val get_model : ``context -> model`

Return a model for a satisfiable logical context.

**Raises**

**Warning!**

- The should be only called if
`Yices.check`

or`Yices.max_sat`

returned`True`

or`Undef`

. - Calls to functions which modify the context invalidate the model.

`Failure`

if the model is not available`val get_value : ``model -> var_decl -> lbool`

`get_value m v`

returns the assignment for the variable `v`

.
The result is `Undef`

if the value of `v`

is a "don't care".

**Warning!** `v`

must be the declaration of a boolean variable.

See `Yices.get_int_value`

, `Yices.get_arith_value`

and `Yices.get_double_value`

.

`val get_int_value : ``model -> var_decl -> int32`

`get_int_value m v`

returns the integer value assigned to variable `v`

in model `m`

`Failure`

if one of the following errors occurs:`v`

is not a proper declaration or not the declaration of a numerical variable`v`

has no value assigned in model m (typically, this means that`v`

does not occur in the asserted constraints)`v`

has a value that cannot be converted to`long`

, because it is rational or too big

`Yices.get_value`

, `Yices.get_arith_value`

and `Yices.get_double_value`

.`val get_arith_value : ``model -> var_decl -> int32 * int32`

`get_arith_value m v`

returns the rational value as a pair (numerator, denominator)`Failure`

if one of the following errors occurs:`v`

is not a proper declaration or not the declaration of a numerical variable`v`

has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)`v`

has a value that cannot be converted to`long/long`

, because the numerator or the denominator is too big

`Yices.get_value`

, `Yices.get_int_value`

and `Yices.get_double_value`

.`val get_double_value : ``model -> var_decl -> float`

`get_double_value m v`

converts the value assigned to variable `v`

in model `m`

to a floating point number and returns it.`Failure`

if one of the following errors occurs:`v`

is not a proper declaration or not the declaration of a numerical variable`v`

has no value assigned in model`m`

(typically, this means that`v`

does not occur in the asserted constraints)

`Yices.get_value`

, `Yices.get_int_value`

and `Yices.get_arith_value`

.`val get_arith_value_as_string : ``model -> var_decl -> string`

`get_arith_value_as_string m d`

converts the value assigned to a variable,
given its variable declaration `d`

in model `m`

to a character string.`val get_ratio_value : ``model -> var_decl -> Ratio.ratio`

`val get_big_int_value : ``model -> var_decl -> Big_int.big_int`

`val get_bitvector_value : ``model -> var_decl -> int -> bool array`

`get_bitvector_value m v n`

gets the bitvector constant assigned to a
variable `v`

in model `m`

.
It returns an array of `n`

booleans: `bv.(0)`

is the low-order
bit and `bv.(n - 1)`

is the high-order bit.

`n`

should be the size of the bitvector variable `v`

. Otherwise:

- If
`n`

is smaller than`v`

's size, the`n`

lower-order bits of`v`

are returned. - If
`n`

is larger than`v`

's size, then the extra high-order bits are set to 0.

`Failure`

if one of the following errors occurs:`v`

is not a proper declaration or not the declaration of a bitvector variable`v`

has no value assigned in model`m`

(typically, this means that`v`

does not occur in the asserted constraints)

`val get_bv_value : ``model -> var_decl -> int -> bool array`

Alias of

`Yices.get_bitvector_value`

.`val get_scalar_value : ``model -> var_decl -> int`

`get_scalar_value m d`

gets the value assigned to a variable of scalar
type in model `m`

as an integer index.
If `d`

is a variable declaration of a scalar type `tau`

, then
`tau`

must have been defined as `(define-type tau (scalar e_0 ... e_(n-1)))`

for some `n>0`

.

This function returns the value of variable `d`

in model `m`

as an index
between `0`

and `n-1`

(i.e., if the function returns `i`

then the
value of d is `e_i`

).

**Raises** `Failure`

if one of the following error occurs:

`d`

is not the declaration of a scalar variable`d`

is not assigned a value in model`m`

`val get_scalar_value_name : ``model -> var_decl -> string`

`get_scalar_value_name m d`

gets the value assigned to a variable of
scalar type in model `m`

as a string.
If `d`

is a variable declaration of a scalar type `tau`

, then `tau`

must
have been defined as `(define-type tau (scalar e_0 ... e_(n-1)))`

for some `n>0`

.

This function returns the value of variable `d`

in model `m`

as one of the
strings `e_i`

.

**Raises** `Failure`

if one of the following error occurs:

`d`

is not the declaration of a scalar variable`d`

is not assigned a value in model`m`

`val get_assertion_value : ``model -> assertion_id -> bool`

Return true (false) if the assertion of the given assertion id is satisfied (not
satisfied) in the model.

This function is only useful for assertion ids obtained using `Yices.assert_weighted`

,
and if `Yices.max_sat`

was used to build the model. That is the only scenario where an
assertion may not be satisfied in a model produced by yices.

`val evaluate_in_model : ``model -> expr -> lbool`

Evaluate a formula in a model.

Model can be obtained via `Yices.get_model`

, after a call to `Yices.check`

,
`Yices.max_sat`

, or `Yices.find_weighted_model`

`True`

means the formula is true in the model`False`

means the formula is false in the model`Undef`

means the model does not have enough information. typically this is due to a function application, e.g., the model defines`(f 1)`

and`(f 2)`

, but the formula references`(f 3)`

`val display_model : ``model -> unit`

Display the given model in the standard output.

`val get_cost : ``model -> int64`

Return the cost of model

`m`

.
The cost is the sum of the weights of unsatisfied constraints.

**Warning!** The model cost is computed automatically by `Yices.max_sat`

but
not by `Yices.check`

. If `Yices.check`

returns `True`

(or `Undef`

),
you can to call `compute_model_cost`

to compute the cost explicitly.
**But this function does not seem to exist yet... MD**

`val get_cost_as_double : ``model -> float`

Return the cost of the model m, converted to a double-precision
floating point number.

`val iter_bool_var_decl : ``(var_decl -> unit) -> context -> unit`

`val parse_expression : ``context -> string -> expr`

`parse_expression ctx s`

parses string `s`

as a Yices expression and return the expression.
The string must use the Yices input language (not SMT-LIB).`val parse_type : ``context -> string -> typ`

`parse_type ctx s`

parses string `s`

as a Yices type and return the type.
The string must uses the Yices input language (not SMT-LIB).`val parse_command : ``context -> string -> unit`

`parse_command ctx s`

parses and executes the command in string `s`

.
s must use the Yices input language.`val mk_type : ``context -> string -> typ`

`mk_type ctx name`

returns the type associated with the given name. If the type
does not exist, a new uninterpreted type is created.
*Remark:* number, real, int, nat, bool, any are builtin types.

`val number_type_name : ``string`

`val real_type_name : ``string`

`val int_type_name : ``string`

`val nat_type_name : ``string`

`val bool_type_name : ``string`

`val any_type_name : ``string`

`val mk_bitvector_type : ``context -> int -> typ`

`mk_bitvector_typ ctx size`

returns the bitvector type of the given size `(bv size)`

.
The size must be positive.

`val mk_bv_type : ``context -> int -> typ`

Alias of

`Yices.mk_bv_type`

`val mk_function_type : ``context -> typ array -> typ -> typ`

`mk_function_type ctx d r`

returns a function type `(-> d1 ... dn r)`

.`val mk_tuple_type : ``context -> typ array -> typ`

`mk_tuple_type ctx a`

constructs the tuple type `(a0, ..., an)`

.`val mk_bool_var_decl : ``context -> string -> var_decl`

`mk_bool_var_decl ctx name`

returns a new boolean variable declaration.`Failure`

if a variable already exists with the same name.
*Remark:* Short for `mk_var_decl ctx name (mk_type ctx "bool")`

.

`val mk_var_decl : ``context -> string -> typ -> var_decl`

`mk_var_decl ctx name type`

returns a new (global) variable declaration. It is an error to create two variables
with the same name.`val get_var_decl_from_name : ``context -> string -> var_decl`

`get_var_decl_from_name ctx name`

returns a variable declaration associated with the given name.`Failure`

if there is no variable declaration associated with the given name.`val get_var_decl : ``expr -> var_decl`

`get_var_decl e`

returns the variable declaration object associated with
the given name expression.
**Warning!** `e`

must be a name expression created using methods such
as: `Yices.mk_bool_var`

, `Yices.mk_fresh_bool_var`

, or `Yices.mk_bool_var_from_decl`

.

`val get_var_decl_name : ``var_decl -> string`

`get_var_decl_name d`

returns a name of a variable declaration.`val mk_var_from_decl : ``context -> var_decl -> expr`

`mk_var_from_decl ctx d`

returns a name expression (instance) using the given variable declaration.`val mk_bool_var_from_decl : ``context -> var_decl -> expr`

`mk_bool_var_from_decl ctx d`

returns a name expression (instance) using the given variable declaration.`val mk_bool_var : ``context -> string -> expr`

`mk_bool_var ctx name`

returns a name expression for the given variable name.
`mk_bool_var ctx n1 = mk_bool_var ctx n2`

when `n1 = n2`

.

See `Yices.mk_bool_var_decl`

, `Yices.mk_fresh_bool_var`

, `Yices.mk_bool_var_from_decl`

.

`val mk_fresh_bool_var : ``context -> expr`

`mk_fresh_bool_var ctx`

returns a fresh boolean variable.`val mk_true : ``context -> expr`

`mk_true ctx`

returns an expression representing `true`

.`val mk_false : ``context -> expr`

`mk_false ctx`

returns an expression representing `false`

.`val mk_or : ``context -> expr array -> expr`

`mk_or ctx args`

returns an expression representing the disjunction `or`

of the given arguments (as an array).
**Warning!** the length of the array must be greater than 0.

`val mk_and : ``context -> expr array -> expr`

`mk_and ctx args`

returns an expression representing the conjunction `and`

of the given arguments (as an array).
**Warning!** the length of the array must be greater than 0.

`val mk_not : ``context -> expr -> expr`

`mk_not ctx a`

returns an expression representing `(not a)`

.`val mk_eq : ``context -> expr -> expr -> expr`

`mk_eq ctx a1 a2`

returns an expression representing `a1 = a2`

.`val mk_diseq : ``context -> expr -> expr -> expr`

`mk_eq ctx a1 a2`

returns an expression representing `a1 /= a2`

.`val mk_ite : ``context -> expr -> expr -> expr -> expr`

`mk_ite ctx c t e`

returns an expression representing `(if c t e)`

(if `val mk_app : ``context -> expr -> expr array -> expr`

`mk_app ctx f a`

returns a function application term `(f a1 ... an)`

.
The type of `f`

must be a function type, and its arity must
be equal to the number of arguments, that is the size of the array `a`

.

`val mk_function_update : ``context -> expr -> expr array -> expr -> expr`

`mk_function_update ctx f a v`

returns a function update term
`(update f (a1 ... an) v)`

.
The type of `f`

must be a function type, and its arity must
be equal to the number of arguments, that is the size of the array `a`

.

`val mk_tuple_literal : ``context -> expr array -> expr`

`mk_tuple_literal ctx a`

Build the tuple term `(tuple a1 ... an)`

.`val mk_num : ``context -> int -> expr`

`mk_num ctx n`

returns an expression representing the given integer.`val mk_num_from_string : ``context -> string -> expr`

`mk_num_from_string ctx n`

returns an expression representing the number provided in ASCII format.`val mk_sum : ``context -> expr array -> expr`

`mk_sum ctx arr`

returns an expression representing `arr.(0) + ... + arr.(n)`

.
**Warning!** `Array.length arr`

must be greater than zero.

`val mk_sub : ``context -> expr array -> expr`

`mk_sub ctx arr`

returns an expression representing `arr.(0) - ... - arr.(n)`

.
**Warning!** `Array.length arr`

must be greater than zero.

`val mk_mul : ``context -> expr array -> expr`

`mk_mul ctx arr`

returns an expression representing `arr.(0) * ... * arr.(n)`

.
**Warning!** `Array.length arr`

must be greater than zero.

`val mk_lt : ``context -> expr -> expr -> expr`

`mk_lt ctx a1 a2`

returns an expression representing `a1 < a2`

.`val mk_le : ``context -> expr -> expr -> expr`

`mk_le ctx a1 a2`

returns an expression representing `a1 <= a2`

.`val mk_gt : ``context -> expr -> expr -> expr`

`mk_gt ctx a1 a2`

returns an expression representing `a1 > a2`

.`val mk_ge : ``context -> expr -> expr -> expr`

`mk_ge ctx a1 a2`

returns an expression representing `a1 >= a2`

.`val mk_bv_constant : ``context -> int -> int32 -> expr`

`mk_bv_constant ctx size value`

creates a bit vector constant of
`size`

bits and from the given `value`

.
`size`

must be positive.

`val mk_bv_constant_from_array : ``context -> bool array -> expr`

`mk_bv_constant ctx size bv`

creates a bit vector constant from an array
of booleans `bv`

.
Bit `i`

of the bitvector is set to 0 if `bv.(i)`

is `false`

and to 1 if `bv.(i)`

is `true`

.

`val mk_bv_add : ``context -> expr -> expr -> expr`

`mk_bv_add ctx a1 a2`

Bitvector addition
`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_sub : ``context -> expr -> expr -> expr`

`mk_bv_sub ctx a1 a2`

Bitvector subtraction
`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_mul : ``context -> expr -> expr -> expr`

`mk_bv_mul ctx a1 a2`

Bitvector multiplication
`a1`

and `a2`

must be bitvector expression of same size. The result is
truncated to that size too, e.g., multiplication of two 8-bit vectors
gives an 8-bit result.

`val mk_bv_minus : ``context -> expr -> expr`

`mk_bv_minus ctx a1`

Bitvector opposite
`a1`

must be bitvector expression. The result is `(- a1)`

.

`val mk_bv_concat : ``context -> expr -> expr -> expr`

`mk_bv_concat ctx a1 a2`

Bitvector concatenation
`a1`

and `a2`

must be two bitvector expressions. `a1`

is the left
part of the result and `a2`

the right part.

Assuming `a1`

and `a2`

have `n1`

and `n2`

bits, respectively,
then the result is a bitvector `concat`

of size `n1 + n2`

. Bit
0 of `concat`

is bit 0 of `a2`

and bit `n2`

of `concat`

is bit 0
of `a1`

.

`val mk_bv_and : ``context -> expr -> expr -> expr`

`mk_bv_and ctx a1 a2`

Bitwise and
`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_or : ``context -> expr -> expr -> expr`

`mk_bv_or ctx a1 a2`

Bitwise or
`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_xor : ``context -> expr -> expr -> expr`

`mk_bv_xor ctx a1 a2`

Bitwise exclusive or
`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_not : ``context -> expr -> expr`

`mk_bv_not ctx a`

Bitwise negation`val mk_bv_extract : ``context -> int -> int -> expr -> expr`

`mk_bv_extract ctx end begin a`

extracts a subvector from the bitvector `a`

.
`a`

must a bitvector expression of size `n`

with `begin < end < n`

.
The result is the subvector from `a[begin]`

to `a[end]`

.

`val mk_bv_sign_extend : ``context -> expr -> int -> expr`

`mk_bv_sign_extend ctx a n`

returns the sign extension of the bitvector `a`

to `n`

bits.
Append `n`

times the most-significant bit of `a`

to the left of `a`

.

`val mk_bv_shift_left0 : ``context -> expr -> int -> expr`

`mk_bv_shift_left0 ctx a n`

Left shift by `n`

bits, padding with zeros.`val mk_bv_shift_left1 : ``context -> expr -> int -> expr`

`mk_bv_shift_left1 ctx a n`

Left shift by `n`

bits, padding with ones.`val mk_bv_shift_right0 : ``context -> expr -> int -> expr`

`mk_bv_shift_right0 ctx a n`

Right shift by `n`

bits, padding with zeros.`val mk_bv_shift_right1 : ``context -> expr -> int -> expr`

`mk_bv_shift_right1 ctx a n`

Right shift by `n`

bits, padding with ones.`val mk_bv_lt : ``context -> expr -> expr -> expr`

`mk_bv_lt ctx a1 a2`

Unsigned comparison: `(a1 < a2)`

`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_le : ``context -> expr -> expr -> expr`

`mk_bv_le ctx a1 a2`

Unsigned comparison: `(a1 <= a2)`

`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_gt : ``context -> expr -> expr -> expr`

`mk_bv_gt ctx a1 a2`

Unsigned comparison: `(a1 > a2)`

`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_ge : ``context -> expr -> expr -> expr`

`mk_bv_ge ctx a1 a2`

Unsigned comparison: `(a1 >= a2)`

`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_slt : ``context -> expr -> expr -> expr`

`mk_bv_slt ctx a1 a2`

Signed comparison: `(a1 < a2)`

`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_sle : ``context -> expr -> expr -> expr`

`mk_bv_sle ctx a1 a2`

Signed comparison: `(a1 <= a2)`

`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_sgt : ``context -> expr -> expr -> expr`

`mk_bv_sgt ctx a1 a2`

Signed comparison: `(a1 > a2)`

`a1`

and `a2`

must be bitvector expression of same size.

`val mk_bv_sge : ``context -> expr -> expr -> expr`

`mk_bv_sge ctx a1 a2`

Signed comparison: `(a1 >= a2)`

`a1`

and `a2`

must be bitvector expression of same size.

`val pp_expr : ``expr -> unit`

Pretty print the given expression in the standard output.

module Future:`sig`

..`end`

Untested and potentially harmful features